Commit 046a69eb authored by leberre's avatar leberre

Fixed a bug in newVar(int) and return a fake constr instead of null to not...

Fixed a bug in newVar(int) and return a fake constr instead of null to not break client code (null usually means that the constraint is trivially satisfied).

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@291 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent bdf153e6
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*
* Based on the original MiniSat specification from:
*
* An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
* Sixth International Conference on Theory and Applications of Satisfiability
* Testing, LNCS 2919, pp 502-518, 2003.
*
* See www.minisat.se for the original solver in C++.
*
*******************************************************************************/
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*
* Based on the original MiniSat specification from:
*
* An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
* Sixth International Conference on Theory and Applications of Satisfiability
* Testing, LNCS 2919, pp 502-518, 2003.
*
* See www.minisat.se for the original solver in C++.
*
*******************************************************************************/
package org.sat4j.pb;
import java.math.BigInteger;
......@@ -50,11 +50,29 @@ public class OPBStringSolver extends DimacsStringSolver implements IPBSolver {
*
*/
private static final long serialVersionUID = 1L;
private int indxConstrObj;
private int nbOfConstraints;
private static IConstr FAKE_CONSTR = new IConstr(){
public int size() {
throw new UnsupportedOperationException("Fake IConstr");
}
public boolean learnt() {
throw new UnsupportedOperationException("Fake IConstr");
}
public double getActivity() {
throw new UnsupportedOperationException("Fake IConstr");
}
public int get(int i) {
throw new UnsupportedOperationException("Fake IConstr");
}
};
/**
*
*/
......@@ -72,31 +90,30 @@ public class OPBStringSolver extends DimacsStringSolver implements IPBSolver {
boolean moreThan, BigInteger d) throws ContradictionException {
StringBuffer out = getOut();
assert lits.size() == coeffs.size();
nbOfConstraints ++;
nbOfConstraints++;
if (moreThan) {
for (int i = 0; i <lits.size();i++)
out.append(coeffs.get(i)+" x"+ lits.get(i) + " ");
out.append(">= "+d+" ;\n");
for (int i = 0; i < lits.size(); i++)
out.append(coeffs.get(i) + " x" + lits.get(i) + " ");
out.append(">= " + d + " ;\n");
} else {
for (int i = 0; i < lits.size(); i++)
out.append(coeffs.get(i).negate() + " x" + lits.get(i) + " ");
out.append(">= " + d.negate() + " ;\n");
}
else {
for (int i = 0; i <lits.size();i++)
out.append(coeffs.get(i).negate()+" x"+ lits.get(i) + " ");
out.append(">= "+d.negate()+" ;\n");
}
return null;
return FAKE_CONSTR;
}
public void setObjectiveFunction(ObjectiveFunction obj) {
StringBuffer out = getOut();
StringBuffer tmp = new StringBuffer();
tmp.append(" #constraint= "+nbOfConstraints+" \n");
tmp.append(" #constraint= " + nbOfConstraints + " \n");
tmp.append("min : ");
IVecInt lits = obj.getVars();
IVec<BigInteger> coeffs = obj.getCoeffs();
for (int i = 0; i <lits.size();i++)
tmp.append(coeffs.get(i)+" x"+ lits.get(i) + " ");
for (int i = 0; i < lits.size(); i++)
tmp.append(coeffs.get(i) + " x" + lits.get(i) + " ");
tmp.append(" ;\n");
out.insert(indxConstrObj,tmp);
out.insert(indxConstrObj, tmp);
}
@Override
......@@ -104,10 +121,10 @@ public class OPBStringSolver extends DimacsStringSolver implements IPBSolver {
throws ContradictionException {
StringBuffer out = getOut();
nbOfConstraints++;
for (IteratorInt iterator = literals.iterator();iterator.hasNext();)
out.append("+1 x"+iterator.next() + " ");
out.append(">= "+degree+" ;\n");
return null;
for (IteratorInt iterator = literals.iterator(); iterator.hasNext();)
out.append("+1 x" + iterator.next() + " ");
out.append(">= " + degree + " ;\n");
return FAKE_CONSTR;
}
@Override
......@@ -115,23 +132,32 @@ public class OPBStringSolver extends DimacsStringSolver implements IPBSolver {
throws ContradictionException {
StringBuffer out = getOut();
nbOfConstraints++;
for (IteratorInt iterator = literals.iterator();iterator.hasNext();)
out.append("-1 x"+iterator.next() + " ");
out.append(">= "+(-degree)+" ;\n");
return null;
for (IteratorInt iterator = literals.iterator(); iterator.hasNext();)
out.append("-1 x" + iterator.next() + " ");
out.append(">= " + (-degree) + " ;\n");
return FAKE_CONSTR;
}
@Override
public IConstr addClause(IVecInt literals) throws ContradictionException {
StringBuffer out = getOut();
nbOfConstraints++;
for (IteratorInt iterator = literals.iterator();iterator.hasNext();)
out.append("+1 x"+iterator.next() + " ");
out.append(">= 1 ;\n");
return null;
int lit;
for (IteratorInt iterator = literals.iterator(); iterator.hasNext();) {
lit = iterator.next();
if (lit > 0) {
out.append("+1 x" + lit + " ");
} else {
out.append("+1 ~x" + -lit + " ");
}
}
out.append(">= 1 ;\n");
return FAKE_CONSTR;
}
/* (non-Javadoc)
/*
* (non-Javadoc)
*
* @see org.sat4j.pb.IPBSolver#getExplanation()
*/
public String getExplanation() {
......@@ -139,38 +165,40 @@ public class OPBStringSolver extends DimacsStringSolver implements IPBSolver {
return null;
}
/* (non-Javadoc)
* @see org.sat4j.pb.IPBSolver#setListOfVariablesForExplanation(org.sat4j.specs.IVecInt)
/*
* (non-Javadoc)
*
* @see
* org.sat4j.pb.IPBSolver#setListOfVariablesForExplanation(org.sat4j.specs
* .IVecInt)
*/
public void setListOfVariablesForExplanation(IVecInt listOfVariables) {
// TODO Auto-generated method stub
}
@Override
public String toString(){
public String toString() {
return getOut().toString();
}
@Override
public String toString(String prefix) {
return "OPB output solver";
return "OPB output solver";
}
@Override
@Override
public int newVar(int howmany) {
StringBuffer out = getOut();
out.append("* #variable= " + howmany);
setNbVars(howmany);
// to add later the number of constraints
indxConstrObj = out.length();
return 0;
}
@Override
public void setExpectedNumberOfClauses(int nb) {
}
out.append("* #variable= " + howmany);
setNbVars(howmany);
// to add later the number of constraints
indxConstrObj = out.length();
return howmany;
}
@Override
public void setExpectedNumberOfClauses(int nb) {
}
}
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