Commit a21ed8d6 authored by leberre's avatar leberre
Browse files

Added objective function to the input.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1673 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent 04aae9be
package org.sat4j.pb.reader;
import java.math.BigInteger;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.ObjectiveFunction;
import org.sat4j.reader.JSONReader;
import org.sat4j.reader.ParseFormatException;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
public class JSONPBReader extends JSONReader<IPBSolver> {
......@@ -15,9 +19,13 @@ public class JSONPBReader extends JSONReader<IPBSolver> {
public static final String WCLAUSE = "(\\[(" + WLITERAL + "(," + WLITERAL
+ ")*)?\\])";
public static final String PB = "(\\[" + WCLAUSE + ",'[=<>]=?',-?\\d+\\])";
public static final String OBJ = "(\\[('min'|'max')," + WCLAUSE + "\\])";
public static final Pattern pseudo = Pattern.compile(PB);
public static final Pattern wclause = Pattern.compile(WCLAUSE);
public static final Pattern wliteral = Pattern.compile(WLITERAL);
public static final Pattern obj = Pattern.compile(OBJ);
public JSONPBReader(IPBSolver solver) {
super(solver);
......@@ -28,12 +36,35 @@ public class JSONPBReader extends JSONReader<IPBSolver> {
throws ParseFormatException, ContradictionException {
if (pseudo.matcher(constraint).matches()) {
handlePB(constraint);
} else if (obj.matcher(constraint).matches()) {
handleObj(constraint);
} else {
throw new UnsupportedOperationException("Wrong formula "
+ constraint);
}
}
private void handleObj(String constraint) {
Matcher matcher = wclause.matcher(constraint);
if (matcher.find()) {
String wclause = matcher.group();
constraint = matcher.replaceFirst("");
matcher = wliteral.matcher(wclause);
IVecInt literals = new VecInt();
String[] pieces = constraint.split(",");
boolean negate = pieces[0].contains("max");
IVec<BigInteger> coefs = new Vec<BigInteger>();
BigInteger coef;
while (matcher.find()) {
literals.push(Integer.valueOf(matcher.group(2)));
coef = new BigInteger(matcher.group(1));
coefs.push(negate ? coef.negate() : coef);
}
solver.setObjectiveFunction(new ObjectiveFunction(literals, coefs));
}
}
private void handlePB(String constraint) throws ContradictionException {
Matcher matcher = wclause.matcher(constraint);
if (matcher.find()) {
......@@ -68,7 +99,6 @@ public class JSONPBReader extends JSONReader<IPBSolver> {
@Override
protected String constraintPattern() {
return "(" + CLAUSE + "|" + CARD + "|" + PB + ")";
return "(" + CLAUSE + "|" + CARD + "|" + PB + "|" + OBJ + ")";
}
}
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