diff --git a/src/main/java/de/stups/probkodkod/KodkodAnalysis.java b/src/main/java/de/stups/probkodkod/KodkodAnalysis.java
index cfb71852848756b23fd4d03761d819b9f2cc306b..06521422b62e198c7ad2043febf6e3deb2fb0550 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 f618ec94360dc9aef2d909e48680846997620fe3..324dc0b4b53bacbbdb58e720fa92f3c879bfdcdd 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 c5c06e8d3fde9b92bf9f90d438d336e3aab78682..77f01842a73dae51e398993bb45ae7bf35d856ad 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 0000000000000000000000000000000000000000..a37dc2dba6901bd1ec3817bc6558a500210f2e40
--- /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 0000000000000000000000000000000000000000..c5bd727dd9515d42cabe23be52283facd6153756
--- /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 5ef71b9def3b5613741f7b58954e8e705f35d90b..1d559d1259fa2126d26fba9a4e2cbd4b2e86a83a 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 91eceacc7c4ac8648e5ee3dfe226742b4273cda5..6e1d0894c4520dca0fc72829c3c0bbec88edf969 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 75b2a27c7be1774702bc0dfa96d5c47b3bc6de36..24695961317854f6c74432a89e29d435b7d95e78 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 4e005ff3223ea3ea43a206fcf4e281dc6b556cf9..c060001888c5b8c34c237c5f7ee100df39952404 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 95c0dbfea0fa2063084fe194967f258c21d80db5..9c6e37d36527f4149f1925ab0456ad9069ed5c1a 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 9df5b14df0e84cec6a926ae0e86e6b017d0b3770..b9c72b5eae5f1b0cdb3a6308aa558cc86a11c5b9 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 e106b9f6595bb3df20d84a854ae707f8f64f5556..1725fe9f33dd7138143cbf5c185c0cb5a894b2b5 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 f663ba41d738e3718a5635972ef87d005934165c..c0c873df2de0b1cd0c0c8eaee897fad784527666 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 404c20abd780b8ceb0c16b5d20892608594e8941..05adb8a19abdcb39262161adabc0a1e1c116af47 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 a2e31403c246e78e46864aca89b1bb8d1fe64bcc..7448a38ef9b78a42c721cb4a748bf73be20fae53 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 8437c86d322f020a23c970668f0d2679e9a738a9..82656ad46d19a3fbdfdbec5cb538d6b141f10116 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 775f4fdc7b9eb1183883ac16f62ddecbc9e41c47..f3791fbd2fe75fc8e240dc59f25ca639355953d8 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 4ab4affa69675ee4988756a6375ba9ebe10f6669..f84e7ba0db78743207d10060489c4bb8260e9896 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))