Commit 45015ab4 authored by Daniel Le Berre's avatar Daniel Le Berre

Initial code for #155

parent 488be78d
Pipeline #4416 failed with stages
in 4 minutes and 51 seconds
......@@ -118,4 +118,16 @@ public class ConstrGroup implements IConstr {
public String toString(VarMapper mapper) {
throw new UnsupportedOperationException();
}
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
for (int i = 0; i < constrs.size(); i++) {
stb.append(constrs.get(i).dump());
if (i < constrs.size() - 1) {
stb.append(System.lineSeparator());
}
}
return stb.toString();
}
}
......@@ -426,4 +426,20 @@ public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
return stb.toString();
}
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append('x');
stb.append(LiteralsUtils.toDimacs(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(size() - this.maxUnsatisfied);
return stb.toString();
}
}
......@@ -529,4 +529,20 @@ public final class MaxWatchCard
}
return stb.toString();
}
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append('x');
stb.append(LiteralsUtils.toDimacs(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(this.degree);
return stb.toString();
}
}
......@@ -63,7 +63,7 @@ public class MinWatchCard
/**
* literals involved in the constraint
*/
private final int[] lits;
protected final int[] lits;
/**
* contains the sign of the constraint : ATLEAT or ATMOST
......@@ -84,7 +84,7 @@ public class MinWatchCard
* Maximum number of falsified literal in the constraint.
*
*/
private final int maxUnsatisfied;
protected final int maxUnsatisfied;
/**
* Constructs and normalizes a cardinality constraint. used by
......@@ -766,4 +766,20 @@ public class MinWatchCard
}
return stb.toString();
}
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append('x');
stb.append(LiteralsUtils.toDimacs(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(this.degree);
return stb.toString();
}
}
......@@ -299,4 +299,14 @@ public abstract class BinaryClause
stb.append("]"); //$NON-NLS-1$
return stb.toString();
}
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append(LiteralsUtils.toDimacs(head));
stb.append(' ');
stb.append(LiteralsUtils.toDimacs(tail));
stb.append(" 0");
return stb.toString();
}
}
......@@ -83,9 +83,8 @@ public class BinaryClauses implements Constr, Propagatable, Serializable {
/*
* (non-Javadoc)
*
* @see
* org.sat4j.minisat.Constr#propagate(org.sat4j.minisat.UnitPropagationListener
* , int)
* @see org.sat4j.minisat.Constr#propagate(org.sat4j.minisat.
* UnitPropagationListener , int)
*/
public boolean propagate(UnitPropagationListener s, int p) {
// assert voc.isFalsified(this.reason);
......@@ -285,4 +284,9 @@ public class BinaryClauses implements Constr, Propagatable, Serializable {
// TODO: implement this method !
throw new UnsupportedOperationException("Not implemented yet!");
}
@Override
public String dump() {
throw new UnsupportedOperationException("Not implemented yet!");
}
}
......@@ -29,6 +29,7 @@ package org.sat4j.minisat.constraints.cnf;
import java.io.Serializable;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.Undoable;
import org.sat4j.specs.Constr;
......@@ -333,4 +334,15 @@ public class CBClause implements Constr, Undoable, Propagatable, Serializable {
public Constr toConstraint() {
return this;
}
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
for (int p : lits) {
stb.append(LiteralsUtils.toDimacs(p));
stb.append(' ');
}
stb.append('0');
return stb.toString();
}
}
......@@ -374,4 +374,18 @@ public abstract class HTClause implements Propagatable, Constr, Serializable {
return stb.toString();
}
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append(LiteralsUtils.toDimacs(this.head));
stb.append(' ');
for (int p : middleLits) {
stb.append(LiteralsUtils.toDimacs(p));
stb.append(' ');
}
stb.append(LiteralsUtils.toDimacs(this.tail));
stb.append(" 0");
return stb.toString();
}
}
......@@ -168,4 +168,12 @@ public class UnitClause implements Constr {
}
return mapper.map(LiteralsUtils.toDimacs(this.literal));
}
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append(literal);
stb.append(" 0");
return stb.toString();
}
}
......@@ -156,4 +156,17 @@ public class UnitClauses implements Constr {
public String toString(VarMapper mapper) {
throw new UnsupportedOperationException("Not implemented yet!");
}
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
for (int i = 0; i < literals.length; i++) {
stb.append(literals[i]);
stb.append(" 0");
if (i < literals.length - 1) {
stb.append(System.lineSeparator());
}
}
return stb.toString();
}
}
......@@ -317,4 +317,15 @@ public abstract class WLClause implements Propagatable, Constr, Serializable {
}
return -1;
}
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
for (int p : lits) {
stb.append(LiteralsUtils.toDimacs(p));
stb.append(' ');
}
stb.append('0');
return stb.toString();
}
}
......@@ -230,4 +230,9 @@ public class Xor implements Constr, Propagatable {
throw new UnsupportedOperationException("Not implemented yet!");
}
@Override
public String dump() {
throw new UnsupportedOperationException("Not implemented yet!");
}
}
......@@ -85,7 +85,8 @@ public interface Constr extends IConstr {
"A tautology cannot be a reason");
}
public void calcReasonOnTheFly(int p, IVecInt trail, IVecInt outReason) {
public void calcReasonOnTheFly(int p, IVecInt trail,
IVecInt outReason) {
throw new UnsupportedOperationException(
"A tautology cannot be a reason");
}
......@@ -141,6 +142,11 @@ public interface Constr extends IConstr {
public int getAssertionLevel(IVecInt trail, int decisionLevel) {
return 0;
}
@Override
public String dump() {
return "";
}
};
/**
......
......@@ -77,4 +77,9 @@ public final class FakeConstr implements IConstr {
public String toString(VarMapper mapper) {
return FAKE_I_CONSTR_MSG;
}
@Override
public String dump() {
throw new UnsupportedOperationException("Not implemented yet!");
}
}
......@@ -88,4 +88,19 @@ public interface IConstr {
* @since 2.3.6
*/
String toString(VarMapper mapper);
/**
* Produces a dump of the constraint using its expected textual
* representation (i.e. Dimacs or OPB format for instance).
*
* {@link #toString()} is aimed at representing the constraint with some
* internal details for e.g. debugging purpose.
*
* This method is supposed to be called to dump the constraint in a file for
* serialization purpose.
*
* @return a textual representation of the constraint, suitable for
* rebuilding it.
*/
String dump();
}
......@@ -85,6 +85,11 @@ public abstract class EmptySolver implements ISolver {
public boolean canBePropagatedMultipleTimes() {
throw new UnsupportedOperationException("Not implemented yet!");
}
@Override
public String dump() {
throw new UnsupportedOperationException("Not implemented yet!");
}
};
private int nbVars;
......@@ -112,7 +117,8 @@ public abstract class EmptySolver implements ISolver {
throw new UnsupportedOperationException("Not implemented yet!");
}
public boolean isSatisfiable(boolean globalTimeout) throws TimeoutException {
public boolean isSatisfiable(boolean globalTimeout)
throws TimeoutException {
throw new UnsupportedOperationException("Not implemented yet!");
}
......
......@@ -68,4 +68,9 @@ public class UnitWeightedClause implements IConstr {
throw new UnsupportedOperationException();
}
@Override
public String dump() {
throw new UnsupportedOperationException();
}
}
......@@ -31,6 +31,7 @@ package org.sat4j.pb.constraints.pb;
import java.math.BigInteger;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.minisat.constraints.card.AtLeast;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.ContradictionException;
......@@ -133,4 +134,19 @@ public final class AtLeastPB extends AtLeast implements PBConstr {
return null;
}
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append("+1 x");
stb.append(LiteralsUtils.toDimacs(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(" >= "); //$NON-NLS-1$
stb.append(size() - this.maxUnsatisfied);
return stb.toString();
}
}
......@@ -31,12 +31,13 @@ package org.sat4j.pb.constraints.pb;
import java.math.BigInteger;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.minisat.constraints.cnf.LearntBinaryClause;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.IVecInt;
public final class LearntBinaryClausePB extends LearntBinaryClause implements
PBConstr {
public final class LearntBinaryClausePB extends LearntBinaryClause
implements PBConstr {
public LearntBinaryClausePB(IVecInt ps, ILits voc) {
super(ps, voc);
......@@ -67,4 +68,14 @@ public final class LearntBinaryClausePB extends LearntBinaryClause implements
return BigInteger.ONE;
}
@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");
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.LearntHTClause;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.IVecInt;
......@@ -83,4 +84,19 @@ public final class LearntHTClausePB extends LearntHTClause implements PBConstr {
return BigInteger.ONE;
}
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append("+1 x");
stb.append(LiteralsUtils.toDimacs(this.head));
for (int p : middleLits) {
stb.append(" +1 x");
stb.append(LiteralsUtils.toDimacs(p));
}
stb.append(" +1 x");
stb.append(LiteralsUtils.toDimacs(this.tail));
stb.append(" >= 1");
return stb.toString();
}
}
......@@ -587,5 +587,10 @@ public final class MaxWatchPbLong extends WatchPbLong {
return cstr.getCoefs();
}
@Override
public String dump() {
return cstr.dump();
}
}
}
......@@ -31,6 +31,7 @@ package org.sat4j.pb.constraints.pb;
import java.math.BigInteger;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.minisat.constraints.card.MinWatchCard;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.ContradictionException;
......@@ -201,4 +202,19 @@ public final class MinWatchCardPB extends MinWatchCard implements PBConstr {
return null;
}
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append("+1 x");
stb.append(LiteralsUtils.toDimacs(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(" >= "); //$NON-NLS-1$
stb.append(size() - this.maxUnsatisfied);
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.OriginalBinaryClause;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.IVecInt;
......@@ -88,4 +89,15 @@ public final class OriginalBinaryClausePB extends OriginalBinaryClause
return c;
}
@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");
return stb.toString();
}
}
......@@ -31,13 +31,14 @@ package org.sat4j.pb.constraints.pb;
import java.math.BigInteger;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.minisat.constraints.cnf.OriginalHTClause;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.UnitPropagationListener;
public final class OriginalHTClausePB extends OriginalHTClause implements
PBConstr {
public final class OriginalHTClausePB extends OriginalHTClause
implements PBConstr {
public OriginalHTClausePB(IVecInt ps, ILits voc) {
super(ps, voc);
......@@ -88,4 +89,18 @@ public final class OriginalHTClausePB extends OriginalHTClause implements
return c;
}
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append("+1 x");
stb.append(LiteralsUtils.toDimacs(this.head));
for (int p : middleLits) {
stb.append(" +1 x");
stb.append(LiteralsUtils.toDimacs(p));
}
stb.append(" +1 x");
stb.append(LiteralsUtils.toDimacs(this.tail));
stb.append(" >= 1");
return stb.toString();
}
}
......@@ -73,4 +73,12 @@ public final class UnitClausePB extends UnitClause implements PBConstr {
return this.voc;
}
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
stb.append("+1 x");
stb.append(literal);
stb.append(" >= 1");
return stb.toString();
}
}
......@@ -64,5 +64,4 @@ public class UnitClausesPB extends UnitClauses implements PBConstr {
public IVecInt computeAnImpliedClause() {
throw new UnsupportedOperationException();
}
}
......@@ -699,4 +699,20 @@ public abstract class WatchPb
return stb.toString();
}
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
if (this.lits.length > 0) {
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(">= ");
stb.append(this.degree);
}
return stb.toString();
}
}
......@@ -712,4 +712,21 @@ public abstract class WatchPbLong
}
return res;
}
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
if (this.lits.length > 0) {
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(">= ");
stb.append(this.degree);
}
return stb.toString();
}
}
......@@ -742,4 +742,21 @@ public abstract class WatchPbLongCP
}
return stb.toString();
}
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
if (this.lits.length > 0) {
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(">= ");
stb.append(this.degree);
}
return stb.toString();
}
}
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