Commit 0132cc33 authored by Daniel Le Berre's avatar Daniel Le Berre

Adding test cases for #155.

parent 45015ab4
Pipeline #4427 failed with stages
in 14 minutes and 51 seconds
package org.sat4j;
import static org.junit.Assert.assertEquals;
import org.junit.Test;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.IVecInt;
public class BugSAT155 {
@Test
public void testBasicDump() throws ContradictionException {
ISolver solver = SolverFactory.newDefault();
IVecInt literals = new VecInt(new int[] { 1, 2, 3 });
IConstr c1 = solver.addClause(literals);
assertEquals("1 2 3 0", c1.dump());
}
@Test
public void testBasicDump4Card() throws ContradictionException {
ISolver solver = SolverFactory.newDefault();
IVecInt literals = new VecInt(new int[] { 1, 2, 3 });
IConstr c1 = solver.addAtLeast(literals, 2);
assertEquals("x1 + x2 + x3 >= 2", c1.dump());
}
}
package org.sat4j.pb;
import static org.junit.Assert.assertEquals;
import java.math.BigInteger;
import org.junit.Test;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
public class BugSAT155 {
@Test
public void testBasicDump() throws ContradictionException {
IPBSolver solver = SolverFactory.newDefault();
IVecInt literals = new VecInt(new int[] { 1, 2, 3 });
IConstr c1 = solver.addClause(literals);
assertEquals("1 2 3 0", c1.dump());
}
@Test
public void testBasicDumpPB() throws ContradictionException {
IPBSolver solver = SolverFactory.newCuttingPlanes();
IVecInt literals = new VecInt(new int[] { 1, 2, 3 });
IConstr c1 = solver.addClause(literals);
assertEquals("+1 x1 +1 x2 +1 x3 >= 1", c1.dump());
}
@Test
public void testBasicDump4Card() throws ContradictionException {
IPBSolver solver = SolverFactory.newDefault();
IVecInt literals = new VecInt(new int[] { 1, 2, 3 });
IConstr c1 = solver.addAtLeast(literals, 2);
assertEquals("x1 + x2 + x3 >= 2", c1.dump());
}
@Test
public void testBasicDump4CardPB() throws ContradictionException {
IPBSolver solver = SolverFactory.newCuttingPlanes();
IVecInt literals = new VecInt(new int[] { 1, 2, 3 });
IConstr c1 = solver.addAtLeast(literals, 2);
assertEquals("+1 x1 +1 x2 +1 x3 >= 2", c1.dump());
}
@Test
public void testBasicDump4PB() throws ContradictionException {
IPBSolver solver = SolverFactory.newDefault();
IVecInt literals = new VecInt(new int[] { 1, 2, 3 });
IVec<BigInteger> coeffs = new Vec<>();
coeffs.push(BigInteger.valueOf(2)).push(BigInteger.ONE)
.push(BigInteger.ONE);
IConstr c1 = solver.addAtLeast(literals, coeffs, BigInteger.valueOf(2));
assertEquals("+2 x1 +1 x2 +1 x3 >= 2", c1.dump());
}
}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment