Commit 171059c7 authored by Daniel Le Berre's avatar Daniel Le Berre

Merge branch 'master' of https://gitlab.ow2.org/sat4j/sat4j.git

parents 3bc22078 2d75931e
Pipeline #201 passed with stage
in 11 minutes and 6 seconds
No preview for this file type
......@@ -429,7 +429,9 @@ public abstract class AbstractLauncher implements Serializable, ILogAble {
}
protected void flushLog() {
this.out.print(logBuffer.toString());
if (logBuffer != null) {
this.out.print(logBuffer.toString());
}
logBuffer = null;
}
......
......@@ -23,7 +23,6 @@ import java.util.Map;
import org.sat4j.AbstractLauncher;
import org.sat4j.ILauncherMode;
import org.sat4j.pb.tools.PBAdapter;
import org.sat4j.reader.ECSPFormat;
import org.sat4j.reader.ParseFormatException;
import org.sat4j.reader.Reader;
......@@ -41,7 +40,9 @@ public class CSPLauncher extends AbstractLauncher {
private boolean shouldOnlyDisplayEncoding = false;
public CSPLauncher() {
bufferizeLog();
if(System.getProperty("CompetitionOutput") != null) {
bufferizeLog();
}
}
/*
......@@ -55,7 +56,7 @@ public class CSPLauncher extends AbstractLauncher {
if (args.length == 2) {
asolver = SolverFactory.instance().createSolverByName(args[0]);
} else {
asolver = new CspSatSolverDecorator(new PBAdapter(SolverFactory.newDefault()));
asolver = new CspSatSolverDecorator(org.sat4j.pb.SolverFactory.newDefault());
}
log(asolver.toString(COMMENT_PREFIX));
this.shouldOnlyDisplayEncoding = asolver.shouldOnlyDisplayEncoding();
......@@ -138,4 +139,14 @@ public class CSPLauncher extends AbstractLauncher {
return args[0];
return args[1];
}
@Override
protected void displayResult() {
try {
Thread.sleep(200);
} catch (InterruptedException e) {
e.printStackTrace();
}
super.displayResult();
}
}
......@@ -21,6 +21,7 @@ package org.sat4j.csp.constraints3;
import java.util.SortedSet;
import java.util.TreeSet;
import org.sat4j.csp.intension.ICspToSatEncoder;
import org.sat4j.csp.intension.IIntensionCtrEncoder;
import org.sat4j.reader.XMLCSP3Reader;
import org.xcsp.common.Types.TypeOperatorRel;
......@@ -40,19 +41,20 @@ public class ComparisonCtrBuilder {
public ComparisonCtrBuilder(IIntensionCtrEncoder intensionEnc) {
this.intensionCtrEncoder = intensionEnc;
}
public boolean buildCtrAllDifferent(XVarInteger[] list) { // TODO:
// remove
// dependence
// to
// varmapping
public boolean buildCtrAllDifferent(XVarInteger[] list) {
final ICspToSatEncoder solver = this.intensionCtrEncoder.getSolver();
for (int i = 0; i < list.length - 1; ++i) {
final String norm1 = CtrBuilderUtils.normalizeCspVarName(list[i].id);
final int[] d1 = solver.getCspVarDomain(list[i].id);
for (int j = i + 1; j < list.length; ++j) {
final String norm2 = CtrBuilderUtils.normalizeCspVarName(list[j].id);
final String expr = "ne(" + norm1 + "," + norm2 + ")";
if (this.intensionCtrEncoder.encode(expr))
return true;
final int[] d2 = solver.getCspVarDomain(list[j].id);
for(int v1 : d1) {
for(int v2 : d2) {
if(v1 == v2) {
solver.addClause(new int[]{-solver.getSolverVar(list[i].id, v1), -solver.getSolverVar(list[j].id, v2)});
}
}
}
}
}
return false;
......
......@@ -41,6 +41,22 @@ public class ConnectionCtrBuilder {
this.intensionCtrEncoder = intensionEnc;
}
public boolean buildCtrChannel(String id, XVarInteger[] list, int startIndex, XVarInteger value) {
for(int i=0; i<list.length; ++i) {
final String[] andParts = new String[list.length];
for(int j=0; j<list.length; ++j) {
final String normJ = CtrBuilderUtils.normalizeCspVarName(list[j].id);
andParts[j] = "eq("+normJ+","+(i==j ? 1 : 0)+")";
}
final String andExpr = CtrBuilderUtils.chainExpressionsForAssociativeOp(andParts, "and");
final String expr = "imp(eq("+CtrBuilderUtils.normalizeCspVarName(value.id)+","+(i+startIndex)+"),"+andExpr+")";
if(this.intensionCtrEncoder.encode(expr)) {
return true;
}
}
return false;
}
public boolean buildCtrChannel(String id, XVarInteger[] list1, int startIndex1, XVarInteger[] list2, int startIndex2) {
if(list1.length != list2.length) {
throw new IllegalArgumentException("lists of different sizes provided as arguments of channel constraint");
......@@ -112,7 +128,7 @@ public class ConnectionCtrBuilder {
}
public boolean buildCtrElement(String id, XVarInteger[] list, int value) {
return buildCtrElement(id, list, 0, null, TypeRank.ANY, value);
return buildCtrElementAnyIndex(list, value);
}
public boolean buildCtrMaximum(String id, XVarInteger[] list, int startIndex, XVarInteger index, TypeRank rank, Condition condition) {
......@@ -200,7 +216,7 @@ public class ConnectionCtrBuilder {
public boolean buildCtrElement(String id, XVarInteger[] list, int startIndex, XVarInteger index, TypeRank rank, int value) {
if(rank == TypeRank.ANY) {
return buildCtrElementAnyIndex(list, value);
return buildCtrElementForceIndex(list, startIndex, index, value);
} else if(rank == TypeRank.FIRST) {
return buildCtrElementNotAnyIndex(list, startIndex, index, value, true);
} else if(rank == TypeRank.LAST) {
......@@ -221,6 +237,20 @@ public class ConnectionCtrBuilder {
return false;
}
private boolean buildCtrElementForceIndex(XVarInteger[] list, int startIndex, XVarInteger index, int value) {
final int len = list.length;
final String[] subexprs = new String[list.length];
final String normIndex = CtrBuilderUtils.normalizeCspVarName(index.id);
for(int i=0; i<len; ++i) {
final String lImpl = "eq("+Integer.toString(i+startIndex)+","+normIndex+")";
final String rImpl = "eq("+value+","+CtrBuilderUtils.normalizeCspVarName(list[i].id)+")";
subexprs[i] = "imp("+lImpl+","+rImpl+")";
}
final String expr = CtrBuilderUtils.chainExpressionsForAssociativeOp(subexprs, "and");
this.intensionCtrEncoder.encode(expr);
return false;
}
private boolean buildCtrElementNotAnyIndex(XVarInteger[] list, int startIndex, XVarInteger index, int value, boolean isFirst) {
int len = list.length;
String[] subExprs = new String[len];
......@@ -240,12 +270,12 @@ public class ConnectionCtrBuilder {
}
public boolean buildCtrElement(String id, XVarInteger[] list, XVarInteger value) {
return buildCtrElement(id, list, 0, null, TypeRank.ANY, value);
return buildCtrElementAnyIndex(list, value);
}
public boolean buildCtrElement(String id, XVarInteger[] list, int startIndex, XVarInteger index, TypeRank rank, XVarInteger value) {
if(rank == TypeRank.ANY) {
return buildCtrElementAnyIndex(list, value);
return buildCtrElementForceIndex(list, startIndex, index, value);
} else if(rank == TypeRank.FIRST) {
return buildCtrElementFirstIndex(list, startIndex, index, value);
} else if(rank == TypeRank.LAST) {
......@@ -254,6 +284,21 @@ public class ConnectionCtrBuilder {
throw new IllegalArgumentException();
}
private boolean buildCtrElementForceIndex(XVarInteger[] list, int startIndex, XVarInteger index, XVarInteger value) {
final int len = list.length;
final String[] subexprs = new String[list.length];
final String normIndex = CtrBuilderUtils.normalizeCspVarName(index.id);
final String normValue = CtrBuilderUtils.normalizeCspVarName(value.id);
for(int i=0; i<len; ++i) {
final String lImpl = "eq("+Integer.toString(i+startIndex)+","+normIndex+")";
final String rImpl = "eq("+normValue+","+CtrBuilderUtils.normalizeCspVarName(list[i].id)+")";
subexprs[i] = "imp("+lImpl+","+rImpl+")";
}
final String expr = CtrBuilderUtils.chainExpressionsForAssociativeOp(subexprs, "and");
this.intensionCtrEncoder.encode(expr);
return false;
}
private boolean buildCtrElementAnyIndex(XVarInteger[] list, XVarInteger value) {
int len = list.length;
String[] subExprs = new String[len];
......@@ -262,7 +307,8 @@ public class ConnectionCtrBuilder {
String normVar = CtrBuilderUtils.normalizeCspVarName(list[i].id);
subExprs[i] = "eq("+normVar+","+normValue+")";
}
this.intensionCtrEncoder.encode(CtrBuilderUtils.chainExpressionsForAssociativeOp(subExprs, "or"));
final String expr = CtrBuilderUtils.chainExpressionsForAssociativeOp(subExprs, "or");
this.intensionCtrEncoder.encode(expr);
return false;
}
......@@ -298,4 +344,62 @@ public class ConnectionCtrBuilder {
return false;
}
public boolean buildCtrElement(String id, int[] list, int startIndex, XVarInteger index, TypeRank rank, XVarInteger value) {
if(rank == TypeRank.ANY) {
return buildCtrElementForceIndex(list, startIndex, index, value);
} else if(rank == TypeRank.FIRST) {
return buildCtrElementFirstIndex(list, startIndex, index, value);
} else if(rank == TypeRank.LAST) {
return buildCtrElementLastIndex(list, startIndex, index, value);
}
throw new IllegalArgumentException();
}
private boolean buildCtrElementForceIndex(int[] list, int startIndex, XVarInteger index, XVarInteger value) {
final int len = list.length;
final String[] subexprs = new String[list.length];
final String normIndex = CtrBuilderUtils.normalizeCspVarName(index.id);
final String normValue = CtrBuilderUtils.normalizeCspVarName(value.id);
for(int i=0; i<len; ++i) {
final String lImpl = "eq("+Integer.toString(i+startIndex)+","+normIndex+")";
final String rImpl = "eq("+normValue+","+Integer.toString(list[i])+")";
subexprs[i] = "imp("+lImpl+","+rImpl+")";
}
final String expr = CtrBuilderUtils.chainExpressionsForAssociativeOp(subexprs, "and");
this.intensionCtrEncoder.encode(expr);
return false;
}
private boolean buildCtrElementFirstIndex(int[] list, int startIndex, XVarInteger index, XVarInteger value) {
for(int i=0; i<list.length; ++i) {
// or(ne(i,index),and(eq(i,index),eq(xi,value),ne(x0,value),...,ne(xi-1,value)))
String normIndex = CtrBuilderUtils.normalizeCspVarName(index.id);
String normValue = CtrBuilderUtils.normalizeCspVarName(value.id);
StringBuilder sbuf = new StringBuilder();
sbuf.append("or(ne(").append(i+startIndex).append(',').append(normIndex).append("),and(eq(").append(i+startIndex).append(',').append(normIndex).append("),eq(").append(Integer.toString(list[i])).append(',').append(normValue).append(')');
for(int j=0; j<i; ++j) {
sbuf.append(",ne(").append(Integer.toString(list[j])).append(',').append(normValue).append(')'); // end NE operator
}
sbuf.append("))");
this.intensionCtrEncoder.encode(sbuf.toString());
}
return false;
}
private boolean buildCtrElementLastIndex(int[] list, int startIndex, XVarInteger index, XVarInteger value) {
for(int i=0; i<list.length; ++i) {
// or(ne(i,index),and(eq(i,index),eq(xi,value),ne(xi+1,value),...,ne(xn,value)))
String normIndex = CtrBuilderUtils.normalizeCspVarName(index.id);
String normValue = CtrBuilderUtils.normalizeCspVarName(value.id);
StringBuilder sbuf = new StringBuilder();
sbuf.append("or(ne(").append(i+startIndex).append(',').append(normIndex).append("),and(eq(").append(i+startIndex).append(',').append(normIndex).append("),eq(").append(Integer.toString(list[i])).append(',').append(normValue).append(')'); // end EQ2 operator
for(int j=i+1; j<list.length; ++j) {
sbuf.append(",ne(").append(Integer.toString(list[j])).append(',').append(normValue).append(')');
}
sbuf.append("))");
this.intensionCtrEncoder.encode(sbuf.toString());
}
return false;
}
}
......@@ -68,7 +68,42 @@ public class CountingCtrBuilder {
exprBuf.append(',');
}
varId = list[list.length-1].id;
exprBuf.append(CtrBuilderUtils.normalizeCspVarName(varId));
final int lastCoeff = coeffs[list.length-1];
final String normName = CtrBuilderUtils.normalizeCspVarName(varId);
exprBuf.append(lastCoeff == 1 ? normName : "mul("+lastCoeff+","+normName+")");
for(int i=0; i<list.length-1; ++i) {
exprBuf.append(')');
}
exprBuf.append(',');
if(condition instanceof ConditionVar) {
varId = ((ConditionVar) condition).x.id();
exprBuf.append(CtrBuilderUtils.normalizeCspVarName(varId));
} else if(condition instanceof ConditionVal) {
exprBuf.append(((ConditionVal) condition).k);
} else {
throw new UnsupportedOperationException("this kind of condition is not supported yet.");
}
exprBuf.append(')');
String expr = exprBuf.toString();
return this.intensionCtrEnc.encode(expr);
}
public boolean buildCtrSum(String id, XVarInteger[] list, XVarInteger[] coeffs, Condition condition) {
String varId;
StringBuilder exprBuf = new StringBuilder();
exprBuf.append(((ConditionRel)condition).operator.toString().toLowerCase());
exprBuf.append('(');
for(int i=0; i<list.length-1; ++i) {
exprBuf.append("add(");
exprBuf.append("mul(").append(CtrBuilderUtils.normalizeCspVarName(coeffs[i].id)).append(',');
varId = list[i].id;
exprBuf.append(CtrBuilderUtils.normalizeCspVarName(varId));
exprBuf.append(')');
exprBuf.append(',');
}
varId = list[list.length-1].id;
final String normName = CtrBuilderUtils.normalizeCspVarName(varId);
exprBuf.append("mul("+CtrBuilderUtils.normalizeCspVarName(coeffs[list.length-1].id)+","+normName+")");
for(int i=0; i<list.length-1; ++i) {
exprBuf.append(')');
}
......@@ -213,7 +248,7 @@ public class CountingCtrBuilder {
}
public boolean buildCtrNotAllEqual(String id, XVarInteger[] list) {
return buildCtrNValues(id, list, new StringCondition("ne(", ","+Integer.toString(list.length)+""));
return buildCtrNValues(id, list, new StringCondition("ne(", ",1)"));
}
public boolean buildCtrCardinality(String id, XVarInteger[] list, boolean closed, int[] values, XVarInteger[] occurs) {
......
......@@ -94,7 +94,9 @@ public class ObjBuilder {
literals.push(this.cspToSatEncoder.getSolverVar(varId, val));
coeffs.push(BigInteger.valueOf(val));
}
return new ObjectiveFunction(literals, coeffs);
final ObjectiveFunction obj = new ObjectiveFunction(literals, coeffs);
// obj.setCorrection(BigInteger.ONE);
return obj;
}
public void buildObjToMaximize(final String id, final XVarInteger x) {
......@@ -158,6 +160,7 @@ public class ObjBuilder {
throw new UnsupportedOperationException();
}
if(negate) {
obj.setCorrectionFactor(BigInteger.ONE.negate());
obj.negate();
}
addObjectiveFunction(obj);
......@@ -208,6 +211,7 @@ public class ObjBuilder {
}
if(min < 0) throw new UnsupportedOperationException("negative coeff");
final ObjectiveFunction obj = new ObjectiveFunction();
// obj.setCorrection(BigInteger.ONE);
final BigInteger step = BigInteger.valueOf(max+1);
BigInteger fact = BigInteger.ONE;
for(int i=xlist.length; i>=0; --i) {
......@@ -223,14 +227,17 @@ public class ObjBuilder {
private ObjectiveFunction buildExprObjToMinimize(String expr, boolean negate) {
final ObjectiveFunction obj = this.intensionEnc.encodeObj(expr);
// obj.setCorrection(BigInteger.ONE);
if(negate) {
obj.negate();
obj.setCorrectionFactor(BigInteger.ONE.negate());
}
return obj;
}
private ObjectiveFunction buildSumObjToMinimize(final XVarInteger[] xlist, final int[] xcoeffs) {
final ObjectiveFunction obj = new ObjectiveFunction();
// obj.setCorrection(BigInteger.ONE);
final int size = xlist.length;
for(int i=0; i<size; ++i) {
obj.add(buildObjForVar(xlist[i]).multiply(BigInteger.valueOf(xcoeffs[i])));
......
......@@ -19,7 +19,10 @@
package org.sat4j.csp.constraints3;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashSet;
import java.util.List;
import java.util.Set;
import org.sat4j.csp.intension.IIntensionCtrEncoder;
import org.sat4j.reader.XMLCSP3Reader;
......@@ -472,4 +475,80 @@ public class SchedulingCtrBuilder {
return false;
}
public boolean buildCtrCircuit(String id, XVarInteger[] list, int startIndex) {
final List<List<Integer>> circuits = buildCircuits(new int[list.length], 0);
final String circuitsExprs[] = new String[circuits.size()];
for(int i=0; i<circuits.size(); ++i) {
final List<Integer> circuit = circuits.get(i);
final String eqExprs[] = new String[circuit.size()];
for(int j=0; j<circuit.size(); ++j) {
final String norm = CtrBuilderUtils.normalizeCspVarName(list[j].id);
eqExprs[j] = "eq("+norm+","+(circuit.get(j)+startIndex)+")";
}
circuitsExprs[i] = CtrBuilderUtils.chainExpressionsForAssociativeOp(eqExprs, "and");
}
final String expr = CtrBuilderUtils.chainExpressionsForAssociativeOp(circuitsExprs, "or");
return this.intensionEnc.encode(expr);
}
private List<List<Integer>> buildCircuits(int[] circuit, int length) {
if(length == circuit.length) {
return returnIfCircuit(circuit);
}
List<List<Integer>> circuits = new ArrayList<>();
for(int i=0; i<circuit.length; ++i) {
boolean mustContinue = false;
for(int j=0; j<length; ++j) {
if(circuit[j] == i) {
mustContinue = true;
break;
}
}
if(mustContinue) {
continue;
}
circuit[length] = i;
circuits.addAll(buildCircuits(circuit, length+1));
}
return circuits;
}
private List<List<Integer>> returnIfCircuit(int[] circuit) {
Set<Integer> visited = new HashSet<>();
int i=0;
for(; i < circuit.length && circuit[i] == i; ++i) {
visited.add(circuit[i]);
}
if(i < circuit.length) {
final int start = i;
visited.add(i);
for(i=circuit[i]; i!=start; i=circuit[i]) {
visited.add(i);
}
i = start;
}
for(; i<circuit.length; ++i) {
if(circuit[i] == i) {
visited.add(i);
}
}
List<List<Integer>> circuits = new ArrayList<>();
if(visited.size() == circuit.length) {
List<Integer> circuitAsList = new ArrayList<>();
Arrays.stream(circuit).forEach(x -> circuitAsList.add(x));
circuits.add(circuitAsList);
}
return circuits;
}
public boolean buildCtrCircuit(String id, XVarInteger[] list, int startIndex, XVarInteger size) {
// TODO Auto-generated method stub
return false;
}
public boolean buildCtrCircuit(String id, XVarInteger[] list, int startIndex, int size) {
// TODO Auto-generated method stub
return false;
}
}
......@@ -76,7 +76,7 @@ public class TseitinBasedIntensionCtrEncoder implements IIntensionCtrEncoder {
private boolean encodeExpression(IExpression expression) {
Map<Integer, Integer> map = encodeWithTseitin(expression);
for(Map.Entry<Integer, Integer> entry : map.entrySet()) {
this.solver.addClause(new int[]{entry.getKey() == 0 ? -entry.getValue() : entry.getValue()});
this.solver.addClause(new int[]{entry.getKey().equals(0) ? -entry.getValue() : entry.getValue()});
}
return false;
}
......@@ -371,7 +371,7 @@ public class TseitinBasedIntensionCtrEncoder implements IIntensionCtrEncoder {
Iterator<Entry<Integer, Integer>> it2 = mappings.get(1).entrySet().iterator();
while(it2.hasNext()) {
Entry<Integer, Integer> entry2 = it2.next();
buildImplVar(ret, entry1.getValue(), entry2.getValue(), entry1.getKey()!=entry2.getKey()?1:0);
buildImplVar(ret, entry1.getValue(), entry2.getValue(), !entry1.getKey().equals(entry2.getKey())?1:0);
}
}
return ret;
......@@ -387,7 +387,7 @@ public class TseitinBasedIntensionCtrEncoder implements IIntensionCtrEncoder {
Iterator<Entry<Integer, Integer>> it2 = mappings.get(1).entrySet().iterator();
while(it2.hasNext()) {
Entry<Integer, Integer> entry2 = it2.next();
buildImplVar(ret, entry1.getValue(), entry2.getValue(), entry1.getKey()==entry2.getKey()?1:0);
buildImplVar(ret, entry1.getValue(), entry2.getValue(), entry1.getKey().equals(entry2.getKey())?1:0);
}
}
return ret;
......@@ -404,7 +404,7 @@ public class TseitinBasedIntensionCtrEncoder implements IIntensionCtrEncoder {
public Map<Integer, Integer> encodeOperatorNot(List<Map<Integer,Integer>> mappings) {
Map<Integer, Integer> ret = new HashMap<>();
for(Map.Entry<Integer, Integer> entry : mappings.get(0).entrySet()) {
ret.put(entry.getKey()==0 ? 1 : 0, entry.getValue());
ret.put(entry.getKey().equals(0) ? 1 : 0, entry.getValue());
}
return ret;
}
......@@ -419,7 +419,7 @@ public class TseitinBasedIntensionCtrEncoder implements IIntensionCtrEncoder {
Iterator<Entry<Integer, Integer>> it2 = mappings.get(1).entrySet().iterator();
while(it2.hasNext()) {
Entry<Integer, Integer> entry2 = it2.next();
buildImplVar(ret, entry1.getValue(), entry2.getValue(), entry1.getKey()!=0 && entry2.getKey()!=0?1:0);
buildImplVar(ret, entry1.getValue(), entry2.getValue(), !entry1.getKey().equals(0) && !entry2.getKey().equals(0)?1:0);
}
}
return ret;
......@@ -435,7 +435,7 @@ public class TseitinBasedIntensionCtrEncoder implements IIntensionCtrEncoder {
Iterator<Entry<Integer, Integer>> it2 = mappings.get(1).entrySet().iterator();
while(it2.hasNext()) {
Entry<Integer, Integer> entry2 = it2.next();
buildImplVar(ret, entry1.getValue(), entry2.getValue(), entry1.getKey()!=0 || entry2.getKey()!=0?1:0);
buildImplVar(ret, entry1.getValue(), entry2.getValue(), !entry1.getKey().equals(0) || !entry2.getKey().equals(0)?1:0);
}
}
return ret;
......@@ -451,7 +451,7 @@ public class TseitinBasedIntensionCtrEncoder implements IIntensionCtrEncoder {
Iterator<Entry<Integer, Integer>> it2 = mappings.get(1).entrySet().iterator();
while(it2.hasNext()) {
Entry<Integer, Integer> entry2 = it2.next();
buildImplVar(ret, entry1.getValue(), entry2.getValue(), entry1.getKey()!=0 ^ entry2.getKey()!=0?1:0);
buildImplVar(ret, entry1.getValue(), entry2.getValue(), !entry1.getKey().equals(0) ^ !entry2.getKey().equals(0)?1:0);
}
}
return ret;
......@@ -467,7 +467,7 @@ public class TseitinBasedIntensionCtrEncoder implements IIntensionCtrEncoder {
Iterator<Entry<Integer, Integer>> it2 = mappings.get(1).entrySet().iterator();
while(it2.hasNext()) {
Entry<Integer, Integer> entry2 = it2.next();
buildImplVar(ret, entry1.getValue(), entry2.getValue(), (entry1.getKey()!=0) == (entry2.getKey()!=0)?1:0);
buildImplVar(ret, entry1.getValue(), entry2.getValue(), (!entry1.getKey().equals(0)) == (!entry2.getKey().equals(0))?1:0);
}
}
return ret;
......@@ -483,7 +483,7 @@ public class TseitinBasedIntensionCtrEncoder implements IIntensionCtrEncoder {
Iterator<Entry<Integer, Integer>> it2 = mappings.get(1).entrySet().iterator();
while(it2.hasNext()) {
Entry<Integer, Integer> entry2 = it2.next();
buildImplVar(ret, entry1.getValue(), entry2.getValue(), entry1.getKey()==0 || entry2.getKey()!=0?1:0);
buildImplVar(ret, entry1.getValue(), entry2.getValue(), entry1.getKey().equals(0) || !entry2.getKey().equals(0)?1:0);
}
}
return ret;
......@@ -500,7 +500,7 @@ public class TseitinBasedIntensionCtrEncoder implements IIntensionCtrEncoder {
Iterator<Entry<Integer, Integer>> it3 = mappings.get(2).entrySet().iterator();
while(it3.hasNext()) {
Entry<Integer, Integer> entry3 = it3.next();
buildImplVar(ret, entry1.getValue(), entry2.getValue(), entry3.getValue(), entry1.getKey()!=0?entry2.getKey():entry3.getKey());
buildImplVar(ret, entry1.getValue(), entry2.getValue(), entry3.getValue(), !entry1.getKey().equals(0)?entry2.getKey():entry3.getKey());
}
}
}
......
......@@ -19,7 +19,6 @@
package org.sat4j.reader;
import java.io.BufferedReader;
import java.io.FileNotFoundException;
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
......@@ -101,7 +100,10 @@ public enum ECSPFormat {
if(shouldOnlyDisplayEncoding) {
return pw;
}
XMLCommentPrintWriter commentPrintWriter = new XMLCommentPrintWriter(pw);
if(System.getProperty("CompetitionOutput") != null) {
return pw;
}
final XMLCommentPrintWriter commentPrintWriter = new XMLCommentPrintWriter(pw);
commentPrintWriter.addDncPrefix("v ");
return commentPrintWriter;
}
......
......@@ -21,6 +21,7 @@ package org.sat4j.reader;
import java.io.IOException;
import java.io.InputStream;
import java.io.PrintWriter;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.List;
import java.util.Map;
......@@ -44,6 +45,7 @@ import org.sat4j.csp.intension.ICspToSatEncoder;
import org.sat4j.csp.intension.IIntensionCtrEncoder;
import org.sat4j.csp.intension.IntensionCtrEncoderFactory;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.ObjectiveFunction;
import org.sat4j.pb.PseudoOptDecorator;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IProblem;
......@@ -172,25 +174,31 @@ public class XMLCSP3Reader extends Reader implements XCallbacks2 {
StringBuilder strModelBuffer = new StringBuilder();
switch(this.launcher.getExitCode()) {
case OPTIMUM_FOUND:
final ObjectiveFunction obj = this.solver.getObjectiveFunction();
BigInteger degree = obj.calculateDegree(this.solver);
final BigInteger offset = obj.getCorrectionOffset();
final BigInteger factor = obj.getCorrectionFactor();
degree = degree.multiply(factor).add(offset);
strModelBuffer.append("<instantiation type=\"optimum\" cost=\"")
.append(this.solver.getObjectiveFunction().calculateDegree(this.solver).toString())
.append(degree.toString())
.append("\">\n");
appendModel(strModelBuffer, model);
strModelBuffer.append("v </instantiation>\n");
break;
case UPPER_BOUND:
case SATISFIABLE:
strModelBuffer.append("<instantiation type=\"solution\">\n");
appendModel(strModelBuffer, model);
strModelBuffer.append("v </instantiation>\n");
break;
case UNSATISFIABLE:
strModelBuffer.append(AbstractLauncher.COMMENT_PREFIX).append(" no model");
strModelBuffer.append(AbstractLauncher.COMMENT_PREFIX).append(" no model\n");
break;
case UNKNOWN:
default:
strModelBuffer.append(AbstractLauncher.COMMENT_PREFIX).append(" unknown state");
strModelBuffer.append(AbstractLauncher.COMMENT_PREFIX).append(" unknown state\n");
break;
}
strModelBuffer.append("v </instantiation>");
return strModelBuffer.toString();
}
......@@ -570,6 +578,11 @@ public class XMLCSP3Reader extends Reader implements XCallbacks2 {
this.contradictionFound |= this.countingCtrBuilder.buildCtrSum(id, list, coeffs, condition);
}
@Override
public void buildCtrSum(String id, XVarInteger[] list, XVarInteger[] coeffs, Condition condition) {
this.contradictionFound |= this.countingCtrBuilder.buildCtrSum(id, list, coeffs, condition);
}
/**
* @see XCallbacks2#buildCtrLex(String, XVarInteger[][], TypeOperator)
*/
......@@ -607,7 +620,7 @@ public class XMLCSP3Reader extends Reader implements XCallbacks2 {
*/
@Override
public void buildCtrChannel(String id, XVarInteger[] list, int startIndex, XVarInteger value) {
unimplementedCase(id); // TODO: check (again) set variables are not supported yet
this.contradictionFound |= this.connectionCtrBuilder.buildCtrChannel(id, list, startIndex, value);
}
/**
......@@ -807,7 +820,7 @@ public class XMLCSP3Reader extends Reader implements XCallbacks2 {
*/
@Override
public void buildCtrElement(String id, XVarInteger[] list, int value) {
this.contradictionFound |= this.connectionCtrBuilder.buildCtrElement(id, list, 0, null, TypeRank.ANY, value);
this.contradictionFound |= this.connectionCtrBuilder.buildCtrElement(id, list, value);
}