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
authorblanchet
Mon Dec 06 13:33:09 2010 +0100 (2010-12-06 ago)
changeset 4100775275c796b46
parent 41006 000ca46429cd
child 41008 298226ba5606
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
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 06 13:33:09 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 06 13:33:09 2010 +0100
     1.3 @@ -270,7 +270,7 @@
     1.4      val intro_table = inductive_intro_table ctxt subst def_table
     1.5      val ground_thm_table = ground_theorem_table thy
     1.6      val ersatz_table = ersatz_table ctxt
     1.7 -    val (hol_ctxt as {wf_cache, ...}) =
     1.8 +    val hol_ctxt as {wf_cache, ...} =
     1.9        {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
    1.10         stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
    1.11         whacks = whacks, binary_ints = binary_ints,
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     2.3 @@ -562,7 +562,11 @@
     2.4                               string_for_vars ", " (sort int_ord xs))
     2.5         |> space_implode "\n"))
     2.6  
     2.7 -fun solve max_var (comps, clauses) =
     2.8 +(* The ML solver timeout should correspond more or less to the overhead of
     2.9 +   invoking an external prover. *)
    2.10 +val ml_solver_timeout = SOME (seconds 0.02)
    2.11 +
    2.12 +fun solve tac_timeout max_var (comps, clauses) =
    2.13    let
    2.14      val asgs = map_filter (fn [(x, (_, a))] => SOME (x, a) | _ => NONE) clauses
    2.15      fun do_assigns assigns =
    2.16 @@ -578,13 +582,22 @@
    2.17      else
    2.18        let
    2.19          (* use the first ML solver (to avoid startup overhead) *)
    2.20 -        val solvers = !SatSolver.solvers
    2.21 -                      |> filter (member (op =) ["dptsat", "dpll"] o fst)
    2.22 +        val (ml_solvers, nonml_solvers) =
    2.23 +          !SatSolver.solvers
    2.24 +          |> List.partition (member (op =) ["dptsat", "dpll"] o fst)
    2.25 +        val res =
    2.26 +          if null nonml_solvers then
    2.27 +            time_limit tac_timeout (snd (hd ml_solvers)) prop
    2.28 +          else
    2.29 +            time_limit ml_solver_timeout (snd (hd ml_solvers)) prop
    2.30 +            handle TimeLimit.TimeOut =>
    2.31 +                   time_limit tac_timeout (SatSolver.invoke_solver "auto") prop
    2.32        in
    2.33 -        case snd (hd solvers) prop of
    2.34 +        case res of
    2.35            SatSolver.SATISFIABLE assigns => do_assigns assigns
    2.36          | _ => (trace_msg (K "*** Unsolvable"); NONE)
    2.37        end
    2.38 +      handle TimeLimit.TimeOut => (trace_msg (K "*** Timed out"); NONE)
    2.39    end
    2.40  
    2.41  type mcontext =
    2.42 @@ -1192,8 +1205,8 @@
    2.43  fun amass f t (ms, accum) =
    2.44    let val (m, accum) = f t accum in (m :: ms, accum) end
    2.45  
    2.46 -fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
    2.47 -          (nondef_ts, def_ts) =
    2.48 +fun infer which no_harmless (hol_ctxt as {ctxt, tac_timeout, ...}) binarize
    2.49 +          alpha_T (nondef_ts, def_ts) =
    2.50    let
    2.51      val _ = trace_msg (fn () => "****** " ^ which ^ " analysis: " ^
    2.52                                  string_for_mtype MAlpha ^ " is " ^
    2.53 @@ -1208,7 +1221,7 @@
    2.54      val (def_ms, (gamma, cset)) =
    2.55        ([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
    2.56    in
    2.57 -    case solve (!max_fresh) cset of
    2.58 +    case solve tac_timeout (!max_fresh) cset of
    2.59        SOME asgs => (print_mcontext ctxt asgs gamma;
    2.60                      SOME (asgs, (nondef_ms, def_ms), !constr_mcache))
    2.61      | _ => NONE