diff --git a/src/main/java/de/stups/probkodkod/KodkodInteraction.java b/src/main/java/de/stups/probkodkod/KodkodInteraction.java index 847b967b765f358692cb5e1223a846d5dd30f5d3..a73d3685bfecd6cdc102c0f0457f4b5c7f3f23f6 100644 --- a/src/main/java/de/stups/probkodkod/KodkodInteraction.java +++ b/src/main/java/de/stups/probkodkod/KodkodInteraction.java @@ -13,7 +13,6 @@ import java.util.logging.Level; import java.util.logging.Logger; import java.util.logging.SimpleFormatter; -import kodkod.engine.satlab.SATFactory; import de.prob.prolog.output.IPrologTermOutput; import de.prob.prolog.output.PrologTermOutput; import de.stups.probkodkod.parser.lexer.Lexer; @@ -24,6 +23,7 @@ import de.stups.probkodkod.parser.parser.ParserException; import de.stups.probkodkod.tools.LogReader; import de.stups.probkodkod.tools.LogWriter; import de.stups.probkodkod.tools.MergeWriter; +import kodkod.engine.satlab.SATFactory; /** * Main class for the Kodkod wrapper. @@ -87,13 +87,11 @@ public class KodkodInteraction { out = new PrintWriter(System.out); } else { MergeWriter merge = new MergeWriter(fw); - in = new LogReader(new InputStreamReader(System.in), - merge.createWriter(" ProB:")); - out = new PrintWriter(new LogWriter(new OutputStreamWriter( - System.out), merge.createWriter("Kodkod:"))); + in = new LogReader(new InputStreamReader(System.in), merge.createWriter(" ProB:")); + 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(); interaction.interaction(in, out); @@ -107,8 +105,8 @@ public class KodkodInteraction { } } - private static void is_up_and_running(PrintStream out) { - SATFactory satfac = SolverChecker.determineSatFactory(); + private static void is_up_and_running(PrintStream out, SATSolver satSolver) { + SATFactory satfac = SolverChecker.determineSatFactory(satSolver); out.println("ProB-Kodkod started: " + satfac.toString()); } diff --git a/src/main/java/de/stups/probkodkod/SolverChecker.java b/src/main/java/de/stups/probkodkod/SolverChecker.java index 606030d96c8fc085a17becf5f1ffe449fe688282..5d358894ff87b4eb0bce203eb936b1c675183f97 100644 --- a/src/main/java/de/stups/probkodkod/SolverChecker.java +++ b/src/main/java/de/stups/probkodkod/SolverChecker.java @@ -25,16 +25,25 @@ import kodkod.instance.Universe; */ public class SolverChecker { 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 = { - // new SAT4JWithTimeoutFactory(), SATFactory.MiniSat, - // SATFactory.DefaultSAT4J }; + public static SATFactory determineSatFactory(SATSolver satSolver) { + switch (satSolver) { + 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>(); - for (final SATFactory factory : FACTORIES) { + for (final SATFactory factory : factories) { try { check(factory); // the factory seems to work, we use it