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 |
|
} |