Commit a55071dd authored by lonca's avatar lonca
Browse files

Made some adjustments in order to be compatible with the new version of XCSP3 API.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@2548 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent 1bf3594d
......@@ -103,7 +103,7 @@ public class CSPLauncher extends AbstractLauncher {
this.out.write("c CSP to SAT var mapping:\n");
Map<Integer, String> mapping = this.reader.getMapping();
for(Map.Entry<Integer, String> entry : mapping.entrySet()) {
this.out.write(entry.getValue()+";"+entry.getKey()+"\n");
this.out.write("c "+entry.getValue()+";"+entry.getKey()+"\n");
}
}
}
......
......@@ -23,7 +23,7 @@ import java.util.TreeSet;
import org.sat4j.csp.intension.IIntensionCtrEncoder;
import org.sat4j.reader.XMLCSP3Reader;
import org.xcsp.common.Types.TypeOperator;
import org.xcsp.common.Types.TypeOperatorRel;
import org.xcsp.parser.entries.XVariables.XVarInteger;
/**
......@@ -130,7 +130,7 @@ public class ComparisonCtrBuilder {
return false;
}
public boolean buildCtrOrdered(String id, XVarInteger[] list, TypeOperator operator) {
public boolean buildCtrOrdered(String id, XVarInteger[] list, TypeOperatorRel operator) {
for(int i=0; i<list.length-1; ++i) {
String normalized1 = CtrBuilderUtils.normalizeCspVarName(list[i].id);
String normalized2 = CtrBuilderUtils.normalizeCspVarName(list[i+1].id);
......@@ -140,7 +140,7 @@ public class ComparisonCtrBuilder {
return false;
}
public boolean buildCtrLex(String id, XVarInteger[][] lists, TypeOperator operator) {
public boolean buildCtrLex(String id, XVarInteger[][] lists, TypeOperatorRel operator) {
boolean contradictionFound = false;
for(int i=0; i<lists.length-1; ++i) {
contradictionFound |= buildCtrLex(id, lists[i], lists[i+1], operator);
......@@ -148,7 +148,7 @@ public class ComparisonCtrBuilder {
return contradictionFound;
}
public boolean buildCtrLexMatrix(String id, XVarInteger[][] matrix, TypeOperator operator) {
public boolean buildCtrLexMatrix(String id, XVarInteger[][] matrix, TypeOperatorRel operator) {
boolean contradictionFound = false;
contradictionFound |= buildCtrLex(id, matrix, operator);
XVarInteger[][] tMatrix = CtrBuilderUtils.transposeMatrix(matrix);
......@@ -157,8 +157,8 @@ public class ComparisonCtrBuilder {
}
private boolean buildCtrLex(String id, XVarInteger[] list1,
XVarInteger[] list2, TypeOperator operator) {
TypeOperator strictOp = CtrBuilderUtils.strictTypeOperator(operator);
XVarInteger[] list2, TypeOperatorRel operator) {
TypeOperatorRel strictOp = CtrBuilderUtils.strictTypeOperator(operator);
String[] chains = new String[list1.length];
String id01 = list1[0].id;
String id02 = list2[0].id;
......
......@@ -28,7 +28,10 @@ import org.sat4j.csp.Var;
import org.sat4j.pb.IPBSolver;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVec;
import org.xcsp.common.Types.TypeOperator;
import org.xcsp.common.Types.TypeOperatorRel;
import org.xcsp.common.predicates.XNode;
import org.xcsp.common.predicates.XNodeLeaf;
import org.xcsp.common.predicates.XNodeParent;
import org.xcsp.parser.entries.XVariables.XVarInteger;
/**
......@@ -109,14 +112,35 @@ public class CtrBuilderUtils {
return false;
}
public static TypeOperator strictTypeOperator(TypeOperator op) {
public static TypeOperatorRel strictTypeOperator(TypeOperatorRel op) {
switch(op) {
case GE: return TypeOperator.GT;
case LE: return TypeOperator.LT;
case SUBSEQ: return TypeOperator.SUBSET;
case SUPSEQ: return TypeOperator.SUPSET;
case GE: return TypeOperatorRel.GT;
case LE: return TypeOperatorRel.LT;
default: return op;
}
}
public static String syntaxTreeRootToString(final XNodeParent<XVarInteger> syntaxTreeRoot) {
final StringBuffer treeToString = new StringBuffer();
fillSyntacticStrBuffer(syntaxTreeRoot, treeToString);
return treeToString.toString();
}
private static void fillSyntacticStrBuffer(final XNode<XVarInteger> child,
final StringBuffer treeToString) {
if(child instanceof XNodeLeaf<?>) {
treeToString.append(CtrBuilderUtils.normalizeCspVarName(child.toString()));
return;
}
treeToString.append(child.getType().toString().toLowerCase());
final XNode<XVarInteger>[] sons = ((XNodeParent<XVarInteger>) child).sons;
treeToString.append('(');
fillSyntacticStrBuffer(sons[0], treeToString);
for(int i=1; i<sons.length; ++i) {
treeToString.append(',');
fillSyntacticStrBuffer(sons[i], treeToString);
}
treeToString.append(')');
}
}
......@@ -29,8 +29,6 @@ import org.sat4j.csp.intension.ICspToSatEncoder;
import org.sat4j.csp.intension.IIntensionCtrEncoder;
import org.sat4j.reader.XMLCSP3Reader;
import org.xcsp.common.Types.TypeFlag;
import org.xcsp.common.predicates.XNode;
import org.xcsp.common.predicates.XNodeLeaf;
import org.xcsp.common.predicates.XNodeParent;
import org.xcsp.parser.entries.XDomains.XDomInteger;
import org.xcsp.parser.entries.XValues.IntegerEntity;
......@@ -49,41 +47,17 @@ public class GenericCtrBuilder {
private final ICspToSatEncoder cspToSatSolver;
public GenericCtrBuilder(ICspToSatEncoder cspToSatEncoder, IIntensionCtrEncoder intensionEnc) {
this.cspToSatSolver = cspToSatEncoder;
public GenericCtrBuilder(IIntensionCtrEncoder intensionEnc) {
this.intensionCtrEnc = intensionEnc;
this.cspToSatSolver = intensionEnc.getSolver();
}
public boolean buildCtrIntension(String id, XVarInteger[] xscope, XNodeParent<XVarInteger> syntaxTreeRoot) {
syntaxTreeRootToString(syntaxTreeRoot);
String expr = syntaxTreeRootToString(syntaxTreeRoot);
String expr = CtrBuilderUtils.syntaxTreeRootToString(syntaxTreeRoot);
this.intensionCtrEnc.encode(expr);
return false;
}
private String syntaxTreeRootToString(XNodeParent<XVarInteger> syntaxTreeRoot) {
StringBuffer treeToString = new StringBuffer();
fillSyntacticStrBuffer(syntaxTreeRoot, treeToString);
return treeToString.toString();
}
private void fillSyntacticStrBuffer(XNode<XVarInteger> child,
StringBuffer treeToString) {
if(child instanceof XNodeLeaf<?>) {
treeToString.append(CtrBuilderUtils.normalizeCspVarName(child.toString()));
return;
}
treeToString.append(child.getType().toString().toLowerCase());
XNode<XVarInteger>[] sons = ((XNodeParent<XVarInteger>) child).sons;
treeToString.append('(');
fillSyntacticStrBuffer(sons[0], treeToString);
for(int i=1; i<sons.length; ++i) {
treeToString.append(',');
fillSyntacticStrBuffer(sons[i], treeToString);
}
treeToString.append(')');
}
public boolean buildCtrExtension(String id, XVarInteger x, int[] values, boolean positive, Set<TypeFlag> flags) {
XVarInteger[] xArr = new XVarInteger[]{x};
int nVals = values.length;
......
......@@ -47,11 +47,11 @@ public class StringCondition {
}
public StringCondition(ConditionVal condition) {
this.asString = condition.operator.name().toLowerCase()+"("+LEFT_OPERAND+","+Integer.toString(((ConditionVal)condition).k)+")";
this.asString = condition.operator.name().toLowerCase()+"("+LEFT_OPERAND+","+Long.toString(((ConditionVal)condition).k)+")";
}
public StringCondition(ConditionIntvl condition) {
this.asString = "and(ge("+LEFT_OPERAND+","+Integer.toString(condition.min)+"),le("+LEFT_OPERAND+","+Integer.toString(condition.max)+"))";
this.asString = "and(ge("+LEFT_OPERAND+","+Long.toString(condition.min)+"),le("+LEFT_OPERAND+","+Long.toString(condition.max)+"))";
}
public StringCondition(String str) {
......
......@@ -53,6 +53,7 @@ import org.xcsp.common.Types.TypeConditionOperatorRel;
import org.xcsp.common.Types.TypeFlag;
import org.xcsp.common.Types.TypeObjective;
import org.xcsp.common.Types.TypeOperator;
import org.xcsp.common.Types.TypeOperatorRel;
import org.xcsp.common.Types.TypeRank;
import org.xcsp.common.predicates.XNodeParent;
import org.xcsp.parser.XCallbacks2;
......@@ -132,10 +133,10 @@ public class XMLCSP3Reader extends Reader implements XCallbacks2 {
this.comparisonCtrBuilder = new ComparisonCtrBuilder(this.intensionEnc);
this.connectionCtrBuilder = new ConnectionCtrBuilder(this.intensionEnc);
this.schedulingCtrBuilder = new SchedulingCtrBuilder(this.intensionEnc);
this.genericCtrBuilder = new GenericCtrBuilder(this.cspToSatEncoder, this.intensionEnc);
this.genericCtrBuilder = new GenericCtrBuilder(this.intensionEnc);
this.countingCtrBuilder = new CountingCtrBuilder(this.intensionEnc);
this.languageCtrBuilder = new LanguageCtrBuilder(this.cspToSatEncoder);
// this.objBuilder = new ObjBuilder(solver, this.cspToSatEncoder.getVarmapping(), this.cspToSatEncoder.getFirstInternalVarMapping());
this.objBuilder = new ObjBuilder(solver, this.intensionEnc);
}
/**
......@@ -438,7 +439,7 @@ public class XMLCSP3Reader extends Reader implements XCallbacks2 {
*/
@Override
public void buildObjToMinimize(String id, XVarInteger x) {
this.objBuilder.buildObjToMaximize(id, x); // TODO not under test yet
this.objBuilder.buildObjToMinimize(id, x); // TODO not under test yet
}
/**
......@@ -470,7 +471,7 @@ public class XMLCSP3Reader extends Reader implements XCallbacks2 {
*/
@Override
public void buildObjToMinimize(String id, XNodeParent<XVarInteger> syntaxTreeRoot) {
unimplementedCase(id); // TODO
this.objBuilder.buildObjToMinimize(id, syntaxTreeRoot);
}
/**
......@@ -478,7 +479,7 @@ public class XMLCSP3Reader extends Reader implements XCallbacks2 {
*/
@Override
public void buildObjToMaximize(String id, XNodeParent<XVarInteger> syntaxTreeRoot) {
unimplementedCase(id); // TODO
this.objBuilder.buildObjToMaximize(id, syntaxTreeRoot);
}
/**
......@@ -533,7 +534,7 @@ public class XMLCSP3Reader extends Reader implements XCallbacks2 {
* @see XCallbacks2#buildCtrOrdered(String, XVarInteger[], TypeOperator)
*/
@Override
public void buildCtrOrdered(String id, XVarInteger[] list, TypeOperator operator) {
public void buildCtrOrdered(String id, XVarInteger[] list, TypeOperatorRel operator) {
this.contradictionFound |= this.comparisonCtrBuilder.buildCtrOrdered(id, list, operator);
}
......@@ -555,7 +556,7 @@ public class XMLCSP3Reader extends Reader implements XCallbacks2 {
* @see XCallbacks2#buildCtrLex(String, XVarInteger[][], TypeOperator)
*/
@Override
public void buildCtrLex(String id, XVarInteger[][] lists, TypeOperator operator) {
public void buildCtrLex(String id, XVarInteger[][] lists, TypeOperatorRel operator) {
this.contradictionFound |= this.comparisonCtrBuilder.buildCtrLex(id, lists, operator);
}
......@@ -563,7 +564,7 @@ public class XMLCSP3Reader extends Reader implements XCallbacks2 {
* @see XCallbacks2#buildCtrLexMatrix(String, XVarInteger[][], TypeOperator)
*/
@Override
public void buildCtrLexMatrix(String id, XVarInteger[][] matrix, TypeOperator operator) {
public void buildCtrLexMatrix(String id, XVarInteger[][] matrix, TypeOperatorRel operator) {
this.contradictionFound |= this.comparisonCtrBuilder.buildCtrLexMatrix(id, matrix, operator);
}
......
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