# HG changeset patch
# User blanchet
# Date 1355280422 -3600
# Node ID d5dc28fafd9d926b6f45d4d587e2baba9e74ebf0
# Parent  3c6ac2da2f4519f918e3eaf114db8fc7aa10e0cc
made MaSh evaluation driver work with SMT solvers

diff -r 3c6ac2da2f45 -r d5dc28fafd9d src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Wed Dec 12 02:47:45 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Wed Dec 12 03:47:02 2012 +0100
@@ -33,7 +33,7 @@
   (*filter*)
   type 'a smt_filter_data =
     ('a * thm) list * ((int * thm) list * Proof.context)
-  val smt_filter_preprocess: Proof.state ->
+  val smt_filter_preprocess: Proof.context -> thm list -> thm ->
     ('a * (int option * thm)) list -> int -> 'a smt_filter_data
   val smt_filter_apply: Time.time -> 'a smt_filter_data ->
     {outcome: SMT_Failure.failure option, used_facts: ('a * thm) list}
@@ -272,15 +272,14 @@
 
 type 'a smt_filter_data = ('a * thm) list * ((int * thm) list * Proof.context)
 
-fun smt_filter_preprocess st xwthms i =
+fun smt_filter_preprocess ctxt facts goal xwthms i =
   let
     val ctxt =
-      Proof.context_of st
+      ctxt
       |> Config.put SMT_Config.oracle false
       |> Config.put SMT_Config.drop_bad_facts true
       |> Config.put SMT_Config.filter_only_facts true
 
-    val {facts, goal, ...} = Proof.goal st
     val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
     fun negate ct = Thm.dest_comb ct ||> Thm.apply cnot |-> Thm.apply
     val cprop =
diff -r 3c6ac2da2f45 -r d5dc28fafd9d src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 12 02:47:45 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 12 03:47:02 2012 +0100
@@ -957,7 +957,7 @@
 fun smt_filter_loop ctxt name
                     ({debug, verbose, overlord, max_mono_iters,
                       max_new_mono_instances, timeout, slice, ...} : params)
-                    state i =
+                    state goal i =
   let
     val max_slices = if slice then Config.get ctxt smt_max_slices else 1
     val repair_context =
@@ -1001,8 +1001,9 @@
         val birth = Timer.checkRealTimer timer
         val _ =
           if debug then Output.urgent_message "Invoking SMT solver..." else ()
+        val state_facts = these (try (#facts o Proof.goal) state)
         val (outcome, used_facts) =
-          SMT_Solver.smt_filter_preprocess state facts i
+          SMT_Solver.smt_filter_preprocess ctxt state_facts goal facts i
           |> SMT_Solver.smt_filter_apply slice_timeout
           |> (fn {outcome, used_facts} => (outcome, used_facts))
           handle exn => if Exn.is_interrupt exn then
@@ -1051,14 +1052,14 @@
 
 fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...})
         minimize_command
-        ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
+        ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
   let
     val ctxt = Proof.context_of state
     val num_facts = length facts
     val facts = facts ~~ (0 upto num_facts - 1)
                 |> map (smt_weighted_fact ctxt num_facts)
     val {outcome, used_facts = used_pairs, run_time} =
-      smt_filter_loop ctxt name params state subgoal facts
+      smt_filter_loop ctxt name params state goal subgoal facts
     val used_facts = used_pairs |> map fst
     val outcome = outcome |> Option.map failure_from_smt_failure
     val (preplay, message, message_tail) =