Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
14   52   2   4,67
6   34   0,29   3
3     1,33  
1    
 
  ConflictMapMerging       Line # 9 14 2 65,2% 0.65217394
 
No Tests
 
1    package org.sat4j.minisat.constraints.pb;
2   
3    import java.math.BigInteger;
4    import java.util.HashMap;
5    import java.util.Map;
6   
7    import org.sat4j.minisat.core.ILits;
8   
 
9    public class ConflictMapMerging extends ConflictMap {
10   
 
11  76761 toggle public ConflictMapMerging(Map<Integer, BigInteger> m, BigInteger d, ILits voc,
12    int level) {
13  76761 super(m, d, voc, level);
14    }
 
15  76761 toggle public static IConflict createConflict(PBConstr cpb, int level) {
16  76761 Map<Integer, BigInteger> m = new HashMap<Integer, BigInteger>();
17  76761 int lit;
18  76761 BigInteger coefLit;
19  1613002 for (int i = 0; i < cpb.size(); i++) {
20  1536241 lit = cpb.get(i);
21  1536241 coefLit = cpb.getCoef(i);
22  1536241 assert cpb.get(i) != 0;
23  1536241 assert cpb.getCoef(i).signum() > 0;
24  1536241 m.put(lit, coefLit);
25    }
26  76761 return new ConflictMapMerging(m, cpb.getDegree(), cpb.getVocabulary(),
27    level);
28    }
29   
30    /**
31    * reduces the constraint defined by wpb until the result of the cutting
32    * plane is a conflict. this reduction returns a clause.
33    *
34    * @param litImplied
35    * @param ind
36    * @param reducedCoefs
37    * @param wpb
38    * @return
39    */
 
40  0 toggle @Override
41    protected BigInteger reduceUntilConflict(int litImplied, int ind,
42    BigInteger[] reducedCoefs, WatchPb wpb) {
43  0 BigInteger tmp = reducedCoefs[ind].subtract(BigInteger.ONE);
44  0 reducedCoefs[ind] = BigInteger.ONE;
45  0 coefMultCons = coefs.get(litImplied ^ 1);
46  0 coefMult = BigInteger.ONE;
47  0 return saturation(reducedCoefs,wpb.getDegree().subtract(tmp));
48    }
49   
50   
51   
52    }