--- a/src/HOL/Mirabelle.thy Mon Oct 18 11:11:59 2021 +0200
+++ b/src/HOL/Mirabelle.thy Mon Oct 18 11:15:59 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML Mon Oct 18 11:15:59 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