# HG changeset patch
# User blanchet
# Date 1401783224 -7200
# Node ID 7fc7de3b387e650d80d213e58d0ca7efd1bbe1dc
# Parent  5ed907407041b7bf2a5a7a1996b4a164f2e6c113
tuning

diff -r 5ed907407041 -r 7fc7de3b387e src/HOL/Tools/SMT2/smt2_solver.ML
--- a/src/HOL/Tools/SMT2/smt2_solver.ML	Mon Jun 02 22:38:46 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Tue Jun 03 10:13:44 2014 +0200
@@ -8,28 +8,33 @@
 sig
   (*configuration*)
   datatype outcome = Unsat | Sat | Unknown
-  type solver_config = {
-    name: string,
-    class: Proof.context -> SMT2_Util.class,
-    avail: unit -> bool,
-    command: unit -> string list,
-    options: Proof.context -> string list,
-    default_max_relevant: int,
-    can_filter: bool,
-    outcome: string -> string list -> outcome * string list,
-    parse_proof: (Proof.context -> SMT2_Translate.replay_data -> string list ->
-      (int * (int * thm)) list * Z3_New_Proof.z3_step list) option,
-    replay: (Proof.context -> SMT2_Translate.replay_data -> string list -> thm) option}
+
+  type parsed_proof =
+    {outcome: SMT2_Failure.failure option,
+     fact_ids: (int * ((string * ATP_Problem_Generate.stature) * thm)) list,
+     atp_proof: unit -> (term, string) ATP_Proof.atp_step list}
+
+  type solver_config =
+    {name: string,
+     class: Proof.context -> SMT2_Util.class,
+     avail: unit -> bool,
+     command: unit -> string list,
+     options: Proof.context -> string list,
+     default_max_relevant: int,
+     can_filter: bool,
+     outcome: string -> string list -> outcome * string list,
+     parse_proof: (Proof.context -> SMT2_Translate.replay_data -> string list ->
+       (int * (int * thm)) list * Z3_New_Proof.z3_step list) option,
+     replay: (Proof.context -> SMT2_Translate.replay_data -> string list -> thm) option}
 
   (*registry*)
   val add_solver: solver_config -> theory -> theory
   val default_max_relevant: Proof.context -> string -> int
 
   (*filter*)
-  val smt2_filter: Proof.context -> thm -> ((string * 'a) * (int option * thm)) list -> int ->
-    Time.time ->
-    {outcome: SMT2_Failure.failure option, fact_ids: (int * ((string * 'a) * thm)) list,
-     atp_proof: unit -> (term, string) ATP_Proof.atp_step list}
+  val smt2_filter: Proof.context -> thm ->
+    ((string * ATP_Problem_Generate.stature) * (int option * thm)) list -> int -> Time.time ->
+    parsed_proof
 
   (*tactic*)
   val smt2_tac: Proof.context -> thm list -> int -> tactic
@@ -134,18 +139,23 @@
 
 datatype outcome = Unsat | Sat | Unknown
 
-type solver_config = {
-  name: string,
-  class: Proof.context -> SMT2_Util.class,
-  avail: unit -> bool,
-  command: unit -> string list,
-  options: Proof.context -> string list,
-  default_max_relevant: int,
-  can_filter: bool,
-  outcome: string -> string list -> outcome * string list,
-  parse_proof: (Proof.context -> SMT2_Translate.replay_data -> string list ->
-    (int * (int * thm)) list * Z3_New_Proof.z3_step list) option,
-  replay: (Proof.context -> SMT2_Translate.replay_data -> string list -> thm) option}
+type parsed_proof =
+  {outcome: SMT2_Failure.failure option,
+   fact_ids: (int * ((string * ATP_Problem_Generate.stature) * thm)) list,
+   atp_proof: unit -> (term, string) ATP_Proof.atp_step list}
+
+type solver_config =
+  {name: string,
+   class: Proof.context -> SMT2_Util.class,
+   avail: unit -> bool,
+   command: unit -> string list,
+   options: Proof.context -> string list,
+   default_max_relevant: int,
+   can_filter: bool,
+   outcome: string -> string list -> outcome * string list,
+   parse_proof: (Proof.context -> SMT2_Translate.replay_data -> string list ->
+     (int * (int * thm)) list * Z3_New_Proof.z3_step list) option,
+   replay: (Proof.context -> SMT2_Translate.replay_data -> string list -> thm) option}
 
 
 (* check well-sortedness *)
@@ -222,12 +232,8 @@
   let val name = SMT2_Config.solver_of ctxt
   in (name, get_info ctxt name) end
 
-fun apply_solver_and_parse_proof ctxt wthms0 =
-  let
-    val wthms = map (apsnd (check_topsort ctxt)) wthms0
-    val (name, {command, parse_proof, ...}) = name_and_info_of ctxt
-    val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt wthms) ctxt
-  in (parse_proof ctxt replay_data output, replay_data) end
+val default_max_relevant = #default_max_relevant oo get_info
+val can_filter = #can_filter o snd o name_and_info_of
 
 fun apply_solver_and_replay ctxt wthms0 =
   let
@@ -236,20 +242,14 @@
     val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt wthms) ctxt
   in replay ctxt replay_data output end
 
-val default_max_relevant = #default_max_relevant oo get_info
-val can_filter = #can_filter o snd o name_and_info_of 
-
 
 (* filter *)
 
 val no_id = ~1
 
-fun smt2_filter ctxt goal xwfacts i time_limit =
+fun smt2_filter ctxt0 goal xwfacts i time_limit =
   let
-    val ctxt =
-      ctxt
-      |> Config.put SMT2_Config.oracle false
-      |> Config.put SMT2_Config.timeout (Time.toReal time_limit)
+    val ctxt = ctxt0 |> Config.put SMT2_Config.timeout (Time.toReal time_limit)
 
     val ({context = ctxt, prems, concl, ...}, _) = Subgoal.focus ctxt i goal
     fun negate ct = Thm.dest_comb ct ||> Thm.apply @{cterm Not} |-> Thm.apply
@@ -267,10 +267,14 @@
     val conjecture_i = 0
     val prems_i = 1
     val facts_i = prems_i + length wprems
+
+    val wthms' = map (apsnd (check_topsort ctxt)) wthms
+    val (name, {command, parse_proof, ...}) = name_and_info_of ctxt
+    val (output, replay_data as {rewrite_rules, ...}) =
+      invoke name command (SMT2_Normalize.normalize ctxt wthms') ctxt
   in
-    wthms
-    |> apply_solver_and_parse_proof ctxt
-    |> (fn ((iidths0, z3_proof), {rewrite_rules, ...}) =>
+    parse_proof ctxt replay_data output
+    |> (fn (iidths0, z3_proof) =>
       let
         val iidths = if can_filter ctxt then iidths0 else map (apsnd (apfst (K no_id))) iwthms
 
@@ -285,8 +289,7 @@
           map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, prop_of th)) helper_ids @
           map (fn (_, ((s, _), th)) => (s, prop_of th)) fact_ids
         val fact_helper_ids =
-          map (fn (id, th) => (id, ATP_Util.short_thm_name ctxt th)) helper_ids @
-          map (fn (id, ((name, _), _)) => (id, name)) fact_ids
+          map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids @ map (apsnd (fst o fst)) fact_ids
       in
         {outcome = NONE, fact_ids = fact_ids,
          atp_proof = fn () => Z3_New_Isar.atp_proof_of_z3_proof ctxt rewrite_rules