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