Commit 68e1622f authored by lonca's avatar lonca
Browse files

SAt4j-csp now displays the mapping between CSP and SAT variables ; this...

SAt4j-csp now displays the mapping between CSP and SAT variables ; this behavior should be set back off in case of a "real solving" (that is solver is not abstract)

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@2529 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent 48fedbfb
......@@ -18,10 +18,16 @@
*******************************************************************************/
package org.sat4j.csp;
import java.io.IOException;
import java.util.Map;
import org.sat4j.AbstractLauncher;
import org.sat4j.ILauncherMode;
import org.sat4j.reader.ECSPFormat;
import org.sat4j.reader.ParseFormatException;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IProblem;
import org.sat4j.specs.ISolver;
public class CSPLauncher extends AbstractLauncher {
......@@ -77,6 +83,29 @@ public class CSPLauncher extends AbstractLauncher {
return aReader;
}
@Override
protected IProblem readProblem(String problemname)
throws ParseFormatException, IOException, ContradictionException {
this.silent = true;
IProblem problem = super.readProblem(problemname);
if(this.reader.hasAMapping()) {
this.out.write("c CSP to SAT var mapping:");
Map<Integer, String> mapping = this.reader.getMapping();
String lastVar="";
for(Map.Entry<Integer, String> entry : mapping.entrySet()) {
final String curVarAssignment = entry.getValue();
final String curVar = curVarAssignment.substring(0, curVarAssignment.indexOf("="));
if(!curVar.equals(lastVar)) {
this.out.write("\nc ");
}
this.out.write(curVarAssignment+":"+entry.getKey()+" ");
lastVar = curVar;
}
this.out.write("\n");
}
return problem;
}
public static void main(String[] args) {
AbstractLauncher lanceur = new CSPLauncher();
if (args.length > 2 || args.length == 0) {
......
......@@ -3,6 +3,8 @@ package org.sat4j.csp.intension;
import java.util.Arrays;
import java.util.LinkedHashMap;
import java.util.Map;
import java.util.SortedMap;
import java.util.TreeMap;
import org.sat4j.core.VecInt;
import org.sat4j.csp.Domain;
......@@ -99,5 +101,18 @@ public class CspToPBSolverDecorator implements ICspToSatEncoder {
}
this.varmapping.put(var.id, cspVar);
}
@Override
public Map<Integer, String> getMapping() {
final SortedMap<Integer, String> mapping = new TreeMap<>();
for(String var : this.varmapping.keySet()) {
int[] domain = getCspVarDomain(var);
for(int i=0; i<domain.length; ++i) {
final int solverVar = getSolverVar(var, domain[i]);
mapping.put(solverVar, var+"="+domain[i]);
}
}
return mapping;
}
}
package org.sat4j.csp.intension;
import java.util.Map;
import org.xcsp.parser.entries.XVariables.XVarInteger;
public interface ICspToSatEncoder {
......@@ -10,6 +12,8 @@ public interface ICspToSatEncoder {
Integer newSatSolverVar();
Map<Integer, String> getMapping();
void newCspVar(XVarInteger var, int[] dom);
void newCspVar(XVarInteger var, int minDom, int maxDom);
......
......@@ -23,6 +23,7 @@ import java.io.InputStream;
import java.io.PrintWriter;
import java.util.ArrayList;
import java.util.List;
import java.util.Map;
import java.util.Set;
import javax.xml.parsers.DocumentBuilderFactory;
......@@ -251,6 +252,21 @@ public class XMLCSP3Reader extends Reader implements XCallbacks2 {
}
}
@Override
public boolean hasAMapping() {
return true;
}
@Override
public Map<Integer, String> getMapping() {
return this.cspToSatEncoder.getMapping();
}
@Override
public boolean isUsingMapping() {
return true;
}
/**
* @see Reader#parseInstance(InputStream)
*/
......
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