| 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 |
|
|
|
|
|
| 65,2% |
Uncovered Elements: 8 (23) |
Complexity: 2 |
Complexity Density: 0,29 |
|
| 9 |
|
public class ConflictMapMerging extends ConflictMap { |
| 10 |
|
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
| 11 |
76761
|
public ConflictMapMerging(Map<Integer, BigInteger> m, BigInteger d, ILits voc,... |
| 12 |
|
int level) { |
| 13 |
76761
|
super(m, d, voc, level); |
| 14 |
|
} |
|
|
|
| 85,7% |
Uncovered Elements: 2 (14) |
Complexity: 2 |
Complexity Density: 0,25 |
|
| 15 |
76761
|
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 |
|
|
| 32 |
|
|
| 33 |
|
|
| 34 |
|
@param |
| 35 |
|
@param |
| 36 |
|
@param |
| 37 |
|
@param |
| 38 |
|
@return |
| 39 |
|
|
|
|
|
| 0% |
Uncovered Elements: 5 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
| 40 |
0
|
@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 |
|
} |