Commit fd8ceafe authored by lonca's avatar lonca

Provided the capability of change the value of a fixed variable : if user type...

Provided the capability of change the value of a fixed variable : if user type vx=y and then vx=z, vx=y is forgotten instead of launching an error. To keep the old behavior, add the "-replacementForbidden" flag in the command line.
Changes have made the scenario simulator incorrect ; it has been temporally removed.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@2041 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent cdba1a93
package org.sat4j.br4cp;
import java.util.Iterator;
import java.util.Set;
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;
import org.sat4j.tools.Backbone;
/**
* A class used to compile propagation in configuration problem due to
* assumptions. This class uses assumptions to keep informations. Although it is
* efficient to chain assumptions ("scenarios"), this class should get
* efficiency issues while canceling first assumptions.
*
* @author lonca
*/
public class AssumptionsBasedBr4cpBackboneComputer extends DefaultBr4cpBackboneComputer {
public AssumptionsBasedBr4cpBackboneComputer(ISolver solver,
ConfigVarMap idMap) throws TimeoutException {
super(solver, idMap);
}
@Override
protected IVecInt computeBackbone(ISolver solver) throws TimeoutException {
IVecInt assumps = new VecInt();
for (Iterator<Set<Integer>> it = solverAssumptions.iterator(); it
.hasNext();) {
for (Iterator<Integer> it2 = it.next().iterator(); it2.hasNext();)
assumps.push(it2.next());
}
if (!this.backbonesStack.isEmpty()) {
for (IteratorInt it = this.backbonesStack.peek().iterator(); it
.hasNext();) {
int next = it.next();
assumps.push(next);
}
}
return Backbone.compute(solver, assumps);
}
}
......@@ -5,10 +5,9 @@ import java.io.IOException;
import java.io.InputStreamReader;
import java.io.PrintStream;
import java.lang.reflect.Method;
import java.util.ArrayList;
import java.util.Iterator;
import java.util.List;
import java.util.Set;
import java.util.TreeSet;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
......@@ -25,11 +24,12 @@ public class Br4cpCLI {
private PrintStream outStream;
private boolean quit = false;
IBr4cpBackboneComputer backboneComputer;
private List<String> assumptions = new ArrayList<String>();
private final AllMUSes muses = new AllMUSes(true,SolverFactory.instance());
private Set<String> assumptions = new TreeSet<String>(
new ConfigVarComparator());
private final AllMUSes muses = new AllMUSes(true, SolverFactory.instance());
private Br4cpAraliaReader reader;
public Br4cpCLI(String instance) throws Exception {
solver = muses.getSolverInstance();
varMap = new ConfigVarMap(solver);
......@@ -37,66 +37,62 @@ public class Br4cpCLI {
readInstance(instance, solver, varMap);
long startTime = System.currentTimeMillis();
this.outStream.println("computing problem backbone...");
backboneComputer = Options.getInstance().getBackboneComputer(solver, varMap);
printNewlyAsserted(backboneComputer, this.solver.getLogPrefix()
+ "rootPropagated:", this.solver.getLogPrefix()
+ "rootReduced:");
backboneComputer = Options.getInstance().getBackboneComputer(solver,
varMap);
printAsserted(backboneComputer, "rootPropagated:", "rootReduced:");
this.outStream.printf("done in %.3fs.\n\n",
(System.currentTimeMillis() - startTime) / 1000.);
runCLI();
}
private void readInstance(String instance, IGroupSolver solver,
ConfigVarMap varMap) {
reader = new Br4cpAraliaReader(solver, varMap);
try {
reader.parseInstance(instance);
} catch (IOException e) {
e.printStackTrace();
System.exit(1);
}
}
private void printNewlyAsserted(IBr4cpBackboneComputer backboneComputer) {
printNewlyAsserted(backboneComputer, this.solver.getLogPrefix()
+ "propagated :", this.solver.getLogPrefix() + "reduced :");
}
private void printNewlyAsserted(IBr4cpBackboneComputer backboneComputer,
String asserted, String removed) {
Set<String> newlyAsserted = backboneComputer.newPropagatedConfigVars();
Set<String> newBooleanAssertions = backboneComputer
.newPropagatedAdditionalVars();
if (!newlyAsserted.isEmpty() || !newBooleanAssertions.isEmpty()) {
this.outStream.print(asserted);
for (String s : newlyAsserted) {
private void printAsserted(IBr4cpBackboneComputer backboneComputer,
String assertedPrefix, String removedPrefix) {
Set<String> asserted = backboneComputer.propagatedConfigVars();
Set<String> propagatedAdditionalVars = backboneComputer
.propagatedAdditionalVars();
if (!asserted.isEmpty() || !propagatedAdditionalVars.isEmpty()) {
this.outStream.print(assertedPrefix);
for (String s : asserted) {
this.outStream.print(" " + s);
}
for (String s : newBooleanAssertions) {
for (String s : propagatedAdditionalVars) {
this.outStream.print(" " + s);
}
this.outStream.println();
}
Set<String> newlyAssertedFalse = backboneComputer.newDomainReductions();
newBooleanAssertions = backboneComputer.newReducedAdditionalVars();
if (!newlyAssertedFalse.isEmpty() || !newBooleanAssertions.isEmpty()) {
this.outStream.print(removed);
for (String s : newlyAssertedFalse) {
Set<String> assertedFalse = backboneComputer.domainReductions();
Set<String> unavailableAdditionalVars = backboneComputer
.unavailableAdditionalVars();
if (!assertedFalse.isEmpty() || !unavailableAdditionalVars.isEmpty()) {
this.outStream.print(removedPrefix);
for (String s : assertedFalse) {
this.outStream.print(" " + s);
}
for (String s : newBooleanAssertions) {
this.outStream.print(" " + s);
for (String s : unavailableAdditionalVars) {
this.outStream.print(" " + s.replaceAll("=99", "=1"));
}
this.outStream.println();
}
}
private void readInstance(String instance, IGroupSolver solver,
ConfigVarMap varMap) {
reader = new Br4cpAraliaReader(solver, varMap);
try {
reader.parseInstance(instance);
} catch (IOException e) {
e.printStackTrace();
System.exit(1);
}
}
private void runCLI() throws Exception {
this.outStream.println("available commands : ");
this.outStream.println(" #assumps : write the list of assumptions");
this.outStream.println(" #restart : clean all assumptions");
this.outStream.println(" #explain vX=Y : explain the assignement of value Y to variable X");
this.outStream.println(" #explain -vX=Y : explain the reduction of value Y in variable X");
this.outStream
.println(" #explain vX=Y : explain the assignement of value Y to variable X");
this.outStream
.println(" #explain -vX=Y : explain the reduction of value Y in variable X");
this.outStream.println(" #quit : exit this program");
this.outStream.println();
BufferedReader inReader = new BufferedReader(new InputStreamReader(
......@@ -105,30 +101,22 @@ public class Br4cpCLI {
this.outStream.print("$> ");
this.outStream.flush();
String line = inReader.readLine();
if(line == null)
if (line == null)
break;
if(line.length() == 0){
if (line.length() == 0) {
continue;
}
try {
Method toCall = getClass().getDeclaredMethod(line.substring(1).split(" ")[0],
new Class<?>[] {String.class});
toCall.invoke(this, new Object[]{line});
Method toCall = getClass().getDeclaredMethod(
line.substring(1).split(" ")[0],
new Class<?>[] { String.class });
toCall.invoke(this, new Object[] { line });
} catch (NoSuchMethodException e) {
assume(line);
}
}
this.outStream.println("Exiting. Bye!");
}
@SuppressWarnings("unused")
private void assumps(String line) {
this.outStream.print("assumptions :");
for(Iterator<String> it = this.assumptions.iterator(); it.hasNext(); ){
this.outStream.print(" "+it.next());
}
this.outStream.println();
}
@SuppressWarnings("unused")
private void restart(String line) {
......@@ -141,35 +129,40 @@ public class Br4cpCLI {
private void quit(String line) {
this.quit = true;
}
@SuppressWarnings("unused")
private void explain(String line) {
muses.reset();
IVecInt assumptions = new VecInt();
String[] words = line.split(" ");
for (int i=1;i<words.length;i++) {
for (int i = 1; i < words.length; i++) {
String assump = words[i].replaceAll("_", ".");
assump = assump.replaceAll("=", ".");
assumptions.push((assump.charAt(0)=='-')?(this.varMap.getSolverVar(assump.substring(1))):(-this.varMap.getSolverVar(assump)));
assumptions.push((assump.charAt(0) == '-') ? (this.varMap
.getSolverVar(assump.substring(1))) : (-this.varMap
.getSolverVar(assump)));
}
for(Set<Integer> assumpsSet : this.backboneComputer.getSolverAssumptions()) {
for(Integer n : assumpsSet){
for (Set<Integer> assumpsSet : this.backboneComputer
.getSolverAssumptions()) {
for (Integer n : assumpsSet) {
assumptions.push(n);
}
}
try {
if(solver.isSatisfiable(assumptions)){
this.outStream.println("ERROR: satisfiable, nothing to explain");
}else{
for (String constraint : reader.decode(solver.unsatExplanation()))
if (solver.isSatisfiable(assumptions)) {
this.outStream
.println("ERROR: satisfiable, nothing to explain");
} else {
for (String constraint : reader.decode(solver
.unsatExplanation()))
this.outStream.println(constraint);
}
} catch (TimeoutException e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
}
private void assume(String line) throws Exception {
String assump = line.replaceAll("_", ".");
assump = assump.replaceAll("=", ".");
......@@ -180,21 +173,43 @@ public class Br4cpCLI {
backboneComputer.setOptionalConfigVarAsNotInstalled(assump);
} else if (this.varMap.isAdditionalVar(assump)) {
backboneComputer.addAdditionalVarAssumption(assump);
} else if (this.varMap.isConfigVar(assump)){
} else if (this.varMap.isConfigVar(assump)) {
addAssumption(assump);
} else {
this.outStream.println(assump+" is not defined");
this.outStream.println(assump + " is not defined");
return;
}
if(!this.assumptions.contains(assump)) {
this.assumptions.add(assump);
for (Iterator<String> it = this.assumptions.iterator(); it
.hasNext();) {
String next = it.next();
if (next.substring(0, next.lastIndexOf("=")).equals(
line.substring(0, line.lastIndexOf('=')))) {
it.remove();
break;
}
}
printNewlyAsserted(backboneComputer);
this.assumptions.add(line);
printAssumptions();
printAsserted(backboneComputer);
} catch (IllegalArgumentException e) {
this.outStream.println("ERROR: " + e.getMessage());
}
}
private void printAssumptions() {
this.outStream.print("d");
for (Iterator<String> it = this.assumptions.iterator(); it.hasNext();) {
this.outStream.print(' ');
this.outStream.print(it.next());
}
this.outStream.println();
}
private void printAsserted(IBr4cpBackboneComputer backboneComputer) {
printAsserted(backboneComputer, "a", "r");
}
private void addAssumption(String assump) throws TimeoutException {
try {
backboneComputer.addAssumption(assump);
......
package org.sat4j.br4cp;
import java.io.BufferedReader;
import java.io.FileReader;
import java.io.IOException;
import java.io.PrintStream;
import java.util.ArrayList;
import java.util.List;
import java.util.Set;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IGroupSolver;
import org.sat4j.specs.TimeoutException;
import org.sat4j.tools.AllMUSes;
/**
* This class is a launcher for BR4CP scenario problems.
*
* @author lonca
*
*/
public class Br4cpScenarioSimulator {
private IGroupSolver solver;
private int currentScenarioIndex;
private long startTime;
private ConfigVarMap varMap;
private List<Integer> nbRemovedValues;
private PrintStream outStream = System.out;
private final AllMUSes muses = new AllMUSes(true,SolverFactory.instance());
public Br4cpScenarioSimulator(String instance, String scenario)
throws IOException, TimeoutException {
solver = muses.getSolverInstance();
varMap = new ConfigVarMap(solver);
this.outStream = Options.getInstance().getOutStream();
this.startTime = System.currentTimeMillis();
readInstance(instance, solver, varMap);
IBr4cpBackboneComputer backboneComputer = Options.getInstance().getBackboneComputer(solver, varMap);
printNewlyAsserted(backboneComputer, this.solver.getLogPrefix()
+ "rootPropagated:", this.solver.getLogPrefix()
+ "rootReduced:");
this.outStream.printf(this.solver.getLogPrefix()
+ "problem backbone computed in %.3fs.\n",
(System.currentTimeMillis() - startTime) / 1000.);
BufferedReader reader = new BufferedReader(new FileReader(scenario));
String line;
currentScenarioIndex = 0;
while ((line = reader.readLine()) != null) {
if ("".equals(line.trim())) {
continue;
}
++currentScenarioIndex;
backboneComputer.clearAssumptions();
this.nbRemovedValues = new ArrayList<Integer>();
this.nbRemovedValues.add(Integer.valueOf(backboneComputer
.newCspDomainReductions().size()));
long scenarioProcessingTime = System.currentTimeMillis();
processScenario(backboneComputer, line);
scenarioProcessingTime = System.currentTimeMillis()
- scenarioProcessingTime;
this.outStream
.println(this.solver.getLogPrefix()
+ "nbRemovedValues="
+ this.nbRemovedValues
.toString()
.substring(
1,
this.nbRemovedValues.toString()
.length() - 1)
.replaceAll(",", ""));
this.outStream.printf(this.solver.getLogPrefix()
+ "scenario processed in %.3fs\n",
scenarioProcessingTime / 1000.);
}
this.outStream.printf(this.solver.getLogPrefix()
+ "solving done in %.3fs.\n",
(System.currentTimeMillis() - startTime) / 1000.);
reader.close();
}
private void processScenario(IBr4cpBackboneComputer backboneComputer,
String line) throws TimeoutException {
this.outStream.println(this.solver.getLogPrefix() + "scenario #"
+ this.currentScenarioIndex);
line = line.replaceAll("\\s+", " ");
String[] words = line.split(" ");
// nbInstances=words[0], words[1].equals("decisions")
for (int i = 3; i < words.length; ++i) {
processWord(backboneComputer, words[i]);
}
backboneComputer.clearAssumptions();
}
private void processWord(IBr4cpBackboneComputer backboneComputer,
String word) throws TimeoutException {
String assump = word.replaceAll("_", ".");
assump = assump.replaceAll("=", ".");
if (this.varMap.isOutOfDomainConfigVar(assump)) {
backboneComputer.setOptionalConfigVarAsNotInstalled(assump);
} else if (!this.varMap.isConfigVar(assump)) {
backboneComputer.addAdditionalVarAssumption(assump);
} else {
try {
backboneComputer.addAssumption(assump);
} catch (ContradictionException e) {
e.printStackTrace();
System.exit(1);
}
}
this.outStream.println(this.solver.getLogPrefix() + "selected : "
+ word);
printNewlyAsserted(backboneComputer);
}
private void printNewlyAsserted(IBr4cpBackboneComputer backboneComputer) {
printNewlyAsserted(backboneComputer, this.solver.getLogPrefix()
+ "propagated :", this.solver.getLogPrefix() + "reduced :");
this.nbRemovedValues.add(Integer.valueOf(backboneComputer
.newCspDomainReductions().size()));
}
private void printNewlyAsserted(IBr4cpBackboneComputer backboneComputer,
String asserted, String removed) {
Set<String> newlyAsserted = backboneComputer.newPropagatedConfigVars();
Set<String> newBooleanAssertions = backboneComputer
.newPropagatedAdditionalVars();
if (!newlyAsserted.isEmpty() || !newBooleanAssertions.isEmpty()) {
this.outStream.print(asserted);
for (String s : newlyAsserted) {
this.outStream.print(" " + s);
}
for (String s : newBooleanAssertions) {
this.outStream.print(" " + s);
}
this.outStream.println();
}
Set<String> newlyAssertedFalse = backboneComputer.newDomainReductions();
newBooleanAssertions = backboneComputer.newReducedAdditionalVars();
if (!newlyAssertedFalse.isEmpty() || !newBooleanAssertions.isEmpty()) {
this.outStream.print(removed);
for (String s : newlyAssertedFalse) {
this.outStream.print(" " + s);
}
for (String s : newBooleanAssertions) {
this.outStream.print(" " + s);
}
this.outStream.println();
}
}
private void readInstance(String instance, IGroupSolver solver,
ConfigVarMap varMap) {
Br4cpAraliaReader reader = new Br4cpAraliaReader(solver, varMap);
try {
reader.parseInstance(instance);
} catch (IOException e) {
e.printStackTrace();
System.exit(1);
}
}
}
package org.sat4j.br4cp;
import java.util.Comparator;
public class ConfigVarComparator implements Comparator<String> {
public int compare(String arg0, String arg1) {
String[] t1 = arg0.split("[.=]");
String[] t2 = arg1.split("[.=]");
for (int i = 0; i < Math.min(t1.length, t2.length); ++i) {
boolean firstIsInteger = false, secondIsInteger = false;
Integer n1 = null, n2 = null;
try {
n1 = Integer.valueOf(t1[i]);
firstIsInteger = true;
} catch (NumberFormatException e) {
}
try {
n2 = Integer.valueOf(t2[i]);
secondIsInteger = true;
} catch (NumberFormatException e) {
}
if (firstIsInteger != secondIsInteger) {
return (firstIsInteger) ? (-1) : (1);
}
if (firstIsInteger && secondIsInteger) {
if (n1.equals(n2)) {
continue;
} else {
return n1.compareTo(n2);
}
}
firstIsInteger = false;
secondIsInteger = false;
try {
n1 = Integer.valueOf(t1[i].replaceAll("[a-zA-Z]", ""));
firstIsInteger = true;
} catch (NumberFormatException e) {
}
try {
n2 = Integer.valueOf(t2[i].replaceAll("[a-zA-Z]", ""));
secondIsInteger = true;
} catch (NumberFormatException e) {
}
if (firstIsInteger != secondIsInteger) {
return (firstIsInteger) ? (-1) : (1);
}
if (firstIsInteger && secondIsInteger) {
if (n1.equals(n2)) {
continue;
} else {
return n1.compareTo(n2);
}
}
return t1[i].compareTo(t2[i]);
}
return t1.length - t2.length;
}
}
......@@ -66,62 +66,36 @@ public interface IBr4cpBackboneComputer {
*/
public Set<String> propagatedConfigVars();
/**
* Returns the propagated configuration variables appeared after the last
* assumption.
*
* @return the propagated configuration variables appeared after the last
* assumption.
*/
public Set<String> newPropagatedConfigVars();
/**
* Returns the variables which became unavailable due to the assumptions.
* Configuration variables vx=y are not returned if vx=z is propagated.
*
* @return the variables which became unavailable due to the assumptions.
*/
public Set<String> domainReductions();
/**
* Returns the variables which became unavailable after the last assumption.
*
* @return the variables which became unavailable after the last assumption.
*/
public Set<String> newDomainReductions();
/**
* Returns the propagated additional variables due to the assumptions.
* Returns the propagated additional variables due to the assumptions, ended with "=1".
* Additional variables propagated to false are not returned, see
* {@link IBr4cpBackboneComputer#unavailableAdditionalVars()}
*
* @return the propagated additional variables due to the assumptions.
*/
public Set<String> propagatedAdditionalVars();
/**
* Returns the positively propagated additional variables appeared after the last
* assumption.
*
* @return the propagated additional variables appeared after the last
* assumption.
*/
public Set<String> newPropagatedAdditionalVars();
/**
* Returns the negatively propagated additional variables appeared after the last
* assumption.
* Returns the additional variables propagated to false, ended with "=1".
*
* @return the propagated additional variables appeared after the last
* assumption.
* @return the additional variables propagated to false, ended with "=1".
*/
public Set<String> newReducedAdditionalVars();
public Set<String> unavailableAdditionalVars();
/**
* Returns the new domain reductions as a CSP solver would do, that is
* adding a X=99 value if optional variable X is not installed.
* Allow to get the assumptions made by the computer. The solver variables
* are returned.
*
* @return the new domain reductions as a CSP solver would do.
* @return the solver variables in the assumption stack
*/
public Set<String> newCspDomainReductions();
public List<Set<Integer>> getSolverAssumptions();
}
......@@ -12,12 +12,7 @@ public class Launcher {
}
String instanceFile = options.getInstanceFile();
if(instanceFile != null) {
String scenarioFile = options.getScenarioFile();
if(scenarioFile != null) {
new Br4cpScenarioSimulator(instanceFile, scenarioFile);
}else{
new Br4cpCLI(instanceFile);
}
new Br4cpCLI(instanceFile);
}else{
throw new IllegalArgumentException("An instance file is required");
}
......
......@@ -14,6 +14,8 @@ public class Options {
private String backboneComputer = "Default";
private boolean replacementForbidden = false;
private PrintStream outStream = System.out;
public static Options getInstance(){
......@@ -66,7 +68,7 @@ public class Options {
private void processOption(String arg) throws IllegalArgumentException, SecurityException, IllegalAccessException, NoSuchFieldException {
int eqIndex = arg.indexOf('=');
if(eqIndex == -1) {
Options.class.getDeclaredField(arg).setBoolean(this, true);
Options.class.getDeclaredField(arg).setBoolean(this, !Options.class.getDeclaredField(arg).getBoolean(this));
}else{
Options.class.getDeclaredField(arg.substring(0, eqIndex)).set(this, arg.substring(eqIndex+1));
}
......@@ -96,4 +98,8 @@ public class Options {
}
}
public boolean areReplacementAllowed() {
return !this.replacementForbidden;
}
}
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