Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
138   271   22   9,2
0   222   0,26   15
15     2,4  
1    
 
  TestsFonctionnels       Line # 30 138 22 0% 0.0
 
No Tests
 
1    package org.sat4j.minisat;
2   
3    import java.io.IOException;
4   
5    import junit.framework.TestCase;
6   
7    import org.sat4j.core.VecInt;
8    import org.sat4j.minisat.core.ILits;
9    import org.sat4j.minisat.core.Solver;
10    import org.sat4j.reader.InstanceReader;
11    import org.sat4j.reader.ParseFormatException;
12    import org.sat4j.specs.ContradictionException;
13    import org.sat4j.specs.IConstr;
14    import org.sat4j.specs.ISolver;
15    import org.sat4j.specs.IVecInt;
16    import org.sat4j.specs.TimeoutException;
17   
18    /*
19    * Created on 11 nov. 2003
20    *
21    * To change the template for this generated file go to
22    * Window>Preferences>Java>Code Generation>Code and Comments
23    */
24    /**
25    * @author leberre
26    *
27    * To change the template for this generated type comment go to
28    * Window>Preferences>Java>Code Generation>Code and Comments
29    */
 
30    public class TestsFonctionnels extends TestCase {
31   
32    private static final String PREFIX = System.getProperty("test.prefix");
33   
34    /**
35    * Constructor for TestsFonctionnels.
36    *
37    * @param arg0
38    */
 
39  0 toggle public TestsFonctionnels(String arg0) {
40  0 super(arg0);
41    }
42   
 
43  0 toggle public void testSat() {
44  0 try {
45  0 reader.parseInstance(PREFIX + "aim-50-yes-ok.cnf");
46  0 assertTrue(solver.isSatisfiable());
47    } catch (TimeoutException e) {
48  0 fail();
49    } catch (Exception e) {
50  0 fail();
51    }
52    }
53   
 
54  0 toggle public void testUnsat() throws TimeoutException {
55  0 try {
56  0 reader.parseInstance(PREFIX + "aim-50-no-ok.cnf");
57  0 assertFalse(solver.isSatisfiable());
58    } catch (IOException e) {
59  0 fail();
60    } catch (ParseFormatException e) {
61  0 fail();
62    } catch (ContradictionException e) {
63    // OK
64    }
65    }
66   
 
67  0 toggle public void testTrivialUnsat() {
68  0 solver.newVar(1);
69  0 IVecInt vec = new VecInt();
70  0 solver.newVar();
71  0 solver.newVar();
72  0 vec.push(1);
73  0 try {
74  0 solver.addClause(vec);
75    } catch (ContradictionException e) {
76  0 fail();
77    }
78  0 vec.clear();
79  0 vec.push(-1);
80  0 try {
81  0 solver.addClause(vec);
82  0 fail();
83    } catch (ContradictionException e1) {
84    }
85    }
86   
 
87  0 toggle public void testTrivialSat() throws TimeoutException {
88  0 solver.reset();
89  0 solver.newVar(2);
90  0 try {
91  0 IVecInt vec = new VecInt();
92  0 vec.push(1);
93  0 solver.addClause(vec);
94  0 vec.clear();
95  0 vec.push(-2);
96  0 solver.addClause(vec);
97  0 assertTrue(solver.isSatisfiable());
98    } catch (ContradictionException e) {
99  0 fail();
100    }
101    }
102   
 
103  0 toggle public void testTrivialSatNewVar() throws TimeoutException {
104  0 try {
105  0 solver.newVar(0);
106  0 solver.newVar();
107  0 IVecInt vec = new VecInt();
108  0 vec.push(1);
109  0 solver.addClause(vec);
110  0 vec.clear();
111  0 solver.newVar();
112  0 vec.push(-2);
113  0 solver.addClause(vec);
114  0 assertTrue(solver.isSatisfiable());
115    } catch (ContradictionException e) {
116  0 fail();
117    }
118    }
119   
 
120  0 toggle public void testBug001() throws TimeoutException {
121  0 solver.reset();
122  0 try {
123  0 reader.parseInstance(PREFIX + "bug001.cnf");
124    } catch (Exception e) {
125  0 e.printStackTrace();
126  0 fail();
127    }
128  0 assertTrue(solver.isSatisfiable());
129    }
130   
 
131  0 toggle public void testTrivialInconsistentFormula() {
132  0 solver.reset();
133  0 try {
134  0 reader.parseInstance(PREFIX + "test3.dimacs");
135  0 assertFalse(solver.isSatisfiable());
136    } catch (ContradictionException e) {
137    // OK
138    } catch (Exception e) {
139  0 e.printStackTrace();
140  0 fail();
141    }
142    }
143   
 
144  0 toggle public void testCommentsInInstance() {
145  0 solver.reset();
146  0 try {
147  0 reader.parseInstance(PREFIX + "testcomments.cnf");
148  0 assertFalse(solver.isSatisfiable());
149    } catch (ContradictionException e) {
150    // OK
151    } catch (Exception e) {
152  0 e.printStackTrace();
153  0 fail();
154    }
155    }
156   
 
157  0 toggle public void testRemoveConstraints() throws TimeoutException {
158  0 try {
159  0 solver.newVar(3);
160  0 IVecInt vec = new VecInt();
161  0 vec.push(1).push(-2);
162  0 IConstr c = solver.addClause(vec);
163  0 assertNotNull(c);
164  0 vec.clear();
165  0 vec.push(-1).push(-2);
166  0 c = solver.addClause(vec);
167  0 assertNotNull(c);
168  0 vec.clear();
169  0 vec.push(-1).push(2);
170  0 solver.addClause(vec);
171    // assertNotNull(c);
172  0 vec.clear();
173  0 vec.push(1).push(2);
174  0 solver.addClause(vec);
175  0 assertEquals(4, solver.nConstraints());
176    // assertNotNull(c);
177  0 assertFalse(solver.isSatisfiable());
178  0 solver.removeConstr(c);
179  0 assertEquals(3, solver.nConstraints());
180  0 assertTrue(solver.isSatisfiable());
181  0 assertEquals(1, solver.model()[0]);
182  0 assertEquals(2, solver.model()[1]);
183  0 vec.clear();
184  0 vec.push(-1).push(-2);
185  0 try {
186  0 c = solver.addClause(vec);
187  0 assertNotNull(c);
188  0 assertEquals(4, solver.nConstraints());
189  0 assertFalse(solver.isSatisfiable());
190    } catch (ContradictionException ce) {
191    // its fine
192    }
193    } catch (ContradictionException e) {
194  0 fail();
195    }
196    }
197   
 
198  0 toggle public void testRemoveAtLeast() {
199  0 solver.newVar(3);
200  0 IVecInt c1 = new VecInt().push(1).push(2).push(3);
201  0 try {
202  0 solver.addClause(c1); // 4 12 14
203  0 assertEquals(1, solver.nConstraints());
204  0 assertEquals(3, c1.size());
205  0 IConstr atLeast = solver.addAtLeast(c1, 2);
206  0 assertEquals(2, solver.nConstraints());
207  0 solver.removeConstr(atLeast);
208  0 assertEquals(1, solver.nConstraints());
209    } catch (ContradictionException e) {
210  0 fail();
211    }
212    }
213   
 
214  0 toggle public void testIsImplied() {
215  0 Solver<ILits> mysolver = (Solver<ILits>) solver;
216  0 solver.newVar(3);
217  0 IVecInt c1 = new VecInt().push(1);
218  0 try {
219  0 mysolver.addClause(c1);
220  0 assertTrue("isImplied(1) ", mysolver.getVocabulary().isImplied(2));
221  0 assertFalse("isImplied(2) :", mysolver.getVocabulary().isImplied(4));
222  0 mysolver.propagate();
223  0 assertTrue("isImplied(1) ", mysolver.getVocabulary().isImplied(2));
224  0 assertFalse("isImplied(2) :", mysolver.getVocabulary().isImplied(4));
225    } catch (ContradictionException e) {
226  0 fail();
227    }
228    }
229   
 
230  0 toggle public void testIsImplied3() {
231  0 Solver<ILits> mysolver = (Solver<ILits>) solver;
232  0 mysolver.newVar(1);
233  0 IVecInt c1 = new VecInt().push(-1);
234  0 try {
235  0 mysolver.addClause(c1);
236  0 mysolver.propagate();
237    } catch (ContradictionException e) {
238  0 fail();
239    }
240  0 assertTrue("isImplied(1) ", mysolver.getVocabulary().isImplied(2));
241  0 assertFalse("isSatisfiedl(1)", mysolver.getVocabulary().isSatisfied(2));
242  0 assertTrue("isFalsified(1)", mysolver.getVocabulary().isFalsified(2));
243    }
244   
 
245  0 toggle public void testErrorMessageWhenNewVarNotCalled() {
246  0 Solver<ILits> mysolver = (Solver<ILits>) solver;
247  0 IVecInt c1 = new VecInt().push(-1);
248  0 try {
249  0 mysolver.addClause(c1);
250  0 mysolver.propagate();
251  0 fail();
252    } catch (RuntimeException e) {
253  0 System.err.append(e.getMessage());
254    } catch (ContradictionException e) {
255  0 fail();
256    }
257    }
258   
259    /*
260    * @see TestCase#setUp()
261    */
 
262  0 toggle @Override
263    protected void setUp() throws Exception {
264  0 solver = SolverFactory.newMiniSAT();
265  0 reader = new InstanceReader(solver);
266    }
267   
268    private ISolver solver;
269   
270    private InstanceReader reader;
271    }
 
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.