Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
31   86   3   7,75
0   57   0,19   4
4     1,5  
1    
 
  CounterPBConstrWithClauseLearningOnCNFTest       Line # 28 31 3 91,4% 0.9142857
 
  (2)
 
1    /*
2    * Created on 17 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.minisat;
8   
9    import java.math.BigInteger;
10   
11    import junit.framework.TestCase;
12   
13    import org.sat4j.core.Vec;
14    import org.sat4j.core.VecInt;
15    import org.sat4j.minisat.core.ILits;
16    import org.sat4j.minisat.core.Solver;
17    import org.sat4j.specs.ContradictionException;
18    import org.sat4j.specs.ISolver;
19    import org.sat4j.specs.IVec;
20    import org.sat4j.specs.IVecInt;
21   
22    /**
23    * @author leberre
24    *
25    * To change the template for this generated type comment go to Window -
26    * Preferences - Java - Code Generation - Code and Comments
27    */
 
28    public class CounterPBConstrWithClauseLearningOnCNFTest extends AbstractM2Test {
29   
30    /**
31    * @param arg0
32    */
 
33  103 toggle public CounterPBConstrWithClauseLearningOnCNFTest(String arg0) {
34  103 super(arg0);
35    }
36   
37    /**
38    * @see TestCase#setUp()
39    */
 
40  103 toggle @Override
41    protected ISolver createSolver() {
42  103 return SolverFactory.newMinimalOPBMax();
43    }
44   
 
45  1 toggle public void testPropagation() {
46  1 solver.newVar(3);
47  1 IVecInt lits = new VecInt();
48  1 lits.push(1);
49  1 lits.push(2);
50  1 lits.push(3);
51  1 IVec<BigInteger> coefs = new Vec<BigInteger>();
52  1 coefs.growTo(lits.size(), BigInteger.ONE);
53  1 Solver<ILits> mysolver = (Solver<ILits>) solver;
54  1 try {
55  1 mysolver.addPseudoBoolean(lits, coefs, true, BigInteger.ONE);
56  1 mysolver.assume(3); // assume -1
57  1 assertNull(mysolver.propagate());
58  1 assertTrue(mysolver.getVocabulary().isSatisfied(3));
59  1 mysolver.assume(5); // assume -2
60  1 assertNull(mysolver.propagate());
61  1 assertTrue(mysolver.getVocabulary().isSatisfied(5));
62  1 assertTrue(mysolver.getVocabulary().isSatisfied(6));
63    } catch (ContradictionException e) {
64  0 e.printStackTrace();
65  0 fail();
66    }
67   
68    }
69   
 
70  1 toggle public void testPropagation2() {
71  1 solver.newVar(3);
72  1 IVecInt lits = new VecInt();
73  1 lits.push(1);
74  1 lits.push(2);
75  1 lits.push(3);
76  1 IVec<BigInteger> coefs = new Vec<BigInteger>();
77  1 coefs.growTo(lits.size(), BigInteger.ONE);
78  1 try {
79  1 solver.addPseudoBoolean(lits, coefs, true, BigInteger.valueOf(4));
80  0 fail();
81    } catch (ContradictionException e) {
82    // everything is fine here.
83    }
84    }
85   
86    }
 
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.