optionally display statistics for Z3 proof reconstruction

--- a/src/HOL/Tools/SMT/smt_config.ML	Mon Dec 29 16:21:33 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Mon Dec 29 22:14:13 2014 +0100
@@ -29,6 +29,7 @@
   val read_only_certificates: bool Config.T
   val verbose: bool Config.T
   val trace: bool Config.T
+  val statistics: bool Config.T
   val monomorph_limit: int Config.T
   val monomorph_instances: int Config.T
   val infer_triggers: bool Config.T
@@ -42,6 +43,7 @@
   (*diagnostics*)
   val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
   val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit
+  val statistics_msg: Proof.context -> ('a -> string) -> 'a -> unit
 
   (*certificates*)
   val select_certificates: string -> Context.generic -> Context.generic
@@ -174,6 +176,7 @@
 val read_only_certificates = Attrib.setup_config_bool @{binding smt_read_only_certificates} (K false)
 val verbose = Attrib.setup_config_bool @{binding smt_verbose} (K true)
 val trace = Attrib.setup_config_bool @{binding smt_trace} (K false)
+val statistics = Attrib.setup_config_bool @{binding smt_statistics} (K false)
 val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10)
 val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500)
 val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false)
@@ -186,8 +189,8 @@
 fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ()
 
 fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose)
-
 fun trace_msg ctxt = cond_trace (Config.get ctxt trace)
+fun statistics_msg ctxt = cond_trace (Config.get ctxt statistics)
 
 
 (* tools *)

--- a/src/HOL/Tools/SMT/z3_replay.ML	Mon Dec 29 16:21:33 2014 +0100
+++ b/src/HOL/Tools/SMT/z3_replay.ML	Mon Dec 29 22:14:13 2014 +0100
@@ -65,13 +65,16 @@
     under_fixes (Z3_Replay_Methods.method_for rule) ctxt
       (if is_fix_step then (map snd nthms, []) else ([], nthms)) fixes concl
 
-fun replay_step ctxt assumed (step as Z3_Proof.Z3_Step {id, prems, fixes, ...}) proofs =
+fun replay_step ctxt assumed (step as Z3_Proof.Z3_Step {id, rule, prems, fixes, ...}) state =
   let
+    val (proofs, stats) = state
     val nthms = map (the o Inttab.lookup proofs) prems
-    val replay = replay_thm ctxt assumed nthms
-    val thm = SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay step
+    val replay = Timing.timing (replay_thm ctxt assumed nthms)
+    val ({elapsed, ...}, thm) =
+      SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay step
       handle TimeLimit.TimeOut => raise SMT_Failure.SMT SMT_Failure.Time_Out
-  in Inttab.update (id, (fixes, thm)) proofs end
+    val stats' = Symtab.cons_list (Z3_Proof.string_of_rule rule, Time.toMilliseconds elapsed) stats
+  in (Inttab.update (id, (fixes, thm)) proofs, stats') end
 
 local
   val remove_trigger = mk_meta_eq @{thm trigger_def}
@@ -205,6 +208,25 @@
        fact_helper_ts prem_ids conjecture_id fact_helper_ids' steps}
   end
 
+fun pretty_statistics total stats =
+  let
+    fun mean_of is =
+      let
+        val len = length is
+        val mid = len div 2
+      in if len mod 2 = 0 then (nth is (mid - 1) + nth is mid) div 2 else nth is mid end
+    fun pretty_item name p = Pretty.item (Pretty.separate ":" [Pretty.str name, p])
+    fun pretty (name, milliseconds) = pretty_item name (Pretty.block (Pretty.separate "," [
+      Pretty.str (string_of_int (length milliseconds) ^ " occurrences") ,
+      Pretty.str (string_of_int (mean_of milliseconds) ^ " ms mean time"),
+      Pretty.str (string_of_int (fold Integer.max milliseconds 0) ^ " ms maximum time"),
+      Pretty.str (string_of_int (fold Integer.add milliseconds 0) ^ " ms total time")]))
+  in
+    Pretty.big_list "Z3 proof reconstruction statistics:" (
+      pretty_item "total time" (Pretty.str (string_of_int total ^ " ms")) ::
+      map pretty (Symtab.dest stats))
+  end
+
 fun replay outer_ctxt
     ({context = ctxt, typs, terms, rewrite_rules, assms, ...} : SMT_Translate.replay_data) output =
   let
@@ -214,8 +236,11 @@
       ctxt3
       |> put_simpset (Z3_Replay_Util.make_simpset ctxt3 [])
       |> Config.put SAT.solver (Config.get ctxt3 SMT_Config.sat_solver)
-    val proofs = fold (replay_step ctxt4 assumed) steps assumed
+    val ({elapsed, ...}, (proofs, stats)) =
+      Timing.timing (fold (replay_step ctxt4 assumed) steps) (assumed, Symtab.empty)
     val (_, Z3_Proof.Z3_Step {id, ...}) = split_last steps
+    val total = Time.toMilliseconds elapsed
+    val _ = SMT_Config.statistics_msg ctxt4 (Pretty.string_of o pretty_statistics total) stats
   in
     Inttab.lookup proofs id |> the |> snd |> discharge rules outer_ctxt ctxt4
   end