split replay and proof parsing for Z3

--- a/src/HOL/SMT2.thy	Mon Jun 02 17:34:25 2014 +0200
+++ b/src/HOL/SMT2.thy	Mon Jun 02 17:34:26 2014 +0200
@@ -306,15 +306,6 @@
 
 declare [[ smt2_trace = false ]]
 
-text {*
-From the set of assumptions given to the SMT solver, those assumptions
-used in the proof are traced when the following option is set to
-@{term true}.  This only works for Z3 when it runs in non-oracle mode
-(see options @{text smt2_solver} and @{text smt2_oracle} above).
-*}
-
-declare [[ smt2_trace_used_facts = false ]]
-
 
 subsection {* Schematic rules for Z3 proof reconstruction *}
 

--- a/src/HOL/Tools/SMT2/smt2_config.ML	Mon Jun 02 17:34:25 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_config.ML	Mon Jun 02 17:34:26 2014 +0200
@@ -28,11 +28,9 @@
   val read_only_certificates: bool Config.T
   val verbose: bool Config.T
   val trace: bool Config.T
-  val trace_used_facts: bool Config.T
   val monomorph_limit: int Config.T
   val monomorph_instances: int Config.T
   val infer_triggers: bool Config.T
-  val filter_only_facts: bool Config.T
   val debug_files: string Config.T
   val sat_solver: string Config.T
 
@@ -155,11 +153,9 @@
 val read_only_certificates = Attrib.setup_config_bool @{binding smt2_read_only_certificates} (K false)
 val verbose = Attrib.setup_config_bool @{binding smt2_verbose} (K true)
 val trace = Attrib.setup_config_bool @{binding smt2_trace} (K false)
-val trace_used_facts = Attrib.setup_config_bool @{binding smt2_trace_used_facts} (K false)
 val monomorph_limit = Attrib.setup_config_int @{binding smt2_monomorph_limit} (K 10)
 val monomorph_instances = Attrib.setup_config_int @{binding smt2_monomorph_instances} (K 500)
 val infer_triggers = Attrib.setup_config_bool @{binding smt2_infer_triggers} (K false)
-val filter_only_facts = Attrib.setup_config_bool @{binding smt2_filter_only_facts} (K false)
 val debug_files = Attrib.setup_config_string @{binding smt2_debug_files} (K "")
 val sat_solver = Attrib.setup_config_string @{binding smt2_sat_solver} (K "cdclite")
 

--- a/src/HOL/Tools/SMT2/smt2_solver.ML	Mon Jun 02 17:34:25 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Mon Jun 02 17:34:26 2014 +0200
@@ -17,8 +17,9 @@
     default_max_relevant: int,
     can_filter: bool,
     outcome: string -> string list -> outcome * string list,
-    replay: (Proof.context -> SMT2_Translate.replay_data -> string list ->
-      ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm) option}
+    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
@@ -142,8 +143,9 @@
   default_max_relevant: int,
   can_filter: bool,
   outcome: string -> string list -> outcome * string list,
-  replay: (Proof.context -> SMT2_Translate.replay_data -> string list ->
-    ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm) option}
+  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 *)
@@ -164,8 +166,9 @@
   command: unit -> string list,
   default_max_relevant: int,
   can_filter: bool,
-  finish: Proof.context -> SMT2_Translate.replay_data -> string list ->
-    ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm}
+  parse_proof: Proof.context -> SMT2_Translate.replay_data -> string list ->
+    (int * (int * thm)) list * Z3_New_Proof.z3_step list,
+  replay: Proof.context -> SMT2_Translate.replay_data -> string list -> thm}
 
 structure Solvers = Generic_Data
 (
@@ -176,35 +179,42 @@
 )
 
 local
-  fun finish outcome replay ocl outer_ctxt
+  fun parse_proof outcome parse_proof0 outer_ctxt replay_data output =
+    (case outcome output of
+      (Unsat, ls) =>
+        (case parse_proof0 of SOME pp => pp outer_ctxt replay_data ls | NONE => ([], []))
+    | (result, _) =>
+        raise SMT2_Failure.SMT (SMT2_Failure.Counterexample {
+          is_real_cex = (result = Sat), free_constraints = [], const_defs = []}))
+
+  fun replay outcome replay0 oracle outer_ctxt
       (replay_data as {context = ctxt, ...} : SMT2_Translate.replay_data) output =
     (case outcome output of
       (Unsat, ls) =>
-        if not (Config.get ctxt SMT2_Config.oracle) andalso is_some replay
-        then the replay outer_ctxt replay_data ls
-        else (([], []), ocl ())
-    | (result, ls) =>
+        if not (Config.get ctxt SMT2_Config.oracle) andalso is_some replay0
+        then the replay0 outer_ctxt replay_data ls
+        else oracle ()
+    | (result, _) =>
         raise SMT2_Failure.SMT (SMT2_Failure.Counterexample {
-          is_real_cex = (result = Sat),
-          free_constraints = [],
-          const_defs = []}))
+          is_real_cex = (result = Sat), free_constraints = [], const_defs = []}))
 
-  val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const False})
+  val cfalse = Thm.cterm_of @{theory} @{prop False}
 in
 
 fun add_solver ({name, class, avail, command, options, default_max_relevant, can_filter,
-    outcome, replay} : solver_config) =
+    outcome, parse_proof = parse_proof0, replay = replay0} : solver_config) =
   let
-    fun solver ocl = {
+    fun solver oracle = {
       command = command,
       default_max_relevant = default_max_relevant,
       can_filter = can_filter,
-      finish = finish (outcome name) replay ocl}
+      parse_proof = parse_proof (outcome name) parse_proof0,
+      replay = replay (outcome name) replay0 oracle}
 
     val info = {name = name, class = class, avail = avail, options = options}
   in
-    Thm.add_oracle (Binding.name name, K cfalse) #-> (fn (_, ocl) =>
-    Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
+    Thm.add_oracle (Binding.name name, K cfalse) #-> (fn (_, oracle) =>
+    Context.theory_map (Solvers.map (Symtab.update_new (name, solver oracle)))) #>
     Context.theory_map (SMT2_Config.add_solver info)
   end
 
@@ -216,12 +226,19 @@
   let val name = SMT2_Config.solver_of ctxt
   in (name, get_info ctxt name) end
 
-fun apply_solver ctxt wthms0 =
+fun apply_solver_and_parse_proof ctxt wthms0 =
   let
     val wthms = map (apsnd (check_topsort ctxt)) wthms0
-    val (name, {command, finish, ...}) = name_and_info_of ctxt
+    val (name, {command, parse_proof, ...}) = name_and_info_of ctxt
     val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt wthms) ctxt
-  in (finish ctxt replay_data output, replay_data) end
+  in (parse_proof ctxt replay_data output, replay_data) end
+
+fun apply_solver_and_replay ctxt wthms0 =
+  let
+    val wthms = map (apsnd (check_topsort ctxt)) wthms0
+    val (name, {command, replay, ...}) = name_and_info_of ctxt
+    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 
@@ -236,7 +253,6 @@
     val ctxt =
       ctxt
       |> Config.put SMT2_Config.oracle false
-      |> Config.put SMT2_Config.filter_only_facts true
       |> Config.put SMT2_Config.timeout (Time.toReal time_limit)
 
     val ({context = ctxt, prems, concl, ...}, _) = Subgoal.focus ctxt i goal
@@ -257,8 +273,8 @@
     val facts_i = prems_i + length wprems
   in
     wthms
-    |> apply_solver ctxt
-    |> (fn (((iidths0, z3_proof), _), {rewrite_rules, ...}) =>
+    |> apply_solver_and_parse_proof ctxt
+    |> (fn ((iidths0, z3_proof), {rewrite_rules, ...}) =>
       let
         val iidths = if can_filter ctxt then iidths0 else map (apsnd (apfst (K no_id))) iwthms
         fun id_of_index i = the_default no_id (Option.map fst (AList.lookup (op =) iidths i))
@@ -280,25 +296,10 @@
 (* SMT tactic *)
 
 local
-  fun trace_assumptions ctxt wfacts iidths =
-    let val used = map_filter (try (snd o nth wfacts) o fst) iidths in
-      if Config.get ctxt SMT2_Config.trace_used_facts andalso length wfacts > 0 then
-        tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
-          (map (Display.pretty_thm ctxt) used)))
-      else ()
-    end
-
-  fun solve ctxt wfacts =
-    wfacts
-    |> apply_solver ctxt
-    |> fst
-    |>> apfst (trace_assumptions ctxt wfacts)
-    |> snd
-
   fun str_of ctxt fail =
     "Solver " ^ SMT2_Config.solver_of ctxt ^ ": " ^ SMT2_Failure.string_of_failure ctxt fail
 
-  fun safe_solve ctxt wfacts = SOME (solve ctxt wfacts)
+  fun safe_solve ctxt wfacts = SOME (apply_solver_and_replay ctxt wfacts)
     handle
       SMT2_Failure.SMT (fail as SMT2_Failure.Counterexample _) =>
         (SMT2_Config.verbose_msg ctxt (str_of ctxt) fail; NONE)
@@ -319,7 +320,7 @@
 in
 
 val smt2_tac = tac safe_solve
-val smt2_tac' = tac (SOME oo solve)
+val smt2_tac' = tac (SOME oo apply_solver_and_replay)
 
 end
 

--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Mon Jun 02 17:34:25 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Mon Jun 02 17:34:26 2014 +0200
@@ -58,6 +58,7 @@
   can_filter = false,
   outcome =
     on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
+  parse_proof = NONE,
   replay = NONE }
 
 end
@@ -78,6 +79,7 @@
   default_max_relevant = 350 (* FUDGE *),
   can_filter = false,
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
+  parse_proof = NONE,
   replay = NONE }
 
 
@@ -143,6 +145,7 @@
   default_max_relevant = 350 (* FUDGE *),
   can_filter = true,
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
+  parse_proof = SOME Z3_New_Replay.parse_proof,
   replay = SOME Z3_New_Replay.replay }
 
 end

--- a/src/HOL/Tools/SMT2/z3_new_replay.ML	Mon Jun 02 17:34:25 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay.ML	Mon Jun 02 17:34:26 2014 +0200
@@ -7,8 +7,9 @@
 
 signature Z3_NEW_REPLAY =
 sig
-  val replay: Proof.context -> SMT2_Translate.replay_data -> string list ->
-    ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm
+  val parse_proof: Proof.context -> SMT2_Translate.replay_data -> string list ->
+    (int * (int * thm)) list * Z3_New_Proof.z3_step list
+  val replay: Proof.context -> SMT2_Translate.replay_data -> string list -> thm
 end
 
 structure Z3_New_Replay: Z3_NEW_REPLAY =
@@ -172,24 +173,28 @@
   singleton (Proof_Context.export inner_ctxt outer_ctxt)
   #> discharge_assms outer_ctxt (make_discharge_rules rules)
 
+fun parse_proof outer_ctxt
+    ({context=ctxt, typs, terms, rewrite_rules, assms} : SMT2_Translate.replay_data) output =
+  let
+    val (steps, ctxt2) = Z3_New_Proof.parse typs terms output ctxt
+    val ((iidths, _), _) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2
+  in
+    (iidths, steps)
+  end
+
 fun replay outer_ctxt
     ({context=ctxt, typs, terms, rewrite_rules, assms} : SMT2_Translate.replay_data) output =
   let
     val (steps, ctxt2) = Z3_New_Proof.parse typs terms output ctxt
-    val ((iidths, rules), (ctxt3, assumed)) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2
+    val ((_, rules), (ctxt3, assumed)) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2
+    val ctxt4 =
+      ctxt3
+      |> put_simpset (Z3_New_Replay_Util.make_simpset ctxt3 [])
+      |> Config.put SAT.solver (Config.get ctxt3 SMT2_Config.sat_solver)
+    val proofs = fold (replay_step ctxt4 assumed) steps assumed
+    val (_, Z3_New_Proof.Z3_Step {id, ...}) = split_last steps
   in
-    if Config.get ctxt3 SMT2_Config.filter_only_facts then
-      ((iidths, steps), TrueI)
-    else
-      let
-        val ctxt4 =
-          ctxt3
-          |> put_simpset (Z3_New_Replay_Util.make_simpset ctxt3 [])
-          |> Config.put SAT.solver (Config.get ctxt3 SMT2_Config.sat_solver)
-        val proofs = fold (replay_step ctxt4 assumed) steps assumed
-        val (_, Z3_New_Proof.Z3_Step {id, ...}) = split_last steps
-        val thm = Inttab.lookup proofs id |> the |> snd |> discharge rules outer_ctxt ctxt4
-      in (([], steps), thm) end
+    Inttab.lookup proofs id |> the |> snd |> discharge rules outer_ctxt ctxt4
   end
 
 end