Skip to content
Snippets Groups Projects
Commit 0be2621a authored by Sebastian Krings's avatar Sebastian Krings
Browse files

submit sat solver selection on startup

parent 2f108075
Branches
No related tags found
No related merge requests found
...@@ -13,7 +13,6 @@ import java.util.logging.Level; ...@@ -13,7 +13,6 @@ import java.util.logging.Level;
import java.util.logging.Logger; import java.util.logging.Logger;
import java.util.logging.SimpleFormatter; import java.util.logging.SimpleFormatter;
import kodkod.engine.satlab.SATFactory;
import de.prob.prolog.output.IPrologTermOutput; import de.prob.prolog.output.IPrologTermOutput;
import de.prob.prolog.output.PrologTermOutput; import de.prob.prolog.output.PrologTermOutput;
import de.stups.probkodkod.parser.lexer.Lexer; import de.stups.probkodkod.parser.lexer.Lexer;
...@@ -24,6 +23,7 @@ import de.stups.probkodkod.parser.parser.ParserException; ...@@ -24,6 +23,7 @@ import de.stups.probkodkod.parser.parser.ParserException;
import de.stups.probkodkod.tools.LogReader; import de.stups.probkodkod.tools.LogReader;
import de.stups.probkodkod.tools.LogWriter; import de.stups.probkodkod.tools.LogWriter;
import de.stups.probkodkod.tools.MergeWriter; import de.stups.probkodkod.tools.MergeWriter;
import kodkod.engine.satlab.SATFactory;
/** /**
* Main class for the Kodkod wrapper. * Main class for the Kodkod wrapper.
...@@ -87,13 +87,11 @@ public class KodkodInteraction { ...@@ -87,13 +87,11 @@ public class KodkodInteraction {
out = new PrintWriter(System.out); out = new PrintWriter(System.out);
} else { } else {
MergeWriter merge = new MergeWriter(fw); MergeWriter merge = new MergeWriter(fw);
in = new LogReader(new InputStreamReader(System.in), in = new LogReader(new InputStreamReader(System.in), merge.createWriter(" ProB:"));
merge.createWriter(" ProB:")); out = new PrintWriter(new LogWriter(new OutputStreamWriter(System.out), merge.createWriter("Kodkod:")));
out = new PrintWriter(new LogWriter(new OutputStreamWriter(
System.out), merge.createWriter("Kodkod:")));
} }
is_up_and_running(System.out); is_up_and_running(System.out, SATSolver.valueOf(args[0]));
KodkodInteraction interaction = new KodkodInteraction(); KodkodInteraction interaction = new KodkodInteraction();
interaction.interaction(in, out); interaction.interaction(in, out);
...@@ -107,8 +105,8 @@ public class KodkodInteraction { ...@@ -107,8 +105,8 @@ public class KodkodInteraction {
} }
} }
private static void is_up_and_running(PrintStream out) { private static void is_up_and_running(PrintStream out, SATSolver satSolver) {
SATFactory satfac = SolverChecker.determineSatFactory(); SATFactory satfac = SolverChecker.determineSatFactory(satSolver);
out.println("ProB-Kodkod started: " + satfac.toString()); out.println("ProB-Kodkod started: " + satfac.toString());
} }
......
...@@ -25,16 +25,25 @@ import kodkod.instance.Universe; ...@@ -25,16 +25,25 @@ import kodkod.instance.Universe;
*/ */
public class SolverChecker { public class SolverChecker {
private static final Logger LOGGER = Logger.getLogger("de.stups.probkodkod"); private static final Logger LOGGER = Logger.getLogger("de.stups.probkodkod");
private static final SATFactory[] FACTORIES = { SATFactory.Lingeling, SATFactory.Glucose, SATFactory.MiniSat,
new SAT4JWithTimeoutFactory() };
// private static final SATFactory[] FACTORIES = { public static SATFactory determineSatFactory(SATSolver satSolver) {
// new SAT4JWithTimeoutFactory(), SATFactory.MiniSat, switch (satSolver) {
// SATFactory.DefaultSAT4J }; case glucose:
return determineSatFactory(SATFactory.Glucose, new SAT4JWithTimeoutFactory());
case lingeling:
return determineSatFactory(SATFactory.Lingeling, new SAT4JWithTimeoutFactory());
case minisat:
return determineSatFactory(SATFactory.MiniSat, new SAT4JWithTimeoutFactory());
case sat4j:
return determineSatFactory(new SAT4JWithTimeoutFactory());
default:
throw new Error("No valid SAT solver back-end for Kodkod selected.");
}
}
public static SATFactory determineSatFactory() { public static SATFactory determineSatFactory(SATFactory... factories) {
Map<String, Throwable> throwables = new HashMap<String, Throwable>(); Map<String, Throwable> throwables = new HashMap<String, Throwable>();
for (final SATFactory factory : FACTORIES) { for (final SATFactory factory : factories) {
try { try {
check(factory); check(factory);
// the factory seems to work, we use it // the factory seems to work, we use it
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment