add option to specify spy file name draft
authorMathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
Tue, 15 Dec 2020 07:03:46 +0100
changeset 73146 fb5ee0d0b76c
parent 73145 6a26a955308e
child 73147 0ab6a765d228
add option to specify spy file name
src/HOL/Tools/SMT/smt_config.ML
src/HOL/Tools/SMT/smt_replay.ML
src/HOL/Tools/SMT/z3_replay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- 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