Commit 3cdc6688 authored by Daniel Le Berre's avatar Daniel Le Berre

Fix issue with negative literals in #155

parent 0132cc33
Pipeline #4428 failed with stages
in 13 minutes and 58 seconds
......@@ -121,10 +121,24 @@ public final class LiteralsUtils {
*
* @param x
* the literal in Dimacs format
* @return the literal in internal format.
* @return the literal in internal format
* @since 2.2
*/
public static int toInternal(int x) {
return x < 0 ? -x << 1 ^ 1 : x << 1;
}
/**
* decode the internal representation in an OPB-like representation.
*
* Note that we use the literal representation (~xi) which may not be
* supoorted by all OPB solvers.
*
* @param p
* a literal in internal format
* @return that literal using the OPB literal format.
*/
public static String toOPB(int p) {
return ((p & 1) == 0 ? "" : "~") + "x" + (p >> 1);
}
}
......@@ -430,12 +430,11 @@ public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append('x');
stb.append(LiteralsUtils.toDimacs(this.lits[0]));
stb.append(LiteralsUtils.toOPB(this.lits[0]));
int i = 1;
while (i < this.lits.length) {
stb.append(" + x"); //$NON-NLS-1$
stb.append(LiteralsUtils.toDimacs(lits[i++]));
stb.append(" + "); //$NON-NLS-1$
stb.append(LiteralsUtils.toOPB(lits[i++]));
}
stb.append(" >= "); //$NON-NLS-1$
stb.append(size() - this.maxUnsatisfied);
......
......@@ -533,12 +533,11 @@ public final class MaxWatchCard
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append('x');
stb.append(LiteralsUtils.toDimacs(this.lits[0]));
stb.append(LiteralsUtils.toOPB(this.lits[0]));
int i = 1;
while (i < this.lits.length) {
stb.append(" + x"); //$NON-NLS-1$
stb.append(LiteralsUtils.toDimacs(lits[i++]));
stb.append(" + "); //$NON-NLS-1$
stb.append(LiteralsUtils.toOPB(lits[i++]));
}
stb.append(" >= "); //$NON-NLS-1$
stb.append(this.degree);
......
......@@ -770,12 +770,11 @@ public class MinWatchCard
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append('x');
stb.append(LiteralsUtils.toDimacs(this.lits[0]));
stb.append(LiteralsUtils.toOPB(this.lits[0]));
int i = 1;
while (i < this.lits.length) {
stb.append(" + x"); //$NON-NLS-1$
stb.append(LiteralsUtils.toDimacs(lits[i++]));
stb.append(" + "); //$NON-NLS-1$
stb.append(LiteralsUtils.toOPB(lits[i++]));
}
stb.append(" >= "); //$NON-NLS-1$
stb.append(this.degree);
......
......@@ -21,6 +21,15 @@ public class BugSAT155 {
}
@Test
public void testBasicDumpNegativeLiteral() 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();
......@@ -30,4 +39,14 @@ public class BugSAT155 {
}
@Test
public void testBasicDump4CardNegativeLiteral()
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());
}
}
......@@ -137,12 +137,12 @@ public final class AtLeastPB extends AtLeast implements PBConstr {
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append("+1 x");
stb.append(LiteralsUtils.toDimacs(this.lits[0]));
stb.append("+1 ");
stb.append(LiteralsUtils.toOPB(this.lits[0]));
int i = 1;
while (i < this.lits.length) {
stb.append(" +1 x"); //$NON-NLS-1$
stb.append(LiteralsUtils.toDimacs(lits[i++]));
stb.append(" +1 "); //$NON-NLS-1$
stb.append(LiteralsUtils.toOPB(lits[i++]));
}
stb.append(" >= "); //$NON-NLS-1$
stb.append(size() - this.maxUnsatisfied);
......
......@@ -71,10 +71,10 @@ public final class LearntBinaryClausePB extends LearntBinaryClause
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append("+1 x");
stb.append(LiteralsUtils.toDimacs(head));
stb.append(" +1 x");
stb.append(LiteralsUtils.toDimacs(tail));
stb.append("+1 ");
stb.append(LiteralsUtils.toOPB(head));
stb.append(" +1 ");
stb.append(LiteralsUtils.toOPB(tail));
stb.append(" >= 1");
return stb.toString();
}
......
......@@ -87,14 +87,14 @@ public final class LearntHTClausePB extends LearntHTClause implements PBConstr {
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append("+1 x");
stb.append(LiteralsUtils.toDimacs(this.head));
stb.append("+1 ");
stb.append(LiteralsUtils.toOPB(this.head));
for (int p : middleLits) {
stb.append(" +1 x");
stb.append(LiteralsUtils.toDimacs(p));
stb.append(" +1 ");
stb.append(LiteralsUtils.toOPB(p));
}
stb.append(" +1 x");
stb.append(LiteralsUtils.toDimacs(this.tail));
stb.append(" +1 ");
stb.append(LiteralsUtils.toOPB(this.tail));
stb.append(" >= 1");
return stb.toString();
}
......
......@@ -205,12 +205,12 @@ public final class MinWatchCardPB extends MinWatchCard implements PBConstr {
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append("+1 x");
stb.append(LiteralsUtils.toDimacs(this.lits[0]));
stb.append("+1 ");
stb.append(LiteralsUtils.toOPB(this.lits[0]));
int i = 1;
while (i < this.lits.length) {
stb.append(" +1 x"); //$NON-NLS-1$
stb.append(LiteralsUtils.toDimacs(lits[i++]));
stb.append(" +1 "); //$NON-NLS-1$
stb.append(LiteralsUtils.toOPB(lits[i++]));
}
stb.append(" >= "); //$NON-NLS-1$
stb.append(size() - this.maxUnsatisfied);
......
......@@ -92,10 +92,10 @@ public final class OriginalBinaryClausePB extends OriginalBinaryClause
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append("+1 x");
stb.append(LiteralsUtils.toDimacs(head));
stb.append(" +1 x");
stb.append(LiteralsUtils.toDimacs(tail));
stb.append("+1 ");
stb.append(LiteralsUtils.toOPB(head));
stb.append(" +1 ");
stb.append(LiteralsUtils.toOPB(tail));
stb.append(" >= 1");
return stb.toString();
}
......
......@@ -92,14 +92,14 @@ public final class OriginalHTClausePB extends OriginalHTClause
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append("+1 x");
stb.append(LiteralsUtils.toDimacs(this.head));
stb.append("+1 ");
stb.append(LiteralsUtils.toOPB(this.head));
for (int p : middleLits) {
stb.append(" +1 x");
stb.append(LiteralsUtils.toDimacs(p));
stb.append(" +1 ");
stb.append(LiteralsUtils.toOPB(p));
}
stb.append(" +1 x");
stb.append(LiteralsUtils.toDimacs(this.tail));
stb.append(" +1 ");
stb.append(LiteralsUtils.toOPB(this.tail));
stb.append(" >= 1");
return stb.toString();
}
......
......@@ -31,6 +31,7 @@ package org.sat4j.pb.constraints.pb;
import java.math.BigInteger;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.minisat.constraints.cnf.UnitClause;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.IVecInt;
......@@ -76,8 +77,8 @@ public final class UnitClausePB extends UnitClause implements PBConstr {
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append("+1 x");
stb.append(literal);
stb.append("+1 ");
stb.append(LiteralsUtils.toOPB(literal));
stb.append(" >= 1");
return stb.toString();
}
......
......@@ -706,8 +706,8 @@ public abstract class WatchPb
for (int i = 0; i < this.lits.length; i++) {
stb.append("+");
stb.append(this.coefs[i]);
stb.append(" x");
stb.append(LiteralsUtils.toDimacs(this.lits[i]));
stb.append(" ");
stb.append(LiteralsUtils.toOPB(this.lits[i]));
stb.append(' ');
}
stb.append(">= ");
......
......@@ -720,8 +720,8 @@ public abstract class WatchPbLong
for (int i = 0; i < this.lits.length; i++) {
stb.append("+");
stb.append(this.coefs[i]);
stb.append(" x");
stb.append(LiteralsUtils.toDimacs(this.lits[i]));
stb.append(" ");
stb.append(LiteralsUtils.toOPB(this.lits[i]));
stb.append(' ');
}
stb.append(">= ");
......
......@@ -750,8 +750,8 @@ public abstract class WatchPbLongCP
for (int i = 0; i < this.lits.length; i++) {
stb.append("+");
stb.append(this.coefs[i]);
stb.append(" x");
stb.append(LiteralsUtils.toDimacs(this.lits[i]));
stb.append(" ");
stb.append(LiteralsUtils.toOPB(this.lits[i]));
stb.append(' ');
}
stb.append(">= ");
......
......@@ -32,6 +32,15 @@ public class BugSAT155 {
}
@Test
public void testBasicDumpPBNegativeLiteral() 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();
......@@ -48,6 +57,14 @@ public class BugSAT155 {
assertEquals("+1 x1 +1 x2 +1 x3 >= 2", c1.dump());
}
@Test
public void testBasicDump4CardPBNegative() 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();
......@@ -59,4 +76,14 @@ public class BugSAT155 {
assertEquals("+2 x1 +1 x2 +1 x3 >= 2", c1.dump());
}
@Test
public void testBasicDump4PBNegativeLieral() 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