author boehmes Thu, 15 Jan 2015 21:44:51 +0100 changeset 59374 2f5447b764f9 parent 59360 b1e5d552e8cc child 59375 e6acec6a6f6f
more detailed runtime statistics for Z3 proof reconstruction
```--- a/src/HOL/Tools/SMT/z3_replay.ML	Wed Jan 14 17:04:19 2015 +0100
+++ b/src/HOL/Tools/SMT/z3_replay.ML	Thu Jan 15 21:44:51 2015 +0100
@@ -208,6 +208,11 @@
fact_helper_ts prem_ids conjecture_id fact_helper_ids' steps}
end

+fun intermediate_statistics ctxt start total =
+  SMT_Config.statistics_msg ctxt (fn current =>
+    "Reconstructed " ^ string_of_int current ^ " of " ^ string_of_int total ^ " steps in " ^
+    string_of_int (Time.toMilliseconds (#elapsed (Timing.result start))) ^ " ms")
+
fun pretty_statistics total stats =
let
fun mean_of is =
@@ -236,10 +241,16 @@
ctxt3
|> put_simpset (Z3_Replay_Util.make_simpset ctxt3 [])
|> Config.put SAT.solver (Config.get ctxt3 SMT_Config.sat_solver)
-    val ({elapsed, ...}, (proofs, stats)) =
-      Timing.timing (fold (replay_step ctxt4 assumed) steps) (assumed, Symtab.empty)
+    val len = length steps
+    val start = Timing.start ()
+    val print_runtime_statistics = intermediate_statistics ctxt4 start len
+    fun blockwise f (i, x) y =
+      (if i > 0 andalso i mod 100 = 0 then print_runtime_statistics i else (); f x y)
+    val (proofs, stats) =
+      fold_index (blockwise (replay_step ctxt4 assumed)) steps (assumed, Symtab.empty)
+    val _ = print_runtime_statistics len
+    val total = Time.toMilliseconds (#elapsed (Timing.result start))
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```