# HG changeset patch
# User wenzelm
# Date 1634574826 -7200
# Node ID 2ff001a8c9f22f0def7b15c441dd6ea75098f0a5
# Parent  dc1a7c10565b489f8d505826de6299df3dc91ed1# Parent  c87b403b03eb450d173491cf0e758ef3bd708cbf
merged

diff -r c87b403b03eb -r 2ff001a8c9f2 src/HOL/Mirabelle.thy
--- a/src/HOL/Mirabelle.thy	Mon Oct 18 11:49:01 2021 +0200
+++ b/src/HOL/Mirabelle.thy	Mon Oct 18 18:33:46 2021 +0200
@@ -2,11 +2,11 @@
     Author:     Jasmin Blanchette, TU Munich
     Author:     Sascha Boehme, TU Munich
     Author:     Makarius
-    Author:     Martin Desharnais, UniBw Munich
+    Author:     Martin Desharnais, UniBw Munich, MPI-INF Saarbrücken
 *)
 
 theory Mirabelle
-  imports Sledgehammer Predicate_Compile
+  imports Sledgehammer Predicate_Compile Presburger
 begin
 
 ML_file \<open>Tools/Mirabelle/mirabelle.ML\<close>
@@ -19,9 +19,10 @@
 
 ML_file \<open>Tools/Mirabelle/mirabelle_arith.ML\<close>
 ML_file \<open>Tools/Mirabelle/mirabelle_metis.ML\<close>
+ML_file \<open>Tools/Mirabelle/mirabelle_presburger.ML\<close>
 ML_file \<open>Tools/Mirabelle/mirabelle_quickcheck.ML\<close>
+ML_file \<open>Tools/Mirabelle/mirabelle_sledgehammer_filter.ML\<close>
 ML_file \<open>Tools/Mirabelle/mirabelle_sledgehammer.ML\<close>
-ML_file \<open>Tools/Mirabelle/mirabelle_sledgehammer_filter.ML\<close>
 ML_file \<open>Tools/Mirabelle/mirabelle_try0.ML\<close>
 
-end
\ No newline at end of file
+end
diff -r c87b403b03eb -r 2ff001a8c9f2 src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Mon Oct 18 11:49:01 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Mon Oct 18 18:33:46 2021 +0200
@@ -231,7 +231,10 @@
           (* initialize actions *)
           val contexts = actions |> map_index (fn (n, (label, name, args)) =>
             let
-              val make_action = the (get_action name);
+              val make_action =
+                (case get_action name of
+                  SOME f => f
+                | NONE => error "Unknown action");
               val action_subdir = if label = "" then string_of_int n ^ "." ^ name else label;
               val output_dir = Path.append mirabelle_output_dir (Path.basic action_subdir);
               val context =
diff -r c87b403b03eb -r 2ff001a8c9f2 src/HOL/Tools/Mirabelle/mirabelle_arith.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_arith.ML	Mon Oct 18 11:49:01 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_arith.ML	Mon Oct 18 18:33:46 2021 +0200
@@ -13,10 +13,9 @@
 fun make_action ({timeout, ...} : Mirabelle.action_context) =
   let
     fun run_action ({pre, ...} : Mirabelle.command) =
-      if Mirabelle.can_apply timeout Arith_Data.arith_tac pre then
-        "succeeded"
-      else
-        ""
+      (case Timing.timing (Mirabelle.can_apply timeout Arith_Data.arith_tac) pre of
+        ({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)"
+      | (_, false) => "failed")
   in {run_action = run_action, finalize = K ""} end
 
 val () = Mirabelle.register_action "arith" make_action
diff -r c87b403b03eb -r 2ff001a8c9f2 src/HOL/Tools/Mirabelle/mirabelle_presburger.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML	Mon Oct 18 18:33:46 2021 +0200
@@ -0,0 +1,21 @@
+(*  Title:      HOL/Mirabelle/Tools/mirabelle_presburger.ML
+    Author:     Martin Desharnais, MPI-INF Saarbrücken
+
+Mirabelle action: "presburger".
+*)
+
+structure Mirabelle_Presburger: MIRABELLE_ACTION =
+struct
+
+fun make_action ({timeout, ...} : Mirabelle.action_context) =
+  let
+    val _ = Timing.timing
+    fun run_action ({pre, ...} : Mirabelle.command) =
+      (case Timing.timing (Mirabelle.can_apply timeout (Cooper.tac true [] [])) pre of
+        ({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)"
+      | (_, false) => "failed")
+  in {run_action = run_action, finalize = K ""} end
+
+val () = Mirabelle.register_action "presburger" make_action
+
+end
diff -r c87b403b03eb -r 2ff001a8c9f2 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Oct 18 11:49:01 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Oct 18 18:33:46 2021 +0200
@@ -467,7 +467,7 @@
 
 val vampire_config : atp_config =
   let
-    val format = TFF (With_FOOL, Monomorphic)
+    val format = TFF (With_FOOL, Polymorphic)
   in
     {exec = (["VAMPIRE_HOME"], ["vampire"]),
      arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => fn _ =>
@@ -488,9 +488,9 @@
      prem_role = Hypothesis,
      best_slices = fn ctxt =>
        (* FUDGE *)
-       [(0.333, (((500, meshN), format, "mono_native", combs_or_liftingN, false), sosN)),
-        (0.333, (((150, meshN), format, "poly_tags??", combs_or_liftingN, false), sosN)),
-        (0.334, (((50, meshN), format, "mono_native", combs_or_liftingN, false), no_sosN))]
+       [(0.333, (((500, meshN), format, "mono_native_fool", combs_or_liftingN, false), sosN)),
+        (0.333, (((150, meshN), format, "poly_native_fool", combs_or_liftingN, false), sosN)),
+        (0.334, (((50, meshN), format, "mono_native_fool", combs_or_liftingN, false), no_sosN))]
        |> Config.get ctxt force_sos ? (hd #> apfst (K 1.0) #> single),
      best_max_mono_iters = default_max_mono_iters,
      best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}