Commit 83265ace authored by Daniel Le Berre's avatar Daniel Le Berre
Browse files

added constraints for = in the same order as expected by VeriPB

parent ea618d84
......@@ -497,8 +497,8 @@ public class Solver<D extends DataStructureFactory>
public IConstr addExactly(IVecInt literals, int n)
throws ContradictionException {
ConstrGroup group = new ConstrGroup(false);
group.add(addAtMost(literals, n));
group.add(addAtLeast(literals, n));
group.add(addAtMost(literals, n));
return group;
}
......
......@@ -164,10 +164,10 @@ public abstract class PBSolver extends Solver<PBDataStructureFactory>
assert vlits.size() == literals.size();
assert literals.size() == coeffs.size();
ConstrGroup group = new ConstrGroup(false);
group.add(addConstr(this.dsfactory.createPseudoBooleanConstraint(vlits,
coeffs, false, weight)));
group.add(addConstr(this.dsfactory.createPseudoBooleanConstraint(vlits,
coeffs, true, weight)));
group.add(addConstr(this.dsfactory.createPseudoBooleanConstraint(vlits,
coeffs, false, weight)));
return group;
}
......
Supports Markdown
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