src/HOL/Tools/SMT/smt_solver.ML

   val is_locally_installed: Proof.context -> string -> bool
   val is_remotely_available: Proof.context -> string -> bool
   val default_max_relevant: Proof.context -> string -> int
 
   (*filter*)
-  val smt_filter: bool -> Time.time -> Proof.state ->
-    ('a * (int option * thm)) list -> int ->
-    {outcome: SMT_Failure.failure option, used_facts: ('a * thm) list,
-    run_time_in_msecs: int option}
+  type 'a smt_filter_head_result = 'a list * (int option * thm) list *
+    (((int * thm) list * Proof.context) * (int * (int option * thm)) list)
+  val smt_filter_head: Time.time -> Proof.state ->
+    ('a * (int option * thm)) list -> int -> 'a smt_filter_head_result
+  val smt_filter_tail: bool -> 'a smt_filter_head_result ->
+    {outcome: SMT_Failure.failure option, used_facts: ('a * thm) list}
 
   (*tactic*)
   val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic
   val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic
 

   options: Proof.context -> string list,
   reconstruct: Proof.context -> string list * SMT_Translate.recon ->
     int list * thm,
   default_max_relevant: int }
 
-fun gen_solver name (info : solver_info) rm ctxt iwthms =
+fun gen_solver_head ctxt iwthms =
+  SMT_Normalize.normalize ctxt iwthms
+  |> rpair ctxt
+  |-> SMT_Monomorph.monomorph
+
+fun gen_solver_tail (name, info : solver_info) rm (iwthms', ctxt) iwthms =
   let
     val {env_var, is_remote, options, reconstruct, ...} = info
     val cmd = (rm, env_var, is_remote, name)
   in
-    SMT_Normalize.normalize ctxt iwthms
-    |> rpair ctxt
-    |-> SMT_Monomorph.monomorph
-    |> (fn (iwthms', ctxt') => invoke name cmd options iwthms' ctxt'
-    |> reconstruct ctxt')
+    (iwthms', ctxt)
+    |-> invoke name cmd options
+    |> reconstruct ctxt
     |> (fn (idxs, thm) => thm
     |> tap (fn _ => trace_assumptions ctxt iwthms idxs)
     |> pair idxs)
   end
 

 fun name_and_solver_of ctxt =
   let val name = C.solver_of ctxt
   in (name, get_info ctxt name) end
 
 val solver_name_of = fst o name_and_solver_of
-fun solver_of ctxt =
-  let val (name, raw_solver) = name_and_solver_of ctxt
-  in gen_solver name raw_solver end
+fun solver_of ctxt rm ctxt' =
+  `(gen_solver_head ctxt') #-> gen_solver_tail (name_and_solver_of ctxt) rm
 
 val available_solvers_of = Symtab.keys o Solvers.get o Context.Proof
 
 fun is_locally_installed ctxt name =
   let val {env_var, ...} = get_info ctxt name

 val has_topsort = Term.exists_type (Term.exists_subtype (fn
     TFree (_, []) => true
   | TVar (_, []) => true
   | _ => false))
 
-fun smt_solver rm ctxt iwthms =
-  (* without this test, we would run into problems when atomizing the rules: *)
+(* without this test, we would run into problems when atomizing the rules: *)
+fun check_topsort iwthms =
   if exists (has_topsort o Thm.prop_of o snd o snd) iwthms then
     raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("proof state " ^
       "contains the universal sort {}"))
-  else solver_of ctxt rm ctxt iwthms
+  else
+    ()
 
 val cnot = Thm.cterm_of @{theory} @{const Not}
 
-fun mk_result outcome xrules =
-  { outcome = outcome, used_facts = xrules, run_time_in_msecs = NONE }
-
-fun smt_filter run_remote time_limit st xwrules i =
+fun mk_result outcome xrules = { outcome = outcome, used_facts = xrules }
+
+type 'a smt_filter_head_result = 'a list * (int option * thm) list *
+  (((int * thm) list * Proof.context) * (int * (int option * thm)) list)
+
+fun smt_filter_head time_limit st xwrules i =
   let
     val ctxt =
       Proof.context_of st
       |> Config.put C.oracle false
       |> Config.put C.timeout (Time.toReal time_limit)

     val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
     fun negate ct = Thm.dest_comb ct ||> Thm.capply cnot |-> Thm.capply
     val cprop = negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl))
 
     val (xs, wthms) = split_list xwrules
-    val xrules = xs ~~ map snd wthms
-  in
-    wthms
-    |> map_index I
-    |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts))
-    |> smt_solver (SOME run_remote) ctxt'
+  in
+    (xs, wthms,
+     wthms
+     |> map_index I
+     |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts))
+     |> tap check_topsort
+     |> `(gen_solver_head ctxt'))
+  end
+
+fun smt_filter_tail run_remote (xs, wthms, head as ((_, ctxt), _)) =
+  let val xrules = xs ~~ map snd wthms in
+    head
+    |-> gen_solver_tail (name_and_solver_of ctxt) (SOME run_remote)
     |> distinct (op =) o fst
     |> map_filter (try (nth xrules))
     |> (if solver_name_of ctxt = "z3" (* FIXME *) then I else K xrules)
     |> mk_result NONE
   end
   handle SMT_Failure.SMT fail => mk_result (SOME fail) []
-  (* FIXME: measure runtime *)
-
 
 
 (* SMT tactic *)
 
 fun smt_tac' pass_exns ctxt rules =
   CONVERSION (SMT_Normalize.atomize_conv ctxt)
   THEN' Tactic.rtac @{thm ccontr}
   THEN' SUBPROOF (fn {context=ctxt', prems, ...} =>
     let
-      fun solve iwthms = snd (smt_solver NONE ctxt' iwthms)
+      val solve = snd o solver_of ctxt' NONE ctxt' o tap check_topsort
       val tag = "Solver " ^ C.solver_of ctxt' ^ ": "
       val str_of = prefix tag o SMT_Failure.string_of_failure ctxt'
       fun safe_solve iwthms =
         if pass_exns then SOME (solve iwthms)
         else (SOME (solve iwthms)