--- 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
--- 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 =
--- 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
--- /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
--- 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 *)}