introduce new solver factory with timeout, drop minisat option for now

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) {

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) {

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>();

src/main/java/de/stups/probkodkod/sat/SAT4JWithTimeout.java

+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

src/main/java/de/stups/probkodkod/sat/SAT4JWithTimeoutFactory.java

+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";
+	}
+}

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;
     

src/test/resources/problems/functions.kodkod

-problem functions
+problem functions 3500
 
  ((d 2) (r 2))
  

src/test/resources/problems/integercast.kodkod

-problem integercast
+problem integercast 3500
 
 ((inttype (si 0 7) (ai 0 9)))
 

src/test/resources/problems/integers.kodkod

-problem integers
+problem integers 3500
 
 ((inttype (si 0 2))
  (w 2))

src/test/resources/problems/intrange.kodkod

-problem intrange
+problem intrange 3500
 
 ((inttype (p2i 0 8) (is 0 8)))
  

src/test/resources/problems/intvar.kodkod

-problem intvar
+problem intvar 3500
 
 ((inttype (si 0 7)))
 

src/test/resources/problems/loop.kodkod

-problem loop
+problem loop 3500
 
  ((Blocks 8))
 

src/test/resources/problems/negative.kodkod

-problem negative
+problem negative 3500
 
 ((inttype (p2i -15 15)))
 

src/test/resources/problems/projection.kodkod

-problem projection
+problem projection 3500
 
 ((world 2))
 

src/test/resources/problems/relquant.kodkod

-problem relquant
+problem relquant 3500
 
  ((d 2) (r 2))
  

src/test/resources/problems/returnzero.kodkod

-problem returnzero 
+problem returnzero 3500
   ( (inttype(p2i 0 0)) )
   
   ( (x singleton subset p2i) )

src/test/resources/problems/sendmoremoney.kodkod

-problem sendmoremoney ((inttype(p2i 0 199980)))
+problem sendmoremoney 3500
+
+((inttype(p2i 0 199980)))
 
 ( (s singleton subset p2i)
   (e singleton subset p2i)

src/test/resources/problems/simpletwovars.kodkod

-problem simpletwovars
+problem simpletwovars 3500
 
  ((T 2))