Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clone of 62c039ce397c for Isabelle2025 release;
authorwenzelm
Fri, 28 Feb 2025 20:38:47 +0100
changeset 82227 bb2ea9e80c33
parent 82226 8e770d3cc85c
child 82228 79dfbf3bafc1
clone of 62c039ce397c for Isabelle2025 release;
src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Sun Feb 23 22:37:36 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Feb 28 20:38:47 2025 +0100
@@ -223,27 +223,32 @@
 
 val new_e_config : atp_config =
   (* FUDGE: this solved 950/1500 (63.33 %) using MePo when testing *)
-  make_e_config 128
-    [(((2, false, false,  128, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, ""))),
-     (((2, false, false, 1024, meshN), (TH0, "mono_native_higher", keep_lamsN, false, ""))),
-     (((2, false, false,  128, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, ""))),
-     (((2, false, false, 2048, meshN), (TF0, "mono_native", combsN, false, ""))),
-     (((2, false, false,  512, meshN), (TF0, "mono_native", liftingN, false, ""))),
-     (((2, false, false, 1024, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, ""))),
-     (((2, false, false,   64, meshN), (TH0, "mono_native_higher", keep_lamsN, false, ""))),
-     (((2, false, false,  512, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, ""))),
-     (((2, false, false,   32, meshN), (TF0, "mono_native", liftingN, false, ""))),
-     (((2, false, false, 2048, meshN), (TH0, "mono_native_higher", keep_lamsN, false, ""))),
-     (((2, false, false,  256, meshN), (TH0, "mono_native_higher", keep_lamsN, false, ""))),
-     (((2, false, false,  512, meshN), (TF0, "mono_native", combsN, false, ""))),
-     (((2, false, false, 1024, meshN), (TF0, "mono_native", liftingN, false, ""))),
-     (((2, false, false,   16, meshN), (TH0, "mono_native_higher", keep_lamsN, false, ""))),
-     (((2, false, false,  512, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, ""))),
-     (((2, false, false,   64, meshN), (TF0, "mono_native", liftingN, false, ""))),
-     (((2, false, false,  128, meshN), (TF0, "mono_native", combsN, false, ""))),
-     (((2, false, false, 2048, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, ""))),
-     (((2, false, false,  128, meshN), (TX0_MINUS, "mono_native_fool", combsN, false, ""))),
-     (((2, false, false, 2048, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, "")))]
+  let
+    val extra_options = "--auto-schedule"
+    val good_slices =
+      [(((2, false, false,  128, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, extra_options))),
+       (((2, false, false, 1024, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))),
+       (((2, false, false,  128, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, extra_options))),
+       (((2, false, false, 2048, meshN), (TF0, "mono_native", combsN, false, extra_options))),
+       (((2, false, false,  512, meshN), (TF0, "mono_native", liftingN, false, extra_options))),
+       (((2, false, false, 1024, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, extra_options))),
+       (((2, false, false,   64, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))),
+       (((2, false, false,  512, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, extra_options))),
+       (((2, false, false,   32, meshN), (TF0, "mono_native", liftingN, false, extra_options))),
+       (((2, false, false, 2048, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))),
+       (((2, false, false,  256, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))),
+       (((2, false, false,  512, meshN), (TF0, "mono_native", combsN, false, extra_options))),
+       (((2, false, false, 1024, meshN), (TF0, "mono_native", liftingN, false, extra_options))),
+       (((2, false, false,   16, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))),
+       (((2, false, false,  512, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, extra_options))),
+       (((2, false, false,   64, meshN), (TF0, "mono_native", liftingN, false, extra_options))),
+       (((2, false, false,  128, meshN), (TF0, "mono_native", combsN, false, extra_options))),
+       (((2, false, false, 2048, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, extra_options))),
+       (((2, false, false,  128, meshN), (TX0_MINUS, "mono_native_fool", combsN, false, extra_options))),
+       (((2, false, false, 2048, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, extra_options)))]
+    in
+      make_e_config 128 good_slices
+    end
 
 in
isabelle