Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
31   87   3   7,75
0   58   0,19   4
4     1,5  
1    
 
  WatchedPBConstrWithPBConstrLearningOnCNFTest       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 WatchedPBConstrWithPBConstrLearningOnCNFTest extends
29    AbstractM2Test {
30   
31    /**
32    * @param arg0
33    */
 
34  103 toggle public WatchedPBConstrWithPBConstrLearningOnCNFTest(String arg0) {
35  103 super(arg0);
36    }
37   
38    /**
39    * @see TestCase#setUp()
40    */
 
41  103 toggle @Override
42    protected ISolver createSolver() {
43  103 return SolverFactory.newMiniOPBMin();
44    }
45   
 
46  1 toggle public void testPropagation() {
47  1 solver.newVar(3);
48  1 IVecInt lits = new VecInt();
49  1 lits.push(1);
50  1 lits.push(2);
51  1 lits.push(3);
52  1 IVec<BigInteger> coefs = new Vec<BigInteger>();
53  1 coefs.growTo(lits.size(), BigInteger.ONE);
54  1 Solver<ILits> mysolver = (Solver<ILits>) solver;
55  1 try {
56  1 mysolver.addPseudoBoolean(lits, coefs, true, BigInteger.ONE);
57  1 mysolver.assume(3); // assume -1
58  1 assertNull(mysolver.propagate());
59  1 assertTrue(mysolver.getVocabulary().isSatisfied(3));
60  1 mysolver.assume(5); // assume -2
61  1 assertNull(mysolver.propagate());
62  1 assertTrue(mysolver.getVocabulary().isSatisfied(5));
63  1 assertTrue(mysolver.getVocabulary().isSatisfied(6));
64    } catch (ContradictionException e) {
65  0 e.printStackTrace();
66  0 fail();
67    }
68   
69    }
70   
 
71  1 toggle public void testPropagation2() {
72  1 solver.newVar(3);
73  1 IVecInt lits = new VecInt();
74  1 lits.push(1);
75  1 lits.push(2);
76  1 lits.push(3);
77  1 IVec<BigInteger> coefs = new Vec<BigInteger>();
78  1 coefs.growTo(lits.size(), BigInteger.ONE);
79  1 try {
80  1 solver.addPseudoBoolean(lits, coefs, true, BigInteger.valueOf(4));
81  0 fail();
82    } catch (ContradictionException e) {
83    // everything is fine here.
84    }
85    }
86   
87    }
 
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.