Commit ccb9a65d authored by Lonca Emmanuel's avatar Lonca Emmanuel

Fixed sign of returned optimum value.

parent 0ffb0c7e
......@@ -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) {
......@@ -208,6 +210,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,6 +226,7 @@ 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();
}
......@@ -231,6 +235,7 @@ public class ObjBuilder {
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])));
......
......@@ -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,8 +174,14 @@ 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 correction = obj.getCorrection();
if(!correction.equals(BigInteger.ZERO)) {
degree = degree.multiply(correction);
}
strModelBuffer.append("<instantiation type=\"optimum\" cost=\"")
.append(this.solver.getObjectiveFunction().calculateDegree(this.solver).toString())
.append(degree.toString())
.append("\">\n");
appendModel(strModelBuffer, model);
break;
......
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