Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
98   236   10   8,91
4   151   0,2   11
11     1,82  
1    
 
  TestAtMost       Line # 13 98 10 0% 0.0
 
No Tests
 
1    package org.sat4j.minisat.datatype;
2   
3    import junit.framework.TestCase;
4   
5    import org.sat4j.core.VecInt;
6    import org.sat4j.minisat.SolverFactory;
7    import org.sat4j.reader.InstanceReader;
8    import org.sat4j.specs.ContradictionException;
9    import org.sat4j.specs.ISolver;
10    import org.sat4j.specs.IVecInt;
11    import org.sat4j.specs.TimeoutException;
12   
 
13    public class TestAtMost extends TestCase {
14   
15    private static final String PREFIX = System.getProperty("test.prefix");
16   
17    private ISolver solver;
18   
19    private InstanceReader reader;
20   
 
21  0 toggle public TestAtMost(String s) {
22  0 super(s);
23    }
24   
 
25  0 toggle @Override
26    protected void setUp() {
27  0 solver = SolverFactory.newMiniSAT();
28  0 reader = new InstanceReader(solver);
29    }
30   
 
31  0 toggle public void testUnEssaiSat() throws TimeoutException {
32  0 try {
33  0 solver.reset();
34    // 3 variables
35  0 solver.newVar(3);
36    // premi?re contrainte de cardinalit?
37    // a V b V c >= 2
38  0 IVecInt vec = new VecInt();
39  0 vec.push(1);
40  0 vec.push(2);
41  0 vec.push(3);
42  0 solver.addAtLeast(vec, 2);
43   
44    // Deuxi?me contrainte de cardinalit?
45    // a V non b >= 2
46  0 vec = new VecInt();
47  0 vec.push(1);
48  0 vec.push(-2);
49  0 solver.addAtLeast(vec, 2);
50   
51  0 boolean isSat = solver.isSatisfiable();
52   
53  0 assertTrue(isSat);
54    } catch (ContradictionException e) {
55  0 assertTrue(false);
56    }
57    }
58   
59    /**
60    * @param isSat
61    */
 
62  0 toggle private void affichageResultat(boolean isSat) {
63  0 if (isSat) {
64  0 System.out.println("s SATISFIABLE");
65  0 int[] model = solver.model();
66  0 StringBuffer stb = new StringBuffer();
67  0 stb.append("v ");
68  0 for (int i = 0; i < model.length; i++) {
69  0 stb.append(model[i]);
70  0 stb.append(" ");
71    }
72  0 stb.append(" 0");
73  0 System.out.println(stb);
74    } else
75  0 System.out.println("s UNSATISFIABLE");
76    }
77   
 
78  0 toggle public void testUnEssaiUnsat() throws TimeoutException {
79  0 try {
80  0 solver.reset();
81    // 2 variables
82  0 solver.newVar(2);
83    // premi?re contrainte de cardinalit?
84    // a + not b >= 1
85  0 IVecInt vecLit = new VecInt();
86  0 vecLit.push(1);
87  0 vecLit.push(-2);
88  0 solver.addAtLeast(vecLit, 1);
89   
90    // Deuxi?me contrainte de cardinalit?
91    // not a >= 1
92  0 vecLit = new VecInt();
93  0 vecLit.push(-1);
94  0 solver.addAtLeast(vecLit, 1);
95   
96    // Troisi?me contrainte de cardinalit?
97    // b >= 1
98  0 vecLit = new VecInt();
99  0 vecLit.push(2);
100  0 solver.addAtLeast(vecLit, 1);
101   
102  0 boolean isSat = solver.isSatisfiable();
103   
104  0 assertFalse(isSat);
105    } catch (ContradictionException e) {
106  0 assertTrue(false);
107    }
108   
109    }
110   
 
111  0 toggle public void test2Sat() throws TimeoutException {
112  0 try {
113  0 solver.reset();
114    // 2 variables
115  0 solver.newVar(2);
116    // premi?re contrainte de cardinalit?
117    // a + not b <=3
118  0 IVecInt vecLit = new VecInt();
119  0 vecLit.push(1);
120  0 vecLit.push(-2);
121  0 solver.addAtMost(vecLit, 3);
122   
123  0 boolean isSat = solver.isSatisfiable();
124   
125  0 assertTrue(isSat);
126    } catch (ContradictionException e) {
127  0 assertTrue(false);
128    }
129    }
130   
 
131  0 toggle public void test4Unsat() throws TimeoutException {
132  0 try {
133  0 solver.reset();
134    // 2 variables
135  0 solver.newVar(2);
136    // premi?re contrainte de cardinalit?
137    // a + not b >=3
138  0 IVecInt vecLit = new VecInt();
139  0 vecLit.push(1);
140  0 vecLit.push(-2);
141   
142  0 solver.addAtLeast(vecLit, 3);
143   
144  0 solver.isSatisfiable();
145   
146  0 fail();
147    } catch (ContradictionException e) {
148    }
149    }
150   
 
151  0 toggle public void test3Unsat() throws TimeoutException {
152  0 try {
153  0 solver.reset();
154    // 2 variables
155  0 solver.newVar(2);
156    // contrainte de cardinalit?
157    // a >= 1
158  0 IVecInt vecLit = new VecInt();
159  0 vecLit.push(1);
160  0 solver.addAtLeast(vecLit, 1);
161    // contrainte de cardinalit?
162    // b >= 1
163  0 vecLit = new VecInt();
164  0 vecLit.push(2);
165  0 solver.addAtLeast(vecLit, 1);
166    // contrainte de cardinalit?
167    // a + b <=1
168  0 vecLit = new VecInt();
169  0 vecLit.push(1);
170  0 vecLit.push(2);
171  0 solver.addAtMost(vecLit, 1);
172   
173  0 solver.isSatisfiable();
174   
175  0 fail();
176    } catch (ContradictionException e) {
177    }
178   
179    }
180   
 
181  0 toggle public void test5Sat() throws TimeoutException {
182  0 try {
183  0 solver.reset();
184    // 2 variables
185  0 solver.newVar(2);
186    // premi\x{FFFD}re contrainte de cardinalit\x{FFFD}
187    // a + not b <=0
188  0 IVecInt vecLit = new VecInt();
189  0 vecLit.push(1);
190  0 vecLit.push(-2);
191   
192  0 solver.addAtMost(vecLit, 0);
193   
194  0 boolean isSat = solver.isSatisfiable();
195   
196  0 assertTrue(isSat);
197    } catch (ContradictionException e) {
198  0 assertTrue(false);
199    }
200    }
201   
202    // public void testRadar1() throws TimeoutException {
203    // solver.reset();
204    // try {
205    // URL url = DimacsReader.class
206    // .getResource("benchs/10_10_4.5_0.95_100.dimacs");
207    // System.out.println(url);
208    //
209    // solver.parseInstance(url.getFile());
210    // } catch (Exception e) {
211    // System.out.println(e.getMessage());
212    // e.printStackTrace();
213    // fail();
214    // }
215    // System.out.println("fin Radar 1");
216    // assertTrue(solver.isSatisfiable());
217    // }
218   
 
219  0 toggle public void testDimacs1() throws TimeoutException {
220  0 solver.reset();
221  0 try {
222  0 reader.parseInstance(PREFIX + "test1bis.dimacs");
223    } catch (Exception e) {
224  0 System.out.println(e.getMessage());
225  0 e.printStackTrace();
226  0 fail();
227    }
228  0 System.out.println("fin Dimacs 1");
229  0 assertTrue(solver.isSatisfiable());
230    }
231   
 
232  0 toggle public static void main(String[] args) {
233  0 junit.swingui.TestRunner.run(TestAtMost.class);
234    } // main
235   
236    } // TestAtMost
 
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.