src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 41007 75275c796b46
parent 41005 60d931de0709
child 41009 91495051c2ec
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.3 @@ -562,7 +562,11 @@
     1.4                               string_for_vars ", " (sort int_ord xs))
     1.5         |> space_implode "\n"))
     1.6  
     1.7 -fun solve max_var (comps, clauses) =
     1.8 +(* The ML solver timeout should correspond more or less to the overhead of
     1.9 +   invoking an external prover. *)
    1.10 +val ml_solver_timeout = SOME (seconds 0.02)
    1.11 +
    1.12 +fun solve tac_timeout max_var (comps, clauses) =
    1.13    let
    1.14      val asgs = map_filter (fn [(x, (_, a))] => SOME (x, a) | _ => NONE) clauses
    1.15      fun do_assigns assigns =
    1.16 @@ -578,13 +582,22 @@
    1.17      else
    1.18        let
    1.19          (* use the first ML solver (to avoid startup overhead) *)
    1.20 -        val solvers = !SatSolver.solvers
    1.21 -                      |> filter (member (op =) ["dptsat", "dpll"] o fst)
    1.22 +        val (ml_solvers, nonml_solvers) =
    1.23 +          !SatSolver.solvers
    1.24 +          |> List.partition (member (op =) ["dptsat", "dpll"] o fst)
    1.25 +        val res =
    1.26 +          if null nonml_solvers then
    1.27 +            time_limit tac_timeout (snd (hd ml_solvers)) prop
    1.28 +          else
    1.29 +            time_limit ml_solver_timeout (snd (hd ml_solvers)) prop
    1.30 +            handle TimeLimit.TimeOut =>
    1.31 +                   time_limit tac_timeout (SatSolver.invoke_solver "auto") prop
    1.32        in
    1.33 -        case snd (hd solvers) prop of
    1.34 +        case res of
    1.35            SatSolver.SATISFIABLE assigns => do_assigns assigns
    1.36          | _ => (trace_msg (K "*** Unsolvable"); NONE)
    1.37        end
    1.38 +      handle TimeLimit.TimeOut => (trace_msg (K "*** Timed out"); NONE)
    1.39    end
    1.40  
    1.41  type mcontext =
    1.42 @@ -1192,8 +1205,8 @@
    1.43  fun amass f t (ms, accum) =
    1.44    let val (m, accum) = f t accum in (m :: ms, accum) end
    1.45  
    1.46 -fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
    1.47 -          (nondef_ts, def_ts) =
    1.48 +fun infer which no_harmless (hol_ctxt as {ctxt, tac_timeout, ...}) binarize
    1.49 +          alpha_T (nondef_ts, def_ts) =
    1.50    let
    1.51      val _ = trace_msg (fn () => "****** " ^ which ^ " analysis: " ^
    1.52                                  string_for_mtype MAlpha ^ " is " ^
    1.53 @@ -1208,7 +1221,7 @@
    1.54      val (def_ms, (gamma, cset)) =
    1.55        ([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
    1.56    in
    1.57 -    case solve (!max_fresh) cset of
    1.58 +    case solve tac_timeout (!max_fresh) cset of
    1.59        SOME asgs => (print_mcontext ctxt asgs gamma;
    1.60                      SOME (asgs, (nondef_ms, def_ms), !constr_mcache))
    1.61      | _ => NONE