# HG changeset patch
# User blanchet
# Date 1291638789 -3600
# Node ID 75275c796b46a502d5d35d77af0a4f133f1f6af8
# Parent  000ca46429cdb723dd2d070c65b07bac80935a2c
use ML SAT solvers up to a certain time limit, then switch to faster solvers with a timeout -- this becomes necessary with the new, more powerful monotonicity calculus

diff -r 000ca46429cd -r 75275c796b46 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 06 13:33:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 06 13:33:09 2010 +0100
@@ -270,7 +270,7 @@
     val intro_table = inductive_intro_table ctxt subst def_table
     val ground_thm_table = ground_theorem_table thy
     val ersatz_table = ersatz_table ctxt
-    val (hol_ctxt as {wf_cache, ...}) =
+    val hol_ctxt as {wf_cache, ...} =
       {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
        stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
        whacks = whacks, binary_ints = binary_ints,
diff -r 000ca46429cd -r 75275c796b46 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
@@ -562,7 +562,11 @@
                              string_for_vars ", " (sort int_ord xs))
        |> space_implode "\n"))
 
-fun solve max_var (comps, clauses) =
+(* The ML solver timeout should correspond more or less to the overhead of
+   invoking an external prover. *)
+val ml_solver_timeout = SOME (seconds 0.02)
+
+fun solve tac_timeout max_var (comps, clauses) =
   let
     val asgs = map_filter (fn [(x, (_, a))] => SOME (x, a) | _ => NONE) clauses
     fun do_assigns assigns =
@@ -578,13 +582,22 @@
     else
       let
         (* use the first ML solver (to avoid startup overhead) *)
-        val solvers = !SatSolver.solvers
-                      |> filter (member (op =) ["dptsat", "dpll"] o fst)
+        val (ml_solvers, nonml_solvers) =
+          !SatSolver.solvers
+          |> List.partition (member (op =) ["dptsat", "dpll"] o fst)
+        val res =
+          if null nonml_solvers then
+            time_limit tac_timeout (snd (hd ml_solvers)) prop
+          else
+            time_limit ml_solver_timeout (snd (hd ml_solvers)) prop
+            handle TimeLimit.TimeOut =>
+                   time_limit tac_timeout (SatSolver.invoke_solver "auto") prop
       in
-        case snd (hd solvers) prop of
+        case res of
           SatSolver.SATISFIABLE assigns => do_assigns assigns
         | _ => (trace_msg (K "*** Unsolvable"); NONE)
       end
+      handle TimeLimit.TimeOut => (trace_msg (K "*** Timed out"); NONE)
   end
 
 type mcontext =
@@ -1192,8 +1205,8 @@
 fun amass f t (ms, accum) =
   let val (m, accum) = f t accum in (m :: ms, accum) end
 
-fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
-          (nondef_ts, def_ts) =
+fun infer which no_harmless (hol_ctxt as {ctxt, tac_timeout, ...}) binarize
+          alpha_T (nondef_ts, def_ts) =
   let
     val _ = trace_msg (fn () => "****** " ^ which ^ " analysis: " ^
                                 string_for_mtype MAlpha ^ " is " ^
@@ -1208,7 +1221,7 @@
     val (def_ms, (gamma, cset)) =
       ([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
   in
-    case solve (!max_fresh) cset of
+    case solve tac_timeout (!max_fresh) cset of
       SOME asgs => (print_mcontext ctxt asgs gamma;
                     SOME (asgs, (nondef_ms, def_ms), !constr_mcache))
     | _ => NONE