Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
100   226   16   16,67
10   143   0,21   6
6     3,5  
1    
 
  ModelIteratorTest       Line # 27 100 16 91,4% 0.9137931
 
  (4)
 
1    /*
2    * Created on 2 avr. 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;
8   
9    import junit.framework.TestCase;
10   
11    import org.sat4j.core.VecInt;
12    import org.sat4j.minisat.SolverFactory;
13    import org.sat4j.specs.ContradictionException;
14    import org.sat4j.specs.ISolver;
15    import org.sat4j.specs.IVecInt;
16    import org.sat4j.specs.TimeoutException;
17    import org.sat4j.tools.Minimal4CardinalityModel;
18    import org.sat4j.tools.Minimal4InclusionModel;
19    import org.sat4j.tools.ModelIterator;
20   
21    /**
22    * @author leberre
23    *
24    * To change the template for this generated type comment go to
25    * Window>Preferences>Java>Code Generation>Code and Comments
26    */
 
27    public class ModelIteratorTest extends TestCase {
28    /**
29    * Constructor for ModelIteratorTest.
30    *
31    * @param arg0
32    */
 
33  4 toggle public ModelIteratorTest(String arg0) {
34  4 super(arg0);
35    }
36   
 
37  1 toggle public void testModelIterator() {
38  1 try {
39  1 ISolver solver = new ModelIterator(SolverFactory.newMiniLearning());
40  1 solver.newVar(3);
41  1 IVecInt clause = new VecInt();
42  1 clause.push(1);
43  1 clause.push(2);
44  1 clause.push(3);
45  1 solver.addClause(clause);
46  1 clause.clear();
47  1 clause.push(-1);
48  1 clause.push(-2);
49  1 clause.push(-3);
50  1 solver.addClause(clause);
51  1 int counter = 0;
52  7 while (solver.isSatisfiable()) {
53  6 solver.model();
54  6 counter++;
55    }
56  1 assertEquals(6, counter);
57    } catch (ContradictionException e) {
58  0 fail();
59    } catch (TimeoutException e) {
60  0 fail();
61    }
62    }
63   
64    // Is not Implemented Yet. We need a Backup/Restore solution to do so.
65    // public void testIncMinModel() {
66    // try {
67    // ISolver solver = new ModelIterator(new
68    // Minimal4InclusionModel(SolverFactory.newMiniLearning()));
69    // solver.newVar(3);
70    // VecInt clause = new VecInt();
71    // clause.push(1);
72    // clause.push(2);
73    // clause.push(3);
74    // solver.addClause(clause);
75    // clause.clear();
76    // clause.push(-1);
77    // clause.push(-2);
78    // clause.push(-3);
79    // solver.addClause(clause);
80    // int counter = 0;
81    // while (solver.isSatisfiable()) {
82    // int[] model = solver.model();
83    // counter++;
84    // }
85    // assertEquals(3, counter);
86    // } catch (ContradictionException e) {
87    // fail();
88    // } catch (TimeoutException e) {
89    // fail();
90    // }
91    // }
92    //
93    // public void testCardMinModel() {
94    // try {
95    // ISolver solver = new ModelIterator(new
96    // Minimal4CardinalityModel(SolverFactory.newMiniLearning()));
97    // solver.newVar(3);
98    // VecInt clause = new VecInt();
99    // clause.push(1);
100    // clause.push(2);
101    // clause.push(3);
102    // solver.addClause(clause);
103    // clause.clear();
104    // clause.push(-1);
105    // clause.push(-2);
106    // clause.push(-3);
107    // solver.addClause(clause);
108    // int counter = 0;
109    // while (solver.isSatisfiable()) {
110    // int[] model = solver.model();
111    // counter++;
112    // }
113    // assertEquals(3, counter);
114    // } catch (ContradictionException e) {
115    // fail();
116    // } catch (TimeoutException e) {
117    // fail();
118    // }
119    // }
120   
 
121  1 toggle public void testCardModel() {
122  1 try {
123  1 ISolver solver = new Minimal4CardinalityModel(SolverFactory
124    .newMiniLearning());
125  1 solver.newVar(3);
126  1 IVecInt clause = new VecInt();
127  1 clause.push(1);
128  1 clause.push(-2);
129  1 clause.push(3);
130  1 solver.addClause(clause);
131  1 clause.clear();
132  1 clause.push(-1);
133  1 clause.push(2);
134  1 clause.push(-3);
135  1 solver.addClause(clause);
136  1 int counter = 0;
137  11 while (solver.isSatisfiable() && (counter < 10)) {
138  10 solver.model();
139  10 counter++;
140    }
141  1 assertEquals(10, counter);
142    } catch (ContradictionException e) {
143  0 fail();
144    } catch (TimeoutException e) {
145  0 fail();
146    }
147    }
148   
 
149  1 toggle public void testIncModel() {
150  1 try {
151  1 ISolver solver = new Minimal4InclusionModel(SolverFactory
152    .newMiniLearning());
153  1 solver.newVar(3);
154  1 IVecInt clause = new VecInt();
155  1 clause.push(1);
156  1 clause.push(-2);
157  1 clause.push(3);
158  1 solver.addClause(clause);
159  1 clause.clear();
160  1 clause.push(-1);
161  1 clause.push(2);
162  1 clause.push(-3);
163  1 solver.addClause(clause);
164  1 int counter = 0;
165  11 while (solver.isSatisfiable() && (counter < 10)) {
166  10 solver.model();
167  10 counter++;
168    }
169  1 assertEquals(10, counter);
170    } catch (ContradictionException e) {
171  0 fail();
172    } catch (TimeoutException e) {
173  0 fail();
174    }
175    }
176   
 
177  1 toggle public void testIsSatisfiableVecInt() {
178  1 try {
179  1 ISolver solver = SolverFactory.newMiniLearning();
180  1 solver.newVar(3);
181  1 IVecInt clause = new VecInt();
182  1 clause.push(1);
183  1 clause.push(2);
184  1 clause.push(3);
185  1 solver.addClause(clause);
186  1 clause.clear();
187  1 clause.push(-1);
188  1 clause.push(-2);
189  1 clause.push(-3);
190  1 solver.addClause(clause);
191  1 assertTrue(solver.isSatisfiable());
192  1 IVecInt cube = new VecInt();
193  1 cube.push(1);
194  1 assertTrue(solver.isSatisfiable(cube));
195  1 printModel(solver.model());
196  1 cube.push(2);
197  1 assertEquals(2, cube.size());
198  1 assertTrue(solver.isSatisfiable(cube));
199  1 printModel(solver.model());
200  1 cube.push(-3);
201  1 assertEquals(3, cube.size());
202  1 assertTrue(solver.isSatisfiable(cube));
203  1 printModel(solver.model());
204  1 cube.pop();
205  1 cube.push(3);
206  1 assertEquals(3, cube.size());
207  1 System.out.println(" cube " + cube);
208  1 boolean sat = solver.isSatisfiable(cube);
209  1 if (sat) {
210  0 printModel(solver.model());
211    }
212  1 assertFalse(sat);
213    } catch (ContradictionException e) {
214  0 fail();
215    } catch (TimeoutException e) {
216  0 fail();
217    }
218    }
219   
 
220  3 toggle private void printModel(int[] model) {
221  12 for (int i = 0; i < model.length; i++) {
222  9 System.out.print(model[i] + " ");
223    }
224  3 System.out.println();
225    }
226    }
 
CloverReport generated by Clover Code Coverage v2.0a5
mer. juin 27 2007 07:27:33 CEST.		   Beta Testers License registered to clover-support@cenqua.com. This license of Clover2 is provided for beta testing only. You have 5 day(s) before your Beta Tester License expires.