# HG changeset patch
# User desharna
# Date 1634548559 -7200
# Node ID 2c093a3167d1cb619522335710865acc9ffe50c1
# Parent  64c0d78d2f19ce9aa7d7ab803df25d356eef5a01
added Mirabelle action presburger

diff -r 64c0d78d2f19 -r 2c093a3167d1 src/HOL/Mirabelle.thy
--- 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
diff -r 64c0d78d2f19 -r 2c093a3167d1 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 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