Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
187   517   41   11,69
12   370   0,3   8
16     3,5  
2    
 
  GoodOPBReaderTest       Line # 33 185 41 82% 0.8199052
  ReturnCounterStub       Line # 507 2 1 50% 0.5
 
  (12)
 
1    /*
2    * Created on 8 sept. 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.minisat.reader;
8   
9    import java.io.IOException;
10    import java.io.LineNumberReader;
11    import java.io.StringReader;
12    import java.math.BigInteger;
13   
14    import org.jmock.Mock;
15    import org.jmock.MockObjectTestCase;
16    import org.jmock.core.Invocation;
17    import org.jmock.core.Stub;
18    import org.sat4j.core.Vec;
19    import org.sat4j.core.VecInt;
20    import org.sat4j.reader.GoodOPBReader;
21    import org.sat4j.reader.ParseFormatException;
22    import org.sat4j.specs.ContradictionException;
23    import org.sat4j.specs.ISolver;
24    import org.sat4j.specs.IVec;
25    import org.sat4j.specs.IVecInt;
26   
27    /**
28    * @author leberre
29    *
30    * To change the template for this generated type comment go to Window -
31    * Preferences - Java - Code Generation - Code and Comments
32    */
 
33    public class GoodOPBReaderTest extends MockObjectTestCase {
34   
35    /**
36    * @param arg0
37    */
 
38  12 toggle public GoodOPBReaderTest(String arg0) {
39  12 super(arg0);
40    // TODO Auto-generated constructor stub
41    }
42   
 
43  1 toggle public void testParseResetSolverBeforeParsing() {
44    // expectations
45  1 mockSolver.expects(once()).method("reset");
46   
47  1 try {
48  1 String test = "";
49   
50    // execute
51  1 parser.parseInstance(new LineNumberReader(new StringReader(test))); // verify
52  1 mockSolver.verify();
53   
54    } catch (ContradictionException e) {
55  0 fail("Trivialy UNSAT");
56    } catch (IOException e) {
57  0 fail("I/O Error");
58    } catch (ParseFormatException e) {
59  0 fail("Parsing Error");
60    }
61    }
62   
 
63  1 toggle public void testIgnoreCommentedLines() {
64    // expectations
65  1 mockSolver.expects(once()).method("reset");
66  1 mockSolver.expects(once()).method("addPseudoBoolean");
67  1 mockSolver.expects(atLeastOnce()).method("newVar").will(
68    onConsecutiveCalls(returnValue(1), returnValue(2),
69    returnValue(3), returnValue(4)));
70  1 try {
71  1 String test = "* Comment \n -V2 V3 V4 >= 12";
72   
73    // execute
74  1 parser.parseInstance(new LineNumberReader(new StringReader(test)));
75    // verify
76  1 mockSolver.verify();
77   
78    } catch (ContradictionException e) {
79  0 fail("Trivialy UNSAT");
80    } catch (IOException e) {
81  0 fail("I/O Error");
82    } catch (ParseFormatException e) {
83  0 fail("Parsing Error");
84    }
85    }
86   
 
87  1 toggle public void testSkipMinObjectiveFunction() {
88    // expectations
89  1 mockSolver.expects(once()).method("reset");
90  1 mockSolver.expects(once()).method("addPseudoBoolean");
91  1 mockSolver.expects(atLeastOnce()).method("newVar").will(
92    onConsecutiveCalls(returnValue(1), returnValue(2),
93    returnValue(3), returnValue(4)));
94  1 try {
95  1 String test = "* Comment \n min : -V1 -V2 -V3 \n -V2 V3 V4 >= 12";
96   
97    // execute
98  1 parser.parseInstance(new LineNumberReader(new StringReader(test)));
99    // verify
100  1 mockSolver.verify();
101   
102    } catch (ContradictionException e) {
103  0 fail("Trivialy UNSAT");
104    } catch (IOException e) {
105  0 fail("I/O Error");
106    } catch (ParseFormatException e) {
107  0 fail("Parsing Error");
108    }
109    }
110   
 
111  1 toggle public void testSkipMaxObjectiveFunction() {
112   
113    // expectations
114  1 IVecInt expectedLits = new VecInt();
115  1 expectedLits.push(-1);
116  1 expectedLits.push(2);
117  1 expectedLits.push(3);
118  1 IVec<BigInteger> expectedCoeffs = new Vec<BigInteger>(3, BigInteger.ONE);
119   
120    // expectations
121  1 mockSolver.expects(once()).method("reset");
122  1 mockSolver.expects(once()).method("addPseudoBoolean").with(
123    eq(expectedLits), eq(expectedCoeffs), eq(true),
124    eq(BigInteger.valueOf(12)));
125  1 mockSolver.expects(atLeastOnce()).method("newVar").will(
126    onConsecutiveCalls(returnValue(1), returnValue(2),
127    returnValue(3), returnValue(4)));
128   
129  1 try {
130  1 String test = "* Comment \n max : ~V1 ~V2 ~V3 \n ~V2 V3 V4 >= 12";
131    // execute
132  1 parser.parseInstance(new LineNumberReader(new StringReader(test)));
133    // verify
134  1 mockSolver.verify();
135   
136    } catch (ContradictionException e) {
137  0 fail("Trivialy UNSAT");
138    } catch (IOException e) {
139  0 fail("I/O Error");
140    } catch (ParseFormatException e) {
141  0 fail("Parsing Error");
142    }
143    }
144   
 
145  1 toggle public void testSkipConstraintName() {
146   
147    // expectations
148  1 IVecInt expectedLits = new VecInt();
149  1 expectedLits.push(-1);
150  1 expectedLits.push(2);
151  1 expectedLits.push(3);
152  1 IVec<BigInteger> expectedCoeffs = new Vec<BigInteger>(3, BigInteger.ONE);
153   
154    // expectations
155  1 mockSolver.expects(once()).method("reset");
156  1 mockSolver.expects(once()).method("addPseudoBoolean").with(
157    eq(expectedLits), eq(expectedCoeffs), eq(true),
158    eq(BigInteger.valueOf(12)));
159  1 mockSolver.expects(atLeastOnce()).method("newVar").will(
160    onConsecutiveCalls(returnValue(1), returnValue(2),
161    returnValue(3), returnValue(4)));
162   
163  1 try {
164  1 String test = "* Comment \n max : ~V1 ~V2 ~V3 \n C1 : ~V2 V3 V4 >= 12";
165    // execute
166  1 parser.parseInstance(new LineNumberReader(new StringReader(test)));
167    // verify
168  1 mockSolver.verify();
169   
170    } catch (ContradictionException e) {
171  0 fail("Trivialy UNSAT");
172    } catch (IOException e) {
173  0 fail("I/O Error");
174    } catch (ParseFormatException e) {
175  0 fail("Parsing Error");
176    }
177    }
178   
 
179  1 toggle public void testReadCardinalityConstraints() {
180   
181  1 IVecInt expectedLits = new VecInt();
182  1 expectedLits.push(-1);
183  1 expectedLits.push(2);
184  1 expectedLits.push(3);
185   
186  1 IVecInt expectedLits2 = new VecInt();
187  1 expectedLits2.push(1);
188  1 expectedLits2.push(3);
189  1 expectedLits2.push(4);
190  1 IVec<BigInteger> expectedCoeffs = new Vec<BigInteger>(3, BigInteger.ONE);
191   
192    // expectations
193  1 mockSolver.expects(once()).method("reset");
194  1 mockSolver.expects(once()).method("addPseudoBoolean").with(
195    eq(expectedLits), eq(expectedCoeffs), eq(true),
196    eq(BigInteger.valueOf(12))).id("first");
197   
198  1 mockSolver.expects(once()).method("addPseudoBoolean").with(
199    eq(expectedLits2), eq(expectedCoeffs), eq(true),
200    eq(BigInteger.valueOf(34))).after("first");
201  1 mockSolver.expects(atLeastOnce()).method("newVar").will(
202    onConsecutiveCalls(returnValue(1), returnValue(2),
203    returnValue(3), returnValue(4)));
204  1 try {
205  1 String test = "* Comment \n ~V2 V3 V4 >= 12 \n V2 +V4 V6 >= 34";
206   
207    // execute
208  1 parser.parseInstance(new LineNumberReader(new StringReader(test)));
209    // verify
210  1 mockSolver.verify();
211   
212    } catch (ContradictionException e) {
213  0 fail("Trivialy UNSAT");
214    } catch (IOException e) {
215  0 fail("I/O Error");
216    } catch (ParseFormatException e) {
217  0 fail("Parsing Error");
218    }
219    }
220   
 
221  1 toggle public void testReadProblematicCardinalityConstraints() {
222   
223  1 IVecInt expectedLits = new VecInt().push(-1).push(2).push(3);
224   
225  1 IVecInt expectedLits2 = new VecInt().push(1).push(-3).push(4);
226   
227  1 IVec<BigInteger> expectedCoeffs = new Vec<BigInteger>(3, BigInteger.ONE);
228   
229    // expectations
230  1 mockSolver.expects(once()).method("reset");
231  1 mockSolver.expects(once()).method("addPseudoBoolean").with(
232    eq(expectedLits), eq(expectedCoeffs), eq(true),
233    eq(BigInteger.valueOf(12))).id("first");
234   
235  1 mockSolver.expects(once()).method("addPseudoBoolean").with(
236    eq(expectedLits2), eq(expectedCoeffs), eq(true),
237    eq(BigInteger.valueOf(34))).after("first");
238  1 mockSolver.expects(atLeastOnce()).method("newVar").will(
239    onConsecutiveCalls(returnValue(1), returnValue(2),
240    returnValue(3), returnValue(4)));
241  1 try {
242  1 String test = "* Comment \n ~ V2 + V3 + V4 >= 12 \n V2 + ~V4 + V6 >= 34";
243   
244    // execute
245  1 parser.parseInstance(new LineNumberReader(new StringReader(test)));
246    // verify
247  1 mockSolver.verify();
248   
249    } catch (ContradictionException e) {
250  0 fail("Trivialy UNSAT");
251    } catch (IOException e) {
252  0 fail("I/O Error");
253    } catch (ParseFormatException e) {
254  0 fail("Parsing Error");
255    }
256    }
257   
 
258  1 toggle public void testReadPBConstraints() {
259   
260  1 IVecInt expectedLits = new VecInt().push(1).push(2);
261  1 expectedLits.push(3);
262  1 IVec<BigInteger> expectedCoeffs = new Vec<BigInteger>();
263  1 expectedCoeffs.push(BigInteger.valueOf(32));
264  1 expectedCoeffs.push(BigInteger.valueOf(-64));
265  1 expectedCoeffs.push(BigInteger.valueOf(-123456));
266   
267  1 IVecInt expectedLits2 = new VecInt().push(1).push(3).push(4);
268  1 IVec<BigInteger> expectedCoeffs2 = new Vec<BigInteger>(3,
269    BigInteger.ONE);
270   
271    // expectations
272  1 mockSolver.expects(once()).method("reset");
273  1 mockSolver.expects(once()).method("addPseudoBoolean").with(
274    eq(expectedLits), eq(expectedCoeffs), eq(true),
275    eq(BigInteger.valueOf(12))).id("first");
276   
277  1 mockSolver.expects(once()).method("addPseudoBoolean").with(
278    eq(expectedLits2), eq(expectedCoeffs2), eq(true),
279    eq(BigInteger.valueOf(34))).after("first");
280  1 mockSolver.expects(atLeastOnce()).method("newVar").will(
281    onConsecutiveCalls(returnValue(1), returnValue(2),
282    returnValue(3), returnValue(4)));
283  1 try {
284  1 String test = "* Comment \n 32 V2 -64 V3 -123456 V4 >= 12 \n V2 +V4 V6 >= 34";
285   
286    // execute
287  1 parser.parseInstance(new LineNumberReader(new StringReader(test)));
288    // verify
289  1 mockSolver.verify();
290   
291    } catch (ContradictionException e) {
292  0 fail("Trivialy UNSAT");
293    } catch (IOException e) {
294  0 fail("I/O Error");
295    } catch (ParseFormatException e) {
296  0 fail("Parsing Error");
297    }
298    }
299   
 
300  1 toggle public void testReadProblematicPBConstraints() {
301   
302  1 IVecInt expectedLits = new VecInt().push(-1).push(2);
303  1 expectedLits.push(3);
304  1 IVec<BigInteger> expectedCoeffs = new Vec<BigInteger>().push(
305    BigInteger.valueOf(32)).push(BigInteger.valueOf(-64)).push(
306    BigInteger.valueOf(-123456));
307   
308  1 IVecInt expectedLits2 = new VecInt().push(1).push(3).push(4);
309  1 IVec<BigInteger> expectedCoeffs2 = new Vec<BigInteger>(3,
310    BigInteger.ONE);
311   
312    // expectations
313  1 mockSolver.expects(once()).method("reset");
314  1 mockSolver.expects(once()).method("addPseudoBoolean").with(
315    eq(expectedLits), eq(expectedCoeffs), eq(true),
316    eq(BigInteger.valueOf(12))).id("first");
317   
318  1 mockSolver.expects(once()).method("addPseudoBoolean").with(
319    eq(expectedLits2), eq(expectedCoeffs2), eq(true),
320    eq(BigInteger.valueOf(34))).after("first");
321  1 mockSolver.expects(atLeastOnce()).method("newVar").will(
322    onConsecutiveCalls(returnValue(1), returnValue(2),
323    returnValue(3), returnValue(4)));
324  1 try {
325  1 String test = "* Comment \n 32 ~ V2 -64 V3 -123456 V4 >= 12 \n + V2 +V4 + V6 >= 34";
326   
327    // execute
328  1 parser.parseInstance(new LineNumberReader(new StringReader(test)));
329    // verify
330  1 mockSolver.verify();
331   
332    } catch (ContradictionException e) {
333  0 fail("Trivialy UNSAT");
334    } catch (IOException e) {
335  0 fail("I/O Error");
336    } catch (ParseFormatException e) {
337  0 fail("Parsing Error");
338    }
339    }
340   
 
341  1 toggle public void testDiscardTrailingComma() {
342   
343  1 IVecInt expectedLits = new VecInt().push(-1).push(2);
344  1 expectedLits.push(3);
345  1 IVec<BigInteger> expectedCoeffs = new Vec<BigInteger>().push(
346    BigInteger.valueOf(32)).push(BigInteger.valueOf(-64)).push(
347    BigInteger.valueOf(-123456));
348   
349  1 IVecInt expectedLits2 = new VecInt().push(1).push(3).push(4);
350  1 IVec<BigInteger> expectedCoeffs2 = new Vec<BigInteger>(3,
351    BigInteger.ONE);
352   
353    // expectations
354  1 mockSolver.expects(once()).method("reset");
355  1 mockSolver.expects(once()).method("addPseudoBoolean").with(
356    eq(expectedLits), eq(expectedCoeffs), eq(true),
357    eq(BigInteger.valueOf(12))).id("first");
358   
359  1 mockSolver.expects(once()).method("addPseudoBoolean").with(
360    eq(expectedLits2), eq(expectedCoeffs2), eq(true),
361    eq(BigInteger.valueOf(34))).after("first");
362  1 mockSolver.expects(atLeastOnce()).method("newVar").will(
363    onConsecutiveCalls(returnValue(1), returnValue(2),
364    returnValue(3), returnValue(4)));
365  1 try {
366  1 String test = "* Comment \n 32 ~ V2 -64 V3 -123456 V4 >= 12; \n + V2 +V4 + V6 >= 34 ;";
367   
368    // execute
369  1 parser.parseInstance(new LineNumberReader(new StringReader(test)));
370    // verify
371  1 mockSolver.verify();
372   
373    } catch (ContradictionException e) {
374  0 fail("Trivialy UNSAT");
375    } catch (IOException e) {
376  0 fail("I/O Error");
377    } catch (ParseFormatException e) {
378  0 fail("Parsing Error");
379    }
380    }
381   
 
382  1 toggle public void testProblemWithLeadingPlus() {
383   
384  1 IVecInt expectedLits = new VecInt().push(-1).push(2);
385  1 expectedLits.push(3);
386  1 IVec<BigInteger> expectedCoeffs = new Vec<BigInteger>().push(
387    BigInteger.valueOf(32)).push(BigInteger.valueOf(-64)).push(
388    BigInteger.valueOf(-123456));
389   
390  1 IVecInt expectedLits2 = new VecInt().push(1).push(3).push(4);
391  1 IVec<BigInteger> expectedCoeffs2 = new Vec<BigInteger>(3,
392    BigInteger.ONE);
393   
394    // expectations
395  1 mockSolver.expects(once()).method("reset");
396  1 mockSolver.expects(once()).method("addPseudoBoolean").with(
397    eq(expectedLits), eq(expectedCoeffs), eq(true),
398    eq(BigInteger.valueOf(12))).id("first");
399   
400  1 mockSolver.expects(once()).method("addPseudoBoolean").with(
401    eq(expectedLits2), eq(expectedCoeffs2), eq(true),
402    eq(BigInteger.valueOf(34))).after("first");
403  1 mockSolver.expects(atLeastOnce()).method("newVar").will(
404    onConsecutiveCalls(returnValue(1), returnValue(2),
405    returnValue(3), returnValue(4)));
406  1 try {
407  1 String test = "* Comment \n +32 ~ V2 -64 V3 -123456 V4 >= 12; \n + V2 +V4 + V6 >= 34 ;";
408   
409    // execute
410  1 parser.parseInstance(new LineNumberReader(new StringReader(test)));
411    // verify
412  1 mockSolver.verify();
413   
414    } catch (ContradictionException e) {
415  0 fail("Trivialy UNSAT");
416    } catch (IOException e) {
417  0 fail("I/O Error");
418    } catch (ParseFormatException e) {
419  0 fail("Parsing Error");
420    }
421    }
422   
 
423  1 toggle public void testEnigmaProblem() {
424   
425    // create literals
426  1 IVecInt expectedLits = new VecInt();
427  91 for (int i = 1; i <= 90; i++) {
428  90 expectedLits.push(i);
429    }
430    // create coeffs
431  1 IVec<BigInteger> expectedCoeffs = new Vec<BigInteger>();
432  1 BigInteger sum = BigInteger.ZERO;
433  1 BigInteger coef;
434  1 int[] values = { 202, -79, 100023, -89810, -9980, 1000, 100, 10000,
435    100, -1 };
436   
437  11 for (int j = 0; j < values.length; j++) {
438  100 for (int i = 1; i <= 9; i++) {
439  90 expectedCoeffs.push(coef = BigInteger.valueOf(values[j] * i));
440  90 if (coef.signum() > 0) {
441  54 sum = sum.add(coef);
442    }
443    }
444    }
445   
446  1 assert expectedLits.size() == expectedCoeffs.size();
447  1 assert expectedCoeffs.last().equals(BigInteger.valueOf(-9));
448   
449    // expectations
450  1 mockSolver.expects(once()).method("reset");
451  1 mockSolver.expects(once()).method("addPseudoBoolean").with(
452    eq(expectedLits), eq(expectedCoeffs), eq(true),
453    eq(BigInteger.ZERO)).id("first");
454   
455  1 mockSolver.expects(once()).method("addPseudoBoolean").with(
456    eq(expectedLits), eq(expectedCoeffs), eq(false),
457    eq(BigInteger.ZERO)).after("first");
458  1 mockSolver.expects(atLeastOnce()).method("newVar").will(
459    new ReturnCounterStub());
460  1 try {
461   
462  1 String test = "BILANCIO: +202 A1 +404 A2 +606 A3 +808 A4 +1010 A5 +1212 A6 +1414 A7 +1616 A8 +1818 A9 "
463    + "-79 B1 -158 B2 -237 B3 -316 B4 -395 B5 -474 B6 -553 B7 -632 B8 -711 B9 "
464    + " +100023 C1 +200046 C2 +300069 C3 +400092 C4 +500115 C5 +600138 C6 +700161 C7 +800184 C8 +900207 C9 "
465    + " -89810 D1 -179620 D2 -269430 D3 -359240 D4 -449050 D5 -538860 D6 -628670 D7 -718480 D8 -808290 D9 "
466    + " -9980 E1 -19960 E2 -29940 E3 -39920 E4 -49900 E5 -59880 E6 -69860 E7 -79840 E8 -89820 E9 "
467    + " +1000 F1 +2000 F2 +3000 F3 +4000 F4 +5000 F5 +6000 F6 +7000 F7 +8000 F8 +9000 F9 "
468    + " +100 G1 +200 G2 +300 G3 +400 G4 +500 G5 +600 G6 +700 G7 +800 G8 +900 G9 "
469    + " +10000 H1 +20000 H2 +30000 H3 +40000 H4 +50000 H5 +60000 H6 +70000 H7 +80000 H8 +90000 H9 "
470    + " +100 I1 +200 I2 +300 I3 +400 I4 +500 I5 +600 I6 +700 I7 +800 I8 +900 I9 "
471    + " -L1 -2 L2 -3 L3 -4 L4 -5 L5 -6 L6 -7 L7 -8 L8 -9 L9 = 0";
472    // ;
473    // String test = "* Comment \n +32 - V2 -64 V3 -123456 V4 >= 12; \n
474    // + V2 +V4 + V6 >= 34 ;";
475   
476    // execute
477  1 parser.parseInstance(new LineNumberReader(new StringReader(test)));
478    // verify
479  1 mockSolver.verify();
480   
481    } catch (ContradictionException e) {
482  0 fail("Trivialy UNSAT");
483    } catch (IOException e) {
484  0 fail("I/O Error");
485    } catch (ParseFormatException e) {
486  0 fail("Parsing Error");
487    }
488    }
489   
490    /*
491    * (non-Javadoc)
492    *
493    * @see junit.framework.TestCase#setUp()
494    */
 
495  12 toggle @Override
496    protected void setUp() throws Exception {
497  12 mockSolver = new Mock(ISolver.class);
498  12 parser = new GoodOPBReader((ISolver) mockSolver.proxy());
499   
500    }
501   
502    private Mock mockSolver;
503   
504    private GoodOPBReader parser;
505    }
506   
 
507    class ReturnCounterStub implements Stub {
508    private int counter = 1;
509   
 
510  0 toggle public StringBuffer describeTo(StringBuffer buffer) {
511  0 return buffer.append("return <" + counter + "> ");
512    }
513   
 
514  90 toggle public Object invoke(Invocation invocation) throws Throwable {
515  90 return new Integer(counter++);
516    }
517    }
 
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.