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 |
|
|
26 |
|
package org.sat4j.minisat.constraints; |
27 |
|
|
28 |
|
import org.sat4j.minisat.constraints.cnf.LearntWLClause; |
29 |
|
import org.sat4j.minisat.constraints.cnf.Lits; |
30 |
|
import org.sat4j.minisat.constraints.cnf.OriginalWLClause; |
31 |
|
import org.sat4j.minisat.constraints.cnf.WLClause; |
32 |
|
import org.sat4j.minisat.core.Constr; |
33 |
|
import org.sat4j.minisat.core.ILits; |
34 |
|
import org.sat4j.specs.ContradictionException; |
35 |
|
import org.sat4j.specs.IVecInt; |
36 |
|
|
37 |
|
|
38 |
|
@author |
39 |
|
|
40 |
|
|
|
|
| 18,2% |
Uncovered Elements: 9 (11) |
Complexity: 2 |
Complexity Density: 0,67 |
|
41 |
|
public class ClausalDataStructureWL extends AbstractDataStructureFactory<ILits> { |
42 |
|
|
43 |
|
private static final long serialVersionUID = 1L; |
44 |
|
|
45 |
|
|
46 |
|
|
47 |
|
|
48 |
|
@see |
49 |
|
|
|
|
| 0% |
Uncovered Elements: 6 (6) |
Complexity: 2 |
Complexity Density: 0,5 |
|
50 |
0
|
public Constr createClause(IVecInt literals) throws ContradictionException {... |
51 |
0
|
IVecInt v = WLClause.sanityCheck(literals, getVocabulary(), solver); |
52 |
0
|
if (v == null) |
53 |
0
|
return null; |
54 |
0
|
return OriginalWLClause.brandNewClause(solver, getVocabulary(), v); |
55 |
|
} |
56 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
57 |
0
|
public Constr createUnregisteredClause(IVecInt literals) {... |
58 |
0
|
return new LearntWLClause(literals, getVocabulary()); |
59 |
|
} |
60 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
61 |
9
|
@Override... |
62 |
|
protected ILits createLits() { |
63 |
9
|
return new Lits(); |
64 |
|
} |
65 |
|
} |