Clover coverage report -

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

FRAMES NO FRAMES

file stats:	LOC:	108		Methods:	5
	NCLOC:	48		Classes:	1

Source file

Conditionals

Statements

Methods

TOTAL

ModelIterator.java

25%

57,9%

60%

53,6%

1		/*
2		* Created on 22 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		* That class allows to iterate through all the models
19		* (implicants) of a formula.
20		*
21		* <pre>
22		* ISolver solver = new ModelIterator(SolverFactory.OneSolver());
23		* boolean unsat = true;
24		* while (solver.isSatisfiable()) {
25		* unsat = false;
26		* int[] model = solver.model();
27		* // do something with model
28		* }
29		* if (unsat) {
30		* // UNSAT case
31		* }
32		* </pre>
33		*
34		* @author leberre
35		*/
36		public class ModelIterator extends SolverDecorator implements Serializable {
37
38		private static final long serialVersionUID = 1L;
39
40		private boolean trivialfalsity = false;
41
42		/**
43		* @param solver
44		*/
45	1	public ModelIterator(ISolver solver) {
46	1	super(solver);
47		}
48
49		/*
50		* (non-Javadoc)
51		*
52		* @see org.sat4j.ISolver#model()
53		*/
54	6	@Override
55		public int[] model() {
56	6	int[] last = super.model();
57	6	IVecInt clause = new VecInt(last.length);
58	6	for (int q : last) {
59	18	clause.push(-q);
60		}
61	6	try {
62		// System.out.println("adding " + clause);
63	6	addClause(clause);
64		} catch (ContradictionException e) {
65	0	trivialfalsity = true;
66		}
67	6	return last;
68		}
69
70		/*
71		* (non-Javadoc)
72		*
73		* @see org.sat4j.ISolver#isSatisfiable()
74		*/
75	7	@Override
76		public boolean isSatisfiable() throws TimeoutException {
77	7	if (trivialfalsity) {
78	0	return false;
79		}
80	7	trivialfalsity = false;
81	7	return super.isSatisfiable();
82		}
83
84		/*
85		* (non-Javadoc)
86		*
87		* @see org.sat4j.ISolver#isSatisfiable(org.sat4j.datatype.VecInt)
88		*/
89	0	@Override
90		public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
91	0	if (trivialfalsity) {
92	0	return false;
93		}
94	0	trivialfalsity = false;
95	0	return super.isSatisfiable(assumps);
96		}
97
98		/*
99		* (non-Javadoc)
100		*
101		* @see org.sat4j.ISolver#reset()
102		*/
103	0	@Override
104		public void reset() {
105	0	trivialfalsity = false;
106	0	super.reset();
107		}
108		}