| 1 |
|
|
| 2 |
|
|
| 3 |
|
|
| 4 |
|
|
| 5 |
|
|
| 6 |
|
|
| 7 |
|
package org.sat4j.minisat.constraints.pb; |
| 8 |
|
|
| 9 |
|
import java.math.BigInteger; |
| 10 |
|
|
| 11 |
|
import junit.framework.TestCase; |
| 12 |
|
|
| 13 |
|
import org.sat4j.core.Vec; |
| 14 |
|
import org.sat4j.core.VecInt; |
| 15 |
|
import org.sat4j.minisat.SolverFactory; |
| 16 |
|
import org.sat4j.minisat.constraints.PBMaxDataStructure; |
| 17 |
|
import org.sat4j.minisat.core.DataStructureFactory; |
| 18 |
|
import org.sat4j.minisat.core.ILits; |
| 19 |
|
import org.sat4j.minisat.core.Solver; |
| 20 |
|
import org.sat4j.specs.ContradictionException; |
| 21 |
|
import org.sat4j.specs.IVec; |
| 22 |
|
import org.sat4j.specs.IVecInt; |
| 23 |
|
|
| 24 |
|
|
| 25 |
|
@author |
| 26 |
|
|
| 27 |
|
|
| 28 |
|
|
| 29 |
|
|
|
|
|
| 96,7% |
Uncovered Elements: 1 (30) |
Complexity: 6 |
Complexity Density: 0,35 |
|
| 30 |
|
public class WatchPbTest extends TestCase { |
| 31 |
|
|
| 32 |
|
|
| 33 |
|
|
| 34 |
|
|
| 35 |
|
@param |
| 36 |
|
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
| 37 |
1
|
 public WatchPbTest(String arg0) {... |
| 38 |
1
|
super(arg0); |
| 39 |
|
} |
| 40 |
|
|
|
|
|
| 96,3% |
Uncovered Elements: 1 (27) |
Complexity: 6 |
Complexity Density: 0,32 |
1
PASS
|
|
| 41 |
1
|
public void testNormalize() {... |
| 42 |
|
|
| 43 |
|
|
| 44 |
|
|
| 45 |
|
|
| 46 |
|
|
| 47 |
|
|
| 48 |
|
|
| 49 |
|
|
| 50 |
|
|
| 51 |
|
|
| 52 |
|
|
| 53 |
|
|
| 54 |
|
|
| 55 |
|
|
| 56 |
|
|
| 57 |
|
|
| 58 |
|
|
| 59 |
|
|
| 60 |
|
|
| 61 |
|
|
| 62 |
|
|
| 63 |
1
|
IVecInt expectedLits = new VecInt(); |
| 64 |
91
|
for (int i = 1; i <= 90; i++) { |
| 65 |
90
|
expectedLits.push(i); |
| 66 |
|
} |
| 67 |
|
|
| 68 |
1
|
IVec<BigInteger> expectedCoeffs = new Vec<BigInteger>(); |
| 69 |
1
|
BigInteger sum = BigInteger.ZERO; |
| 70 |
1
|
BigInteger coef; |
| 71 |
1
|
int[] values = { 202, -79, 100023, -89810, -9980, 1000, 100, 10000, |
| 72 |
|
100, -1 }; |
| 73 |
|
|
| 74 |
11
|
for (int j = 0; j < values.length; j++) { |
| 75 |
100
|
for (int i = 1; i <= 9; i++) { |
| 76 |
90
|
expectedCoeffs.push(coef = BigInteger.valueOf(values[j] * i)); |
| 77 |
90
|
if (coef.signum() > 0) { |
| 78 |
54
|
sum = sum.add(coef); |
| 79 |
|
} |
| 80 |
|
} |
| 81 |
|
} |
| 82 |
1
|
DataStructureFactory<ILits> daf = new PBMaxDataStructure(); |
| 83 |
1
|
Solver<ILits> solver = (Solver<ILits>) SolverFactory.newMiniLearning(daf); |
| 84 |
1
|
daf.getVocabulary().ensurePool(100); |
| 85 |
1
|
try { |
| 86 |
1
|
solver.addPseudoBoolean(expectedLits, expectedCoeffs, false, |
| 87 |
|
BigInteger.ZERO); |
| 88 |
1
|
assertEquals(sum, ((WatchPb) solver.getIthConstr(0)).getDegree()); |
| 89 |
|
} catch (ContradictionException e) { |
| 90 |
0
|
fail("The constraint is not a contradiction!!!"); |
| 91 |
|
} |
| 92 |
|
} |
| 93 |
|
|
| 94 |
|
} |
org.sat4j.minisat.constraints.pb.WatchPbTest.testNormalize
