Clover coverage report -

Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST

FRAMES NO FRAMES

file stats:	LOC:	84		Methods:	2
	NCLOC:	43		Classes:	1

Source file

Conditionals

Statements

Methods

TOTAL

Minimal4InclusionModel.java

75%

94,7%

100%

89,7%

1		/*
2		* Created on 31 mars 2004
3		*
4		* To change the template for this generated file go to
5		* Window>Preferences>Java>Code Generation>Code and Comments
6		*/
7		package org.sat4j.tools;
8
9		import java.io.Serializable;
10
11		import org.sat4j.core.VecInt;
12		import org.sat4j.specs.ContradictionException;
13		import org.sat4j.specs.ISolver;
14		import org.sat4j.specs.IVecInt;
15		import org.sat4j.specs.TimeoutException;
16
17		/**
18		* Computes models with a minimal subset (with respect to set
19		* inclusion) of negative literals. This is done be adding a clause
20		* containing the negation of the negative literals appearing in the
21		* model found (which prevents any interpretation containing that subset
22		* of negative literals to be a model of the formula).
23		*
24		* Computes only one model minimal for inclusion, since there is currently no
25		* way to save the state of the solver.
26		*
27		* @author leberre
28		*
29		* @see org.sat4j.specs.ISolver#addClause(IVecInt)
30		*/
31		public class Minimal4InclusionModel extends SolverDecorator implements
32		Serializable {
33
34		private static final long serialVersionUID = 1L;
35
36		/**
37		* @param solver
38		*/
39	1	public Minimal4InclusionModel(ISolver solver) {
40	1	super(solver);
41		}
42
43		/*
44		* (non-Javadoc)
45		*
46		* @see org.sat4j.ISolver#model()
47		*/
48	10	@Override
49		public int[] model() {
50	10	int[] prevmodel = null;
51	10	IVecInt vec = new VecInt();
52	10	IVecInt cube = new VecInt();
53		// backUp();
54	10	try {
55	10	do {
56	15	prevmodel = super.model();
57	15	vec.clear();
58	15	cube.clear();
59	15	for (int q : prevmodel) {
60	45	if (q < 0) {
61	9	vec.push(-q);
62		} else {
63	36	cube.push(q);
64		}
65		}
66		// System.out.println("minimizing " + vec + "/" + cube);
67	15	addClause(vec);
68	5	} while (isSatisfiable(cube));
69		} catch (TimeoutException e) {
70		// System.err.println("Solver timed out");
71		} catch (ContradictionException e) {
72		// System.out.println("added trivial unsat clauses?" + vec);
73		}
74		// restore();
75	10	int[] newmodel = new int[vec.size()];
76	10	for (int i = 0, j = 0; i < prevmodel.length; i++) {
77	30	if (prevmodel[i] < 0) {
78	0	newmodel[j++] = prevmodel[i];
79		}
80		}
81
82	10	return newmodel;
83		}
84		}