diff --git a/src/main/java/de/stups/probkodkod/KodkodSession.java b/src/main/java/de/stups/probkodkod/KodkodSession.java index 04a8c81760062045d5f1f703bde823c9278fca70..84e4183b03e0723f9c516c62d256f274111bbf3a 100644 --- a/src/main/java/de/stups/probkodkod/KodkodSession.java +++ b/src/main/java/de/stups/probkodkod/KodkodSession.java @@ -35,7 +35,7 @@ public class KodkodSession { final Solver solver = new Solver(); - SATFactory satFactory = SolverChecker.determineSatFactory(sat); + SATFactory satFactory = SolverChecker.determineSatFactory(sat, timeout); solver.options().setSolver(satFactory); solver.options().setSymmetryBreaking(symmetry); diff --git a/src/main/java/de/stups/probkodkod/SolverChecker.java b/src/main/java/de/stups/probkodkod/SolverChecker.java index cf7238a7f31af581a8f2a10e4addc78d17085564..bfff2a612c9f03a6ef248382fb4b3fbccf3db605 100644 --- a/src/main/java/de/stups/probkodkod/SolverChecker.java +++ b/src/main/java/de/stups/probkodkod/SolverChecker.java @@ -27,15 +27,20 @@ public class SolverChecker { private static final Logger LOGGER = Logger.getLogger("de.stups.probkodkod"); public static SATFactory determineSatFactory(SATSolver satSolver) { + // a default timeout - an individual one is requested by prob anyway + return determineSatFactory(satSolver, 1500); + } + + public static SATFactory determineSatFactory(SATSolver satSolver, long timeout) { switch (satSolver) { case glucose: - return determineSatFactory(SATFactory.Glucose, new SAT4JWithTimeoutFactory()); + return determineSatFactory(SATFactory.Glucose, new SAT4JWithTimeoutFactory(timeout)); case lingeling: - return determineSatFactory(SATFactory.Lingeling, new SAT4JWithTimeoutFactory()); + return determineSatFactory(SATFactory.Lingeling, new SAT4JWithTimeoutFactory(timeout)); case minisat: - return determineSatFactory(SATFactory.MiniSat, new SAT4JWithTimeoutFactory()); + return determineSatFactory(SATFactory.MiniSat, new SAT4JWithTimeoutFactory(timeout)); case sat4j: - return determineSatFactory(new SAT4JWithTimeoutFactory()); + return determineSatFactory(new SAT4JWithTimeoutFactory(timeout)); default: throw new Error("No valid SAT solver back-end for Kodkod selected."); }