From 0be2621aede33818387d2b2f5a8eefcd70f5a1d8 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Thu, 6 Oct 2016 09:24:35 +0200
Subject: [PATCH] submit sat solver selection on startup
---
.../stups/probkodkod/KodkodInteraction.java | 14 +++++------
.../de/stups/probkodkod/SolverChecker.java | 23 +++++++++++++------
2 files changed, 22 insertions(+), 15 deletions(-)
diff --git a/src/main/java/de/stups/probkodkod/KodkodInteraction.java b/src/main/java/de/stups/probkodkod/KodkodInteraction.java
index 847b967..a73d368 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 606030d..5d35889 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
--
GitLab