--- a/src/HOL/Tools/SMT/smt_config.ML Mon Dec 14 21:02:57 2020 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Tue Dec 15 07:03:46 2020 +0100
@@ -185,8 +185,8 @@
val verbose = Attrib.setup_config_bool \<^binding>\<open>smt_verbose\<close> (K true)
val trace = Attrib.setup_config_bool \<^binding>\<open>smt_trace\<close> (K false)
val trace_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_verit\<close> (K false)
-val spy_verit_attr = Attrib.setup_config_bool \<^binding>\<open>smt_spy_verit\<close> (K false)
-val spy_z3 = Attrib.setup_config_bool \<^binding>\<open>smt_spy_z3\<close> (K false)
+val spy_verit_attr = Attrib.setup_config_bool \<^binding>\<open>smt_spy_verit\<close> (K true)
+val spy_z3 = Attrib.setup_config_bool \<^binding>\<open>smt_spy_z3\<close> (K true)
val trace_arith_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_arith_verit\<close> (K false)
val trace_verit_compression = Attrib.setup_config_bool \<^binding>\<open>verit_compress_proofs\<close> (K true)
val statistics = Attrib.setup_config_bool \<^binding>\<open>smt_statistics\<close> (K false)
--- a/src/HOL/Tools/SMT/smt_replay.ML Mon Dec 14 21:02:57 2020 +0100
+++ b/src/HOL/Tools/SMT/smt_replay.ML Tue Dec 15 07:03:46 2020 +0100
@@ -288,6 +288,8 @@
val message = f ()
val thy = Context.theory_long_name ((Context.theory_of o Context.Proof) ctxt)
val spying_version = "1"
+ val name = getenv "ISABELLE_SMT_SPY"
+ val filename = if name = "" then filename else filename ^ "_" ^ name
in
File.append (Path.explode ("$ISABELLE_HOME_USER/" ^ filename))
(spying_version ^ "; " ^ thy ^ "; " ^ (timestamp_format (Time.now ())) ^ ";\n" ^ message ^ "\n")
--- a/src/HOL/Tools/SMT/z3_replay.ML Mon Dec 14 21:02:57 2020 +0100
+++ b/src/HOL/Tools/SMT/z3_replay.ML Tue Dec 15 07:03:46 2020 +0100
@@ -169,6 +169,8 @@
val total = Time.toMilliseconds (#elapsed (Timing.result start))
val (_, Z3_Proof.Z3_Step {id, ...}) = split_last steps
val _ = SMT_Config.statistics_msg ctxt4 (Pretty.string_of o SMT_Replay.pretty_statistics "Z3" total) stats
+ val _ = SMT_Replay.spying (SMT_Config.spy_Z3 ctxt) ctxt
+ (fn () => SMT_Replay.print_stats (Symtab.dest stats)) "spy_z3"
in
Inttab.lookup proofs id |> the |> snd |> discharge rules outer_ctxt ctxt4
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Dec 14 21:02:57 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Tue Dec 15 07:03:46 2020 +0100
@@ -59,7 +59,7 @@
(case get_time y of
SOME time => next_timeout := time_min (time, !next_timeout)
| _ => ());
- SOME y
+ SOME (y, timeout)
end
end
in
@@ -171,6 +171,29 @@
val min_preplay_timeout = seconds 0.002
+fun string_of_method (Metis_Method _) = "metis"
+ | string_of_method Meson_Method = "meson"
+ | string_of_method (SMT_Method SMT_Z3) = "z3"
+ | string_of_method (SMT_Method (SMT_Verit str)) = "verit-" ^ str
+ | string_of_method SATx_Method = "sat"
+ | string_of_method Blast_Method = "blast"
+ | string_of_method Simp_Method = "simp"
+ | string_of_method Simp_Size_Method = "simp_size"
+ | string_of_method Auto_Method = "auto"
+ | string_of_method Fastforce_Method = "fastforce"
+ | string_of_method Force_Method = "force"
+ | string_of_method Moura_Method = "moura"
+ | string_of_method Linarith_Method = "linarith"
+ | string_of_method Presburger_Method = "presburger"
+ | string_of_method Algebra_Method = "algebra"
+
+fun time_of_replay (Played time) = string_of_int (Time.toMilliseconds time)
+ | time_of_replay (Play_Timed_Out _) = "-1"
+ | time_of_replay Play_Failed = "-2"
+
+fun print_stats stats =
+ fold (fn ((x,y), z) => fn msg => msg ^ string_of_method x ^ ": " ^ time_of_replay y ^ "\n") stats ""
+
fun preplay_isar_step ctxt chained timeout0 hopeless step =
let
fun preplay timeout meth = (meth, preplay_isar_step_for_method ctxt chained timeout meth step)
@@ -180,6 +203,8 @@
val meths = proof_methods_of_isar_step step |> subtract (op =) hopeless
in
par_list_map_filter_with_timeout get_time min_preplay_timeout timeout0 preplay meths
+ |> tap (fn times => SMT_Replay.spying true ctxt (fn () => print_stats times) "spy_sledgehammer")
+ |> map fst
|> sort (play_outcome_ord o apply2 snd)
end