Skip to content

GitLab

Commit 309b935d authored by Daniel Le Berre's avatar Daniel Le Berre
Browse files

Check that non unit constraints are really entered in the solver. Thanks 

STAMP.
parent ec652dcd
Pipeline #3319 passed with stages
in 36 minutes and 9 seconds
Hide whitespace changes
Inline Side-by-side
Showing with 9 additions and 4 deletions
org.sat4j.core/src/test/java/org/sat4j/BugSAT34.java
View file @ 309b935d
......@@ -63,7 +63,8 @@ public class BugSAT34 {
for (String name : SolverFactory.instance().solverNames()) {
if (!"DimacsOutput".equals(name) && !"Statistics".equals(name)) {
solvers.add(new Object[] {
SolverFactory.instance().createSolverByName(name), name });
SolverFactory.instance().createSolverByName(name),
name });
}
}
return solvers;
......@@ -74,9 +75,13 @@ public class BugSAT34 {
this.system.newVar(3);
try {
// x_1 v x_2 <=> x_3
this.system.addClause(new VecInt(new int[] { 1, 2, -3 }));
this.system.addClause(new VecInt(new int[] { -1, 3 }));
this.system.addClause(new VecInt(new int[] { -2, 3 }));
IConstr nonunit;
nonunit = this.system.addClause(new VecInt(new int[] { 1, 2, -3 }));
assertNotNull(nonunit);
nonunit = this.system.addClause(new VecInt(new int[] { -1, 3 }));
assertNotNull(nonunit);
nonunit = this.system.addClause(new VecInt(new int[] { -2, 3 }));
assertNotNull(nonunit);
// not both true
this.system.addClause(new VecInt(new int[] { -1, -2 }));
// x2 is true
......
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