--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Tue Mar 05 21:44:52 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Mar 06 09:43:25 2024 +0100
@@ -61,6 +61,7 @@
val TF0 = TFF (Monomorphic, Without_FOOL)
val TF1 = TFF (Polymorphic, Without_FOOL)
val TX0 = TFF (Monomorphic, With_FOOL {with_ite = true, with_let = true})
+val TX0_MINUS = TFF (Monomorphic, With_FOOL {with_ite = false, with_let = false})
val TX1 = TFF (Polymorphic, With_FOOL {with_ite = true, with_let = true})
val TH0 = THF (Monomorphic, {with_ite = true, with_let = true}, THF_With_Choice)
val TH0_MINUS = THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice)
@@ -177,7 +178,9 @@
(* E *)
-val e_config : atp_config =
+local
+
+fun make_e_config max_new_mono_insts good_slices : atp_config =
{exec = (["E_HOME"], ["eprover-ho", "eprover"]),
arguments = fn abduce => fn _ => fn extra_options => fn timeout => fn problem =>
["--tstp-in --tstp-out --silent " ^
@@ -195,8 +198,11 @@
known_szs_status_failures,
prem_role = Conjecture,
generate_isabelle_info = false,
- good_slices =
- let
+ good_slices = K good_slices,
+ good_max_mono_iters = default_max_mono_iters,
+ good_max_new_mono_instances = max_new_mono_insts}
+
+val old_e_config : atp_config = make_e_config default_max_new_mono_instances (let
val (format, type_enc, lam_trans, extra_options) =
if string_ord (getenv "E_VERSION", "3.0") <> LESS then
(* '$ite' support appears to be unsound. *)
@@ -207,17 +213,47 @@
(THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN, "--auto-schedule")
in
(* FUDGE *)
- K [((1000 (* infinity *), false, false, 512, meshN), (format, type_enc, lam_trans, false, extra_options)),
- ((1, true, false, 128, mashN), (format, type_enc, combsN, false, extra_options)),
- ((1000 (* infinity *), false, false, 1024, meshN), (format, type_enc, lam_trans, false, extra_options)),
- ((1000 (* infinity *), false, false, 64, mepoN), (format, type_enc, lam_trans, false, extra_options)),
- ((1000 (* infinity *), false, false, 724, meshN), (TF0, "poly_guards??", lam_trans, false, extra_options)),
- ((1000 (* infinity *), false, true, 256, mepoN), (format, type_enc, liftingN, false, extra_options))]
- end,
- good_max_mono_iters = default_max_mono_iters,
- good_max_new_mono_instances = default_max_new_mono_instances}
+ [((1000 (* infinity *), false, false, 512, meshN), (format, type_enc, lam_trans, false, extra_options)),
+ ((1, true, false, 128, mashN), (format, type_enc, combsN, false, extra_options)),
+ ((1000 (* infinity *), false, false, 1024, meshN), (format, type_enc, lam_trans, false, extra_options)),
+ ((1000 (* infinity *), false, false, 64, mepoN), (format, type_enc, lam_trans, false, extra_options)),
+ ((1000 (* infinity *), false, false, 724, meshN), (TF0, "poly_guards??", lam_trans, false, extra_options)),
+ ((1000 (* infinity *), false, true, 256, mepoN), (format, type_enc, liftingN, false, extra_options))]
+ end)
-val e = (eN, fn () => e_config)
+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, "")))]
+
+in
+
+val e = (eN, fn () =>
+ if string_ord (getenv "E_VERSION", "3.0") <> LESS then
+ new_e_config
+ else
+ old_e_config)
+
+end
(* iProver *)
@@ -423,9 +459,8 @@
((2, false, false, 128, meshN), (TX1, "mono_native", liftingN, false, no_sosN))]
val new_vampire_config : atp_config =
- let val infinity = 1000 in
- (* FUDGE: this solved 998/1500 (66.53 %) using MePo when testing *)
- make_vampire_config new_vampire_basic_options 256
+ (* FUDGE: this solved 998/1500 (66.53 %) using MePo when testing *)
+ make_vampire_config new_vampire_basic_options 256
[(((2, false, false, 512, meshN), (TX0, "mono_native_fool", liftingN, false, ""))),
(((2, false, false, 2048, meshN), (TX0, "mono_native_fool", combsN, false, ""))),
(((2, false, false, 128, meshN), (TX0, "mono_native_fool", liftingN, false, ""))),
@@ -445,7 +480,6 @@
(((2, false, false, 512, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, ""))),
(((2, false, false, 512, meshN), (TX0, "mono_native_fool", combsN, false, ""))),
(((2, false, false, 1024, meshN), (TX1, "poly_native_fool", combsN, false, "")))]
- end
in