1 |
|
|
2 |
|
|
3 |
|
|
4 |
|
|
5 |
|
|
6 |
|
|
7 |
|
|
8 |
|
|
9 |
|
|
10 |
|
|
11 |
|
|
12 |
|
|
13 |
|
|
14 |
|
|
15 |
|
|
16 |
|
|
17 |
|
|
18 |
|
|
19 |
|
|
20 |
|
|
21 |
|
|
22 |
|
|
23 |
|
|
24 |
|
|
25 |
|
package org.sat4j.minisat.constraints; |
26 |
|
|
27 |
|
import java.math.BigInteger; |
28 |
|
|
29 |
|
import org.sat4j.minisat.constraints.pb.IDataStructurePB; |
30 |
|
import org.sat4j.minisat.constraints.pb.MinWatchPb; |
31 |
|
import org.sat4j.minisat.constraints.pb.PBConstr; |
32 |
|
import org.sat4j.specs.ContradictionException; |
33 |
|
import org.sat4j.specs.IVec; |
34 |
|
import org.sat4j.specs.IVecInt; |
35 |
|
|
|
|
| 0% |
Uncovered Elements: 6 (6) |
Complexity: 1 |
Complexity Density: 1 |
|
36 |
|
public class PBMinClauseCardConstrDataStructure extends |
37 |
|
PuebloPBMinClauseCardConstrDataStructure { |
38 |
|
|
39 |
|
|
40 |
|
|
41 |
|
|
42 |
|
private static final long serialVersionUID = 1L; |
43 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
44 |
0
|
@Override... |
45 |
|
protected PBConstr constructPB(IDataStructurePB mpb) |
46 |
|
throws ContradictionException { |
47 |
0
|
return MinWatchPb.normalizedMinWatchPbNew(solver, getVocabulary(), mpb); |
48 |
|
} |
49 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
50 |
0
|
@Override... |
51 |
|
protected PBConstr constructPB(int[] lits, BigInteger[] coefs, BigInteger degree) |
52 |
|
throws ContradictionException { |
53 |
0
|
return MinWatchPb.normalizedMinWatchPbNew(solver, getVocabulary(), lits, coefs, degree); |
54 |
|
} |
55 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
56 |
0
|
@Override... |
57 |
|
protected PBConstr constructLearntPB(IVecInt literals, |
58 |
|
IVec<BigInteger> coefs, BigInteger degree) { |
59 |
0
|
return MinWatchPb.watchPbNew(getVocabulary(), literals, coefs, true, |
60 |
|
degree); |
61 |
|
} |
62 |
|
|
63 |
|
} |