From 55ac98d3fc4f7a90af25f9d63024069232b3b2cb Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Mon, 17 Aug 2015 14:16:21 +0200
Subject: [PATCH] introduce new solver factory with timeout, drop minisat
option for now
---
.../de/stups/probkodkod/KodkodAnalysis.java | 3 +-
.../de/stups/probkodkod/KodkodSession.java | 8 +-
.../de/stups/probkodkod/SolverChecker.java | 8 +-
.../probkodkod/sat/SAT4JWithTimeout.java | 80 +++++++++++++++++++
.../sat/SAT4JWithTimeoutFactory.java | 25 ++++++
src/main/resources/problem.grammar | 2 +-
src/test/resources/problems/functions.kodkod | 2 +-
.../resources/problems/integercast.kodkod | 2 +-
src/test/resources/problems/integers.kodkod | 2 +-
src/test/resources/problems/intrange.kodkod | 2 +-
src/test/resources/problems/intvar.kodkod | 2 +-
src/test/resources/problems/loop.kodkod | 2 +-
src/test/resources/problems/negative.kodkod | 2 +-
src/test/resources/problems/projection.kodkod | 2 +-
src/test/resources/problems/relquant.kodkod | 2 +-
src/test/resources/problems/returnzero.kodkod | 2 +-
.../resources/problems/sendmoremoney.kodkod | 4 +-
.../resources/problems/simpletwovars.kodkod | 2 +-
18 files changed, 132 insertions(+), 20 deletions(-)
create mode 100644 src/main/java/de/stups/probkodkod/sat/SAT4JWithTimeout.java
create mode 100644 src/main/java/de/stups/probkodkod/sat/SAT4JWithTimeoutFactory.java
diff --git a/src/main/java/de/stups/probkodkod/KodkodAnalysis.java b/src/main/java/de/stups/probkodkod/KodkodAnalysis.java
index cfb7185..0652142 100644
--- a/src/main/java/de/stups/probkodkod/KodkodAnalysis.java
+++ b/src/main/java/de/stups/probkodkod/KodkodAnalysis.java
@@ -253,7 +253,8 @@ public class KodkodAnalysis extends DepthFirstAdapter {
node.getFormula().apply(this);
problem.setFormula(formulaStack.pop());
- session.addProblem(problem.createImmutable());
+ long timeout = Long.parseLong(node.getTimeout().getText());
+ session.addProblem(problem.createImmutable(), timeout);
}
private void registerTypes(final Collection<PType> types) {
diff --git a/src/main/java/de/stups/probkodkod/KodkodSession.java b/src/main/java/de/stups/probkodkod/KodkodSession.java
index f618ec9..324dc0b 100644
--- a/src/main/java/de/stups/probkodkod/KodkodSession.java
+++ b/src/main/java/de/stups/probkodkod/KodkodSession.java
@@ -6,9 +6,9 @@ import java.util.logging.Level;
import java.util.logging.Logger;
import kodkod.engine.Solver;
-import kodkod.engine.satlab.SATFactory;
import kodkod.instance.TupleSet;
import de.prob.prolog.output.IPrologTermOutput;
+import de.stups.probkodkod.sat.SAT4JWithTimeoutFactory;
/**
* The session contains all the information that is needed during an interaction
@@ -21,7 +21,7 @@ import de.prob.prolog.output.IPrologTermOutput;
*
*/
public class KodkodSession {
- private final SATFactory SOLVER = SolverChecker.determineSatFactory();
+ // private final SATFactory SOLVER = SolverChecker.determineSatFactory();
private final Logger logger = Logger.getLogger(KodkodSession.class
.getName());
@@ -30,12 +30,12 @@ public class KodkodSession {
private final Map<ImmutableProblem, Request> currentRequests = new HashMap<ImmutableProblem, Request>();
private boolean stopped = false;
- public void addProblem(final ImmutableProblem problem) {
+ public void addProblem(final ImmutableProblem problem, long timeout) {
String id = problem.getId();
problems.put(id, problem);
final Solver solver = new Solver();
- solver.options().setSolver(SOLVER);
+ solver.options().setSolver(new SAT4JWithTimeoutFactory(timeout));
solver.options().setSymmetryBreaking(0);
final Integer bitwidth = problem.getBitwidth();
if (bitwidth != null) {
diff --git a/src/main/java/de/stups/probkodkod/SolverChecker.java b/src/main/java/de/stups/probkodkod/SolverChecker.java
index c5c06e8..77f0184 100644
--- a/src/main/java/de/stups/probkodkod/SolverChecker.java
+++ b/src/main/java/de/stups/probkodkod/SolverChecker.java
@@ -15,6 +15,7 @@ import kodkod.engine.Solver;
import kodkod.engine.satlab.SATFactory;
import kodkod.instance.Bounds;
import kodkod.instance.Universe;
+import de.stups.probkodkod.sat.SAT4JWithTimeoutFactory;
/**
* Here we determine if we use Minisat or SAT4J as back-end. We do this by
@@ -25,8 +26,11 @@ import kodkod.instance.Universe;
public class SolverChecker {
private static final Logger LOGGER = Logger
.getLogger("de.stups.probkodkod");
- private static final SATFactory[] FACTORIES = { SATFactory.MiniSat,
- SATFactory.DefaultSAT4J };
+ private static final SATFactory[] FACTORIES = { new SAT4JWithTimeoutFactory() };
+
+ // private static final SATFactory[] FACTORIES = {
+ // new SAT4JWithTimeoutFactory(), SATFactory.MiniSat,
+ // SATFactory.DefaultSAT4J };
public static SATFactory determineSatFactory() {
Map<String, Throwable> throwables = new HashMap<String, Throwable>();
diff --git a/src/main/java/de/stups/probkodkod/sat/SAT4JWithTimeout.java b/src/main/java/de/stups/probkodkod/sat/SAT4JWithTimeout.java
new file mode 100644
index 0000000..a37dc2d
--- /dev/null
+++ b/src/main/java/de/stups/probkodkod/sat/SAT4JWithTimeout.java
@@ -0,0 +1,80 @@
+package de.stups.probkodkod.sat;
+
+import kodkod.engine.satlab.SATSolver;
+
+import org.sat4j.core.VecInt;
+import org.sat4j.minisat.SolverFactory;
+import org.sat4j.specs.ContradictionException;
+import org.sat4j.specs.ISolver;
+
+final class SAT4JWithTimeout implements SATSolver {
+ private ISolver solver;
+ private boolean sat = true;
+ private int vars, clauses;
+ private long timeout;
+
+ SAT4JWithTimeout(long ms) {
+ this.solver = SolverFactory.instance().defaultSolver();
+ this.solver.setTimeoutMs(ms);
+ this.timeout = ms;
+ this.vars = 0;
+ this.clauses = 0;
+ }
+
+ public int numberOfVariables() {
+ return vars;
+ }
+
+ public int numberOfClauses() {
+ return clauses;
+ }
+
+ public void addVariables(int numVars) {
+ if (numVars < 0)
+ throw new IllegalArgumentException("numVars < 0: " + numVars);
+ else if (numVars > 0) {
+ vars += numVars;
+ solver.newVar(vars);
+ }
+ }
+
+ public boolean addClause(int[] lits) {
+ try {
+ if (sat) {
+ clauses++;
+ solver.addClause(new VecInt(lits));
+ return true;
+ }
+ } catch (ContradictionException e) {
+ sat = false;
+ }
+ return false;
+ }
+
+ public boolean solve() {
+ try {
+ if (sat)
+ sat = solver.isSatisfiable();
+ return sat;
+ } catch (org.sat4j.specs.TimeoutException e) {
+ throw new RuntimeException("timed out");
+ }
+ }
+
+ public final boolean valueOf(int variable) {
+ if (!sat)
+ throw new IllegalStateException();
+ if (variable < 1 || variable > vars)
+ throw new IllegalArgumentException(variable + " !in [1.." + vars
+ + "]");
+ return solver.model(variable);
+ }
+
+ public synchronized final void free() {
+ solver = null;
+ }
+
+ public String toString() {
+ return "SAT4JWithTimeout Solver using " + timeout + " ms timeout";
+ }
+}
\ No newline at end of file
diff --git a/src/main/java/de/stups/probkodkod/sat/SAT4JWithTimeoutFactory.java b/src/main/java/de/stups/probkodkod/sat/SAT4JWithTimeoutFactory.java
new file mode 100644
index 0000000..c5bd727
--- /dev/null
+++ b/src/main/java/de/stups/probkodkod/sat/SAT4JWithTimeoutFactory.java
@@ -0,0 +1,25 @@
+package de.stups.probkodkod.sat;
+
+import kodkod.engine.satlab.SATFactory;
+import kodkod.engine.satlab.SATSolver;
+
+public class SAT4JWithTimeoutFactory extends SATFactory {
+ private long timeout;
+
+ public SAT4JWithTimeoutFactory() {
+ this(1500);
+ }
+
+ public SAT4JWithTimeoutFactory(long ms) {
+ this.timeout = ms;
+ }
+
+ @Override
+ public SATSolver instance() {
+ return new SAT4JWithTimeout(timeout);
+ }
+
+ public String toString() {
+ return "SAT4J with timeout of " + timeout + " ms";
+ }
+}
diff --git a/src/main/resources/problem.grammar b/src/main/resources/problem.grammar
index 5ef71b9..1d559d1 100644
--- a/src/main/resources/problem.grammar
+++ b/src/main/resources/problem.grammar
@@ -99,7 +99,7 @@ Productions
| {reset} reset
| {none};
- problem = keyword_problem [id]:identifier
+ problem = keyword_problem [id]:identifier [timeout]:number
[tpl]:parenl [types]:type* [tpr]:parenr
[rpl]:parenl [relations]:relation* [rpr]:parenr formula;
diff --git a/src/test/resources/problems/functions.kodkod b/src/test/resources/problems/functions.kodkod
index 91eceac..6e1d089 100644
--- a/src/test/resources/problems/functions.kodkod
+++ b/src/test/resources/problems/functions.kodkod
@@ -1,4 +1,4 @@
-problem functions
+problem functions 3500
((d 2) (r 2))
diff --git a/src/test/resources/problems/integercast.kodkod b/src/test/resources/problems/integercast.kodkod
index 75b2a27..2469596 100644
--- a/src/test/resources/problems/integercast.kodkod
+++ b/src/test/resources/problems/integercast.kodkod
@@ -1,4 +1,4 @@
-problem integercast
+problem integercast 3500
((inttype (si 0 7) (ai 0 9)))
diff --git a/src/test/resources/problems/integers.kodkod b/src/test/resources/problems/integers.kodkod
index 4e005ff..c060001 100644
--- a/src/test/resources/problems/integers.kodkod
+++ b/src/test/resources/problems/integers.kodkod
@@ -1,4 +1,4 @@
-problem integers
+problem integers 3500
((inttype (si 0 2))
(w 2))
diff --git a/src/test/resources/problems/intrange.kodkod b/src/test/resources/problems/intrange.kodkod
index 95c0dbf..9c6e37d 100644
--- a/src/test/resources/problems/intrange.kodkod
+++ b/src/test/resources/problems/intrange.kodkod
@@ -1,4 +1,4 @@
-problem intrange
+problem intrange 3500
((inttype (p2i 0 8) (is 0 8)))
diff --git a/src/test/resources/problems/intvar.kodkod b/src/test/resources/problems/intvar.kodkod
index 9df5b14..b9c72b5 100644
--- a/src/test/resources/problems/intvar.kodkod
+++ b/src/test/resources/problems/intvar.kodkod
@@ -1,4 +1,4 @@
-problem intvar
+problem intvar 3500
((inttype (si 0 7)))
diff --git a/src/test/resources/problems/loop.kodkod b/src/test/resources/problems/loop.kodkod
index e106b9f..1725fe9 100644
--- a/src/test/resources/problems/loop.kodkod
+++ b/src/test/resources/problems/loop.kodkod
@@ -1,4 +1,4 @@
-problem loop
+problem loop 3500
((Blocks 8))
diff --git a/src/test/resources/problems/negative.kodkod b/src/test/resources/problems/negative.kodkod
index f663ba4..c0c873d 100644
--- a/src/test/resources/problems/negative.kodkod
+++ b/src/test/resources/problems/negative.kodkod
@@ -1,4 +1,4 @@
-problem negative
+problem negative 3500
((inttype (p2i -15 15)))
diff --git a/src/test/resources/problems/projection.kodkod b/src/test/resources/problems/projection.kodkod
index 404c20a..05adb8a 100644
--- a/src/test/resources/problems/projection.kodkod
+++ b/src/test/resources/problems/projection.kodkod
@@ -1,4 +1,4 @@
-problem projection
+problem projection 3500
((world 2))
diff --git a/src/test/resources/problems/relquant.kodkod b/src/test/resources/problems/relquant.kodkod
index a2e3140..7448a38 100644
--- a/src/test/resources/problems/relquant.kodkod
+++ b/src/test/resources/problems/relquant.kodkod
@@ -1,4 +1,4 @@
-problem relquant
+problem relquant 3500
((d 2) (r 2))
diff --git a/src/test/resources/problems/returnzero.kodkod b/src/test/resources/problems/returnzero.kodkod
index 8437c86..82656ad 100644
--- a/src/test/resources/problems/returnzero.kodkod
+++ b/src/test/resources/problems/returnzero.kodkod
@@ -1,4 +1,4 @@
-problem returnzero
+problem returnzero 3500
( (inttype(p2i 0 0)) )
( (x singleton subset p2i) )
diff --git a/src/test/resources/problems/sendmoremoney.kodkod b/src/test/resources/problems/sendmoremoney.kodkod
index 775f4fd..f3791fb 100644
--- a/src/test/resources/problems/sendmoremoney.kodkod
+++ b/src/test/resources/problems/sendmoremoney.kodkod
@@ -1,4 +1,6 @@
-problem sendmoremoney ((inttype(p2i 0 199980)))
+problem sendmoremoney 3500
+
+((inttype(p2i 0 199980)))
( (s singleton subset p2i)
(e singleton subset p2i)
diff --git a/src/test/resources/problems/simpletwovars.kodkod b/src/test/resources/problems/simpletwovars.kodkod
index 4ab4aff..f84e7ba 100644
--- a/src/test/resources/problems/simpletwovars.kodkod
+++ b/src/test/resources/problems/simpletwovars.kodkod
@@ -1,4 +1,4 @@
-problem simpletwovars
+problem simpletwovars 3500
((T 2))
--
GitLab