# HG changeset patch
# User blanchet
# Date 1394713093 -3600
# Node ID b5d1d9c60341b80269df0a4cbacb065d484e6b03
# Parent  ffd99d397a9fd8c21318e90aa8891c30e345a5a3
have Sledgehammer generate Isar proofs from Z3 proofs

diff -r ffd99d397a9f -r b5d1d9c60341 src/HOL/SMT2.thy
--- a/src/HOL/SMT2.thy	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/SMT2.thy	Thu Mar 13 13:18:13 2014 +0100
@@ -100,11 +100,11 @@
 ML_file "Tools/SMT2/smt2_datatypes.ML"
 ML_file "Tools/SMT2/smt2_normalize.ML"
 ML_file "Tools/SMT2/smt2_translate.ML"
-ML_file "Tools/SMT2/smt2_solver.ML"
 ML_file "Tools/SMT2/smtlib2.ML"
 ML_file "Tools/SMT2/smtlib2_interface.ML"
+ML_file "Tools/SMT2/z3_new_proof.ML"
+ML_file "Tools/SMT2/smt2_solver.ML"
 ML_file "Tools/SMT2/z3_new_interface.ML"
-ML_file "Tools/SMT2/z3_new_proof.ML"
 ML_file "Tools/SMT2/z3_new_proof_tools.ML"
 ML_file "Tools/SMT2/z3_new_proof_literals.ML"
 ML_file "Tools/SMT2/z3_new_proof_rules.ML"
diff -r ffd99d397a9f -r b5d1d9c60341 src/HOL/Tools/SMT2/smt2_solver.ML
--- a/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Mar 13 13:18:13 2014 +0100
@@ -19,19 +19,21 @@
     outcome: string -> string list -> outcome * string list,
     cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list ->
       term list * term list) option,
-    replay: (Proof.context -> SMT2_Translate.replay_data -> string list -> int list * thm) option }
+    replay: (Proof.context -> SMT2_Translate.replay_data -> string list ->
+      (int list * Z3_New_Proof.z3_step list) * thm) option }
 
   (*registry*)
   val add_solver: solver_config -> theory -> theory
   val solver_name_of: Proof.context -> string
   val available_solvers_of: Proof.context -> string list
   val apply_solver: Proof.context -> (int * (int option * thm)) list ->
-    int list * thm
+    (int list * Z3_New_Proof.z3_step list) * thm
   val default_max_relevant: Proof.context -> string -> int
 
   (*filter*)
   val smt2_filter: Proof.context -> thm list -> thm -> ('a * (int option * thm)) list -> int ->
-    Time.time -> {outcome: SMT2_Failure.failure option, used_facts: ('a * thm) list}
+    Time.time -> {outcome: SMT2_Failure.failure option, used_facts: ('a * thm) list,
+      z3_steps: Z3_New_Proof.z3_step list}
 
   (*tactic*)
   val smt2_tac: Proof.context -> thm list -> int -> tactic
@@ -147,7 +149,8 @@
   outcome: string -> string list -> outcome * string list,
   cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list ->
     term list * term list) option,
-  replay: (Proof.context -> SMT2_Translate.replay_data -> string list -> int list * thm) option }
+  replay: (Proof.context -> SMT2_Translate.replay_data -> string list ->
+    (int list * Z3_New_Proof.z3_step list) * thm) option }
 
 
 (* registry *)
@@ -156,7 +159,8 @@
   command: unit -> string list,
   default_max_relevant: int,
   supports_filter: bool,
-  replay: Proof.context -> string list * SMT2_Translate.replay_data -> int list * thm }
+  replay: Proof.context -> string list * SMT2_Translate.replay_data ->
+    (int list * Z3_New_Proof.z3_step list) * thm }
 
 structure Solvers = Generic_Data
 (
@@ -173,12 +177,12 @@
       (Unsat, ls) =>
         if not (Config.get ctxt SMT2_Config.oracle) andalso is_some replay
         then the replay outer_ctxt replay_data ls
-        else ([], ocl ())
+        else (([], []), ocl ())
     | (result, ls) =>
         let
           val (ts, us) =
             (case cex_parser of SOME f => f ctxt replay_data ls | _ => ([], []))
-         in
+        in
           raise SMT2_Failure.SMT (SMT2_Failure.Counterexample {
             is_real_cex = (result = Sat),
             free_constraints = ts,
@@ -256,8 +260,6 @@
 
 val cnot = Thm.cterm_of @{theory} @{const Not}
 
-fun mk_result outcome xrules = { outcome = outcome, used_facts = xrules }
-
 fun smt2_filter ctxt facts goal xwthms i time_limit =
   let
     val ctxt =
@@ -276,18 +278,17 @@
 
     val xthms = map (apsnd snd) xwthms
 
-    fun filter_thms false = K xthms
-      | filter_thms true = map_filter (try (nth xthms)) o fst
+    val filter_thms = if supports_filter ctxt then K xthms else map_filter (try (nth xthms))
   in
     map snd xwthms
     |> map_index I
     |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts))
     |> check_topsorts ctxt
     |> apply_solver ctxt
-    |> filter_thms (supports_filter ctxt)
-    |> mk_result NONE
+    |> fst
+    |> (fn (is, z3_steps) => {outcome = NONE, used_facts = filter_thms is, z3_steps = z3_steps})
   end
-  handle SMT2_Failure.SMT fail => mk_result (SOME fail) []
+  handle SMT2_Failure.SMT fail => {outcome = SOME fail, used_facts = [], z3_steps = []}
 
 
 (* SMT tactic *)
@@ -311,7 +312,7 @@
     iwthms
     |> check_topsorts ctxt
     |> apply_solver ctxt
-    |>> trace_assumptions ctxt iwthms
+    |>> apfst (trace_assumptions ctxt iwthms)
     |> snd
 
   fun str_of ctxt fail =
diff -r ffd99d397a9f -r b5d1d9c60341 src/HOL/Tools/SMT2/z3_new_isar.ML
--- a/src/HOL/Tools/SMT2/z3_new_isar.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_isar.ML	Thu Mar 13 13:18:13 2014 +0100
@@ -78,9 +78,9 @@
     fun step_name_of id = (string_of_int id, [])
 
     (* FIXME: find actual conjecture *)
-    val id_of_last_asserted =
+    val id_of_conjecture =
       proof
-      |> rev |> find_first (fn Z3_New_Proof.Z3_Step {rule, ...} => rule = Z3_New_Proof.Asserted)
+      |> find_first (fn Z3_New_Proof.Z3_Step {rule, ...} => rule = Z3_New_Proof.Asserted)
       |> Option.map (fn Z3_New_Proof.Z3_Step {id, ...} => id)
 
     fun step_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) =
@@ -88,7 +88,7 @@
         val role =
           (case rule of
             Z3_New_Proof.Asserted =>
-              if id_of_last_asserted = SOME id then Negated_Conjecture else Hypothesis
+              if id_of_conjecture = SOME id then Negated_Conjecture else Hypothesis
           | Z3_New_Proof.Rewrite => Lemma
           | Z3_New_Proof.Rewrite_Star => Lemma
           | Z3_New_Proof.Skolemize => Lemma
diff -r ffd99d397a9f -r b5d1d9c60341 src/HOL/Tools/SMT2/z3_new_proof_replay.ML
--- a/src/HOL/Tools/SMT2/z3_new_proof_replay.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_proof_replay.ML	Thu Mar 13 13:18:13 2014 +0100
@@ -7,7 +7,8 @@
 
 signature Z3_NEW_PROOF_REPLAY =
 sig
-  val replay: Proof.context -> SMT2_Translate.replay_data -> string list -> int list * thm
+  val replay: Proof.context -> SMT2_Translate.replay_data -> string list ->
+    (int list * Z3_New_Proof.z3_step list) * thm
 end
 
 structure Z3_New_Proof_Replay: Z3_NEW_PROOF_REPLAY =
@@ -185,8 +186,8 @@
     val proofs = fold (replay_step ctxt3 assumed) steps assumed
     val (_, Z3_New_Proof.Z3_Step {id, ...}) = split_last steps
   in
-    if Config.get ctxt3 SMT2_Config.filter_only_facts then (is, TrueI)
-    else ([], Inttab.lookup proofs id |> the |> snd |> discharge rules outer_ctxt ctxt3)
+    if Config.get ctxt3 SMT2_Config.filter_only_facts then ((is, steps), TrueI)
+    else (([], steps), Inttab.lookup proofs id |> the |> snd |> discharge rules outer_ctxt ctxt3)
   end
 
 end
diff -r ffd99d397a9f -r b5d1d9c60341 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Mar 13 13:18:13 2014 +0100
@@ -39,6 +39,7 @@
 open ATP_Proof_Reconstruct
 open Sledgehammer_Util
 open Sledgehammer_Proof_Methods
+open Sledgehammer_Isar
 open Sledgehammer_Prover
 
 val smt2_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt2_builtins} (K true)
@@ -153,16 +154,19 @@
         val birth = Timer.checkRealTimer timer
         val _ = if debug then Output.urgent_message "Invoking SMT solver..." else ()
 
-        val (outcome, used_facts) =
+        val {outcome, used_facts, z3_steps} =
           SMT2_Solver.smt2_filter ctxt [] goal weighted_facts i slice_timeout
-          |> (fn {outcome, used_facts} => (outcome, used_facts))
           handle exn =>
-            if Exn.is_interrupt exn then reraise exn
-            else (ML_Compiler.exn_message exn |> SMT2_Failure.Other_Failure |> SOME, [])
+            if Exn.is_interrupt exn then
+              reraise exn
+            else
+              {outcome = SOME (SMT2_Failure.Other_Failure (ML_Compiler.exn_message exn)),
+               used_facts = [], z3_steps = []}
 
         val death = Timer.checkRealTimer timer
         val outcome0 = if is_none outcome0 then SOME outcome else outcome0
         val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
+        val timeout = Time.- (timeout, Timer.checkRealTimer timer)
 
         val too_many_facts_perhaps =
           (case outcome of
@@ -172,8 +176,6 @@
           | SOME (SMT2_Failure.Abnormal_Termination _) => true (* kind of *)
           | SOME SMT2_Failure.Out_Of_Memory => true
           | SOME (SMT2_Failure.Other_Failure _) => true)
-
-        val timeout = Time.- (timeout, Timer.checkRealTimer timer)
       in
         if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
            Time.> (timeout, Time.zeroTime) then
@@ -205,13 +207,14 @@
           end
         else
           {outcome = if is_none outcome then NONE else the outcome0, used_facts = used_facts,
-           used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
+           used_from = map (apsnd snd) weighted_facts, z3_steps = z3_steps, run_time = time_so_far}
       end
   in
     do_slice timeout 1 NONE Time.zeroTime
   end
 
-fun run_smt2_solver mode name (params as {debug, verbose, smt_proofs, preplay_timeout, ...})
+fun run_smt2_solver mode name (params as {debug, verbose, isar_proofs, compress_isar,
+      try0_isar, smt_proofs, minimize, preplay_timeout, ...})
     minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
@@ -223,7 +226,7 @@
       end
 
     val weighted_factss = factss |> map (apsnd weight_facts)
-    val {outcome, used_facts = used_pairs, used_from, run_time} =
+    val {outcome, used_facts = used_pairs, used_from, z3_steps, run_time} =
       smt2_filter_loop name params state goal subgoal weighted_factss
     val used_facts = used_pairs |> map fst
     val outcome = outcome |> Option.map failure_of_smt2_failure
@@ -236,13 +239,17 @@
              SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
          fn preplay =>
             let
+              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy z3_steps
+              val isar_params =
+                K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
+                   minimize <> SOME false, atp_proof, goal)
               val one_line_params =
                 (preplay, proof_banner mode name, used_facts,
                  choose_minimize_command thy params minimize_command name preplay, subgoal,
                  subgoal_count)
               val num_chained = length (#facts (Proof.goal state))
             in
-              one_line_proof_text num_chained one_line_params
+              proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params
             end,
          if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
       | SOME failure =>