Commit 3878bb05 authored by leberre's avatar leberre
Browse files

Fix for failing tests.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@2527 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent af47e3af
......@@ -34,6 +34,7 @@ import java.math.BigInteger;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.LearningStrategy;
import org.sat4j.pb.constraints.pb.PBConstr;
import org.sat4j.specs.Constr;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.IVec;
......@@ -58,10 +59,10 @@ public class PBSolverWithImpliedClause extends PBSolverCP {
IVecInt vlits = dimacs2internal(literals);
assert vlits.size() == literals.size();
assert literals.size() == coeffs.size();
PBConstr result = (PBConstr) this.dsfactory
.createPseudoBooleanConstraint(vlits, coeffs, moreThan, degree);
if (result != null) {
IVecInt clits = result.computeAnImpliedClause();
Constr result = this.dsfactory.createPseudoBooleanConstraint(vlits,
coeffs, moreThan, degree);
if (result != null && result != Constr.TAUTOLOGY) {
IVecInt clits = ((PBConstr) result).computeAnImpliedClause();
if (clits != null) {
addConstr(this.dsfactory.createClause(clits));
}
......
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