Commit ccc53e6e authored by leberre's avatar leberre
Browse files

Changed a bit the implementation of AbstractClauseSelector to allow that...

Changed a bit the implementation of AbstractClauseSelector to allow that solver to be used both from the outside (external state) as if the selector variables were forced to false and from power users procedures (internal state) where the power user has the responsibility to make sense of verified selector variables. 

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1676 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent 5f72e810
......@@ -31,9 +31,11 @@ package org.sat4j.tools;
import java.util.Collection;
import org.sat4j.core.VecInt;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.IteratorInt;
import org.sat4j.specs.TimeoutException;
public abstract class AbstractClauseSelectorSolver<T extends ISolver> extends
SolverDecorator<T> {
......@@ -42,6 +44,74 @@ public abstract class AbstractClauseSelectorSolver<T extends ISolver> extends
private int lastCreatedVar;
private boolean pooledVarId = false;
private static interface SelectorState {
boolean isSatisfiable(boolean global) throws TimeoutException;
boolean isSatisfiable() throws TimeoutException;
boolean isSatisfiable(IVecInt assumps) throws TimeoutException;
boolean isSatisfiable(IVecInt assumps, boolean global)
throws TimeoutException;
}
private final SelectorState external = new SelectorState() {
private IVecInt getNegatedSelectors() {
IVecInt assumps = new VecInt();
for (int var : getAddedVars()) {
assumps.push(-var);
}
return assumps;
}
public boolean isSatisfiable(boolean global) throws TimeoutException {
return decorated().isSatisfiable(getNegatedSelectors(), global);
}
public boolean isSatisfiable(IVecInt assumps, boolean global)
throws TimeoutException {
IVecInt all = getNegatedSelectors();
assumps.copyTo(all);
return decorated().isSatisfiable(all, global);
}
public boolean isSatisfiable() throws TimeoutException {
return decorated().isSatisfiable(getNegatedSelectors());
}
public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
IVecInt all = getNegatedSelectors();
assumps.copyTo(all);
return decorated().isSatisfiable(all);
}
};
private final SelectorState internal = new SelectorState() {
public boolean isSatisfiable(boolean global) throws TimeoutException {
return decorated().isSatisfiable(global);
}
public boolean isSatisfiable() throws TimeoutException {
return decorated().isSatisfiable();
}
public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
return decorated().isSatisfiable(assumps);
}
public boolean isSatisfiable(IVecInt assumps, boolean global)
throws TimeoutException {
return decorated().isSatisfiable(assumps, global);
}
};
private SelectorState selectedState = external;
public AbstractClauseSelectorSolver(T solver) {
super(solver);
}
......@@ -72,4 +142,45 @@ public abstract class AbstractClauseSelectorSolver<T extends ISolver> extends
protected void discardLastestVar() {
this.pooledVarId = true;
}
@Override
public boolean isSatisfiable(boolean global) throws TimeoutException {
return selectedState.isSatisfiable(global);
}
@Override
public boolean isSatisfiable(IVecInt assumps, boolean global)
throws TimeoutException {
return selectedState.isSatisfiable(assumps, global);
}
@Override
public boolean isSatisfiable() throws TimeoutException {
return selectedState.isSatisfiable();
}
@Override
public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
return selectedState.isSatisfiable(assumps);
}
/**
* In the internal state, the solver will allow the selector variables to be
* satisfied. As such, the solver will answer "true" to isSatisfiable() on
* an UNSAT problem. it is the responsibility of the user to take into
* account the meaning of the selector variables.
*/
public void internalState() {
this.selectedState = internal;
}
/**
* In external state, the solver will prevent the selector variables to be
* satisfied. As a consequence, from an external point of view, an UNSAT
* problem will answer "false" to isSatisfiable().
*/
public void externalState() {
this.selectedState = external;
}
}
......@@ -96,7 +96,7 @@ public class AllMUSes {
*/
public List<IVecInt> computeAllMUSes(SolutionFoundListener listener) {
computeAllMSS();
css.internalState();
ISolver solver = SolverFactory.newDefault();
IVecInt mus;
......@@ -134,9 +134,7 @@ public class AllMUSes {
} catch (TimeoutException e) {
e.printStackTrace();
}
System.out.println("MUSes = " + musList);
css.externalState();
return musList;
}
......@@ -145,6 +143,7 @@ public class AllMUSes {
}
public List<IVecInt> computeAllMSS(SolutionFoundListener listener) {
css.internalState();
int nVar = css.nVars();
IVecInt pLits = new VecInt();
......@@ -201,9 +200,7 @@ public class AllMUSes {
} catch (ContradictionException e) {
}
System.out.println("MSS = " + mssList);
css.externalState();
return mssList;
}
}
......@@ -92,7 +92,8 @@ public class HighLevelXplain<T extends ISolver> extends
if (solver instanceof SolverDecorator<?>) {
solver = ((SolverDecorator<? extends ISolver>) solver).decorated();
}
return this.xplainStrategy.explain(solver, this.varToHighLevel, this.assump);
return this.xplainStrategy.explain(solver, this.varToHighLevel,
this.assump);
}
public int[] minimalExplanation() throws TimeoutException {
......@@ -130,65 +131,38 @@ public class HighLevelXplain<T extends ISolver> extends
@Override
public int[] findModel() throws TimeoutException {
this.assump = VecInt.EMPTY;
IVecInt extraVariables = new VecInt();
for (Integer p : this.varToHighLevel.keySet()) {
extraVariables.push(-p);
}
return super.findModel(extraVariables);
return super.findModel();
}
@Override
public int[] findModel(IVecInt assumps) throws TimeoutException {
this.assump = assumps;
IVecInt extraVariables = new VecInt();
assumps.copyTo(extraVariables);
for (Integer p : this.varToHighLevel.keySet()) {
extraVariables.push(-p);
}
return super.findModel(extraVariables);
return super.findModel(assumps);
}
@Override
public boolean isSatisfiable() throws TimeoutException {
this.assump = VecInt.EMPTY;
IVecInt extraVariables = new VecInt();
for (Integer p : this.varToHighLevel.keySet()) {
extraVariables.push(-p);
}
return super.isSatisfiable(extraVariables);
return super.isSatisfiable();
}
@Override
public boolean isSatisfiable(boolean global) throws TimeoutException {
this.assump = VecInt.EMPTY;
IVecInt extraVariables = new VecInt();
for (Integer p : this.varToHighLevel.keySet()) {
extraVariables.push(-p);
}
return super.isSatisfiable(extraVariables, global);
return super.isSatisfiable(global);
}
@Override
public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
this.assump = assumps;
IVecInt extraVariables = new VecInt();
assumps.copyTo(extraVariables);
for (Integer p : this.varToHighLevel.keySet()) {
extraVariables.push(-p);
}
return super.isSatisfiable(extraVariables);
return super.isSatisfiable(assumps);
}
@Override
public boolean isSatisfiable(IVecInt assumps, boolean global)
throws TimeoutException {
this.assump = assumps;
IVecInt extraVariables = new VecInt();
assumps.copyTo(extraVariables);
for (Integer p : this.varToHighLevel.keySet()) {
extraVariables.push(-p);
}
return super.isSatisfiable(extraVariables, global);
return super.isSatisfiable(assumps, global);
}
@Override
......
......@@ -165,65 +165,38 @@ public class Xplain<T extends ISolver> extends FullClauseSelectorSolver<T>
@Override
public int[] findModel() throws TimeoutException {
this.assump = VecInt.EMPTY;
IVecInt extraVariables = new VecInt();
for (Integer p : this.constrs.keySet()) {
extraVariables.push(-p);
}
return super.findModel(extraVariables);
return super.findModel();
}
@Override
public int[] findModel(IVecInt assumps) throws TimeoutException {
this.assump = assumps;
IVecInt extraVariables = new VecInt();
assumps.copyTo(extraVariables);
for (Integer p : this.constrs.keySet()) {
extraVariables.push(-p);
}
return super.findModel(extraVariables);
return super.findModel(assumps);
}
@Override
public boolean isSatisfiable() throws TimeoutException {
this.assump = VecInt.EMPTY;
IVecInt extraVariables = new VecInt();
for (Integer p : this.constrs.keySet()) {
extraVariables.push(-p);
}
return super.isSatisfiable(extraVariables);
return super.isSatisfiable();
}
@Override
public boolean isSatisfiable(boolean global) throws TimeoutException {
this.assump = VecInt.EMPTY;
IVecInt extraVariables = new VecInt();
for (Integer p : this.constrs.keySet()) {
extraVariables.push(-p);
}
return super.isSatisfiable(extraVariables, global);
return super.isSatisfiable(global);
}
@Override
public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
this.assump = assumps;
IVecInt extraVariables = new VecInt();
assumps.copyTo(extraVariables);
for (Integer p : this.constrs.keySet()) {
extraVariables.push(-p);
}
return super.isSatisfiable(extraVariables);
return super.isSatisfiable(assumps);
}
@Override
public boolean isSatisfiable(IVecInt assumps, boolean global)
throws TimeoutException {
this.assump = assumps;
IVecInt extraVariables = new VecInt();
assumps.copyTo(extraVariables);
for (Integer p : this.constrs.keySet()) {
extraVariables.push(-p);
}
return super.isSatisfiable(extraVariables, global);
return super.isSatisfiable(assumps, global);
}
@Override
......
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