1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:08 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4       isar_shrink_factor: int,
     1.5       slicing: bool,
     1.6       timeout: Time.time,
     1.7 -     metis_timeout: Time.time,
     1.8 +     preplay_timeout: Time.time,
     1.9       expect: string}
    1.10  
    1.11    datatype prover_fact =
    1.12 @@ -279,7 +279,7 @@
    1.13     isar_shrink_factor: int,
    1.14     slicing: bool,
    1.15     timeout: Time.time,
    1.16 -   metis_timeout: Time.time,
    1.17 +   preplay_timeout: Time.time,
    1.18     expect: string}
    1.19  
    1.20  datatype prover_fact =
    1.21 @@ -870,23 +870,32 @@
    1.22        end
    1.23    in do_slice timeout 1 NONE Time.zeroTime end
    1.24  
    1.25 -(* taken from "Mirabelle" and generalized *)
    1.26 -fun can_apply timeout tac state i =
    1.27 +(* based on "Mirabelle.can_apply" and generalized *)
    1.28 +fun try_apply timeout tac state i =
    1.29    let
    1.30      val {context = ctxt, facts, goal} = Proof.goal state
    1.31      val full_tac = Method.insert_tac facts i THEN tac ctxt i
    1.32 -  in
    1.33 -    case try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal of
    1.34 -      SOME (SOME _) => true
    1.35 -    | _ => false
    1.36 +  in try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal end
    1.37 +
    1.38 +fun try_metis debug timeout ths =
    1.39 +  try_apply timeout (Config.put Metis_Tactics.verbose debug
    1.40 +                     #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths))
    1.41 +
    1.42 +datatype metis_try =
    1.43 +  Preplayed of string * Time.time |
    1.44 +  Preplay_Timed_Out |
    1.45 +  Preplay_Failed
    1.46 +
    1.47 +fun preplay debug timeout ths state i =
    1.48 +  let val timer = Timer.startRealTimer () in
    1.49 +    case try_metis debug timeout ths state i of
    1.50 +      SOME (SOME _) => Preplayed ("metis", Timer.checkRealTimer timer)
    1.51 +    | SOME NONE => Preplay_Failed
    1.52 +    | NONE => Preplay_Timed_Out
    1.53    end
    1.54  
    1.55 -fun can_apply_metis debug timeout ths =
    1.56 -  can_apply timeout (Config.put Metis_Tactics.verbose debug
    1.57 -                     #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths))
    1.58 -
    1.59  fun run_smt_solver auto name
    1.60 -        (params as {debug, verbose, blocking, metis_timeout, ...})
    1.61 +        (params as {debug, verbose, blocking, preplay_timeout, ...})
    1.62          minimize_command
    1.63          ({state, subgoal, subgoal_count, facts, smt_filter, ...}
    1.64           : prover_problem) =
    1.65 @@ -903,13 +912,13 @@
    1.66        case outcome of
    1.67          NONE =>
    1.68          let
    1.69 -          val (method, settings) =
    1.70 -            if can_apply_metis debug metis_timeout (map snd used_facts) state
    1.71 -                               subgoal then
    1.72 -              ("metis", "")
    1.73 -            else
    1.74 -              ("smt", if name = SMT_Solver.solver_name_of ctxt then ""
    1.75 -                      else "smt_solver = " ^ maybe_quote name)
    1.76 +          val (settings, method, time) =
    1.77 +            case preplay debug preplay_timeout (map snd used_facts) state
    1.78 +                         subgoal of
    1.79 +              Preplayed (method, time) => (method, "", SOME time)
    1.80 +            | _ => (if name = SMT_Solver.solver_name_of ctxt then ""
    1.81 +                    else "smt_solver = " ^ maybe_quote name,
    1.82 +                    "smt", NONE)
    1.83          in
    1.84            try_command_line (proof_banner auto blocking name)
    1.85                (apply_on_subgoal settings subgoal subgoal_count ^