--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Nov 12 18:47:07 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Nov 12 00:10:16 2021 +0100
@@ -153,10 +153,8 @@
Const_Types of ctr_optim |
No_Types
-type syntax = {with_ite: bool}
-
datatype type_enc =
- Native of order * fool * syntax * polymorphism * type_level |
+ Native of order * fool * polymorphism * type_level |
Guards of polymorphism * type_level |
Tags of polymorphism * type_level
@@ -165,17 +163,20 @@
fun is_type_enc_native (Native _) = true
| is_type_enc_native _ = false
-fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Free, _, _, _, _)) = false
- | is_type_enc_full_higher_order (Native (Higher_Order _, _, _, _, _)) = true
+fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Free, _, _, _)) = false
+ | is_type_enc_full_higher_order (Native (Higher_Order _, _, _, _)) = true
| is_type_enc_full_higher_order _ = false
-fun is_type_enc_fool (Native (_, With_FOOL, _, _, _)) = true
+fun is_type_enc_fool (Native (_, With_FOOL _, _, _)) = true
| is_type_enc_fool _ = false
-fun is_type_enc_higher_order (Native (Higher_Order _, _, _, _, _)) = true
+fun is_type_enc_higher_order (Native (Higher_Order _, _, _, _)) = true
| is_type_enc_higher_order _ = false
-fun has_type_enc_ite (Native (_, _, {with_ite, ...}, _, _)) = with_ite
+
+fun has_type_enc_ite (Native (_, With_FOOL {with_ite, ...}, _, _)) = with_ite
| has_type_enc_ite _ = false
+fun has_type_enc_let (Native (_, With_FOOL {with_let, ...}, _, _)) = with_let
+ | has_type_enc_let _ = false
-fun polymorphism_of_type_enc (Native (_, _, _, poly, _)) = poly
+fun polymorphism_of_type_enc (Native (_, _, poly, _)) = poly
| polymorphism_of_type_enc (Guards (poly, _)) = poly
| polymorphism_of_type_enc (Tags (poly, _)) = poly
@@ -188,7 +189,7 @@
fun is_type_enc_mangling type_enc =
polymorphism_of_type_enc type_enc = Mangled_Monomorphic
-fun level_of_type_enc (Native (_, _, _, _, level)) = level
+fun level_of_type_enc (Native (_, _, _, level)) = level
| level_of_type_enc (Guards (_, level)) = level
| level_of_type_enc (Tags (_, level)) = level
@@ -391,7 +392,7 @@
fun default c = const_prefix ^ lookup_const c
in
fun make_fixed_const _ \<^const_name>\<open>HOL.eq\<close> = tptp_old_equal
- | make_fixed_const (SOME (Native (Higher_Order THF_With_Choice, _, _, _, _))) c =
+ | make_fixed_const (SOME (Native (Higher_Order THF_With_Choice, _, _, _))) c =
if c = choice_const then tptp_choice else default c
| make_fixed_const _ c = default c
end
@@ -680,34 +681,50 @@
fun native_of_string s =
let
+ val (with_let, s) =
+ (case try (unsuffix "_let") s of
+ SOME s => (true, s)
+ | NONE => (false, s))
+ val (with_ite, s) =
+ (case try (unsuffix "_ite") s of
+ SOME s => (true, s)
+ | NONE => (false, s))
+ val syntax = {with_ite = with_ite, with_let = with_let}
val (fool, core) =
(case try (unsuffix "_fool") s of
- SOME s => (With_FOOL, s)
+ SOME s => (With_FOOL syntax, s)
| NONE => (Without_FOOL, s))
- val syntax = {with_ite = (fool = With_FOOL)}
+
+ fun validate_syntax (type_enc as Native (_, Without_FOOL, _, _)) =
+ if with_ite orelse with_let then
+ error "\"ite\" and \"let\" options require \"native_fool\" or \"native_higher\"."
+ else
+ type_enc
+ | validate_syntax type_enc = type_enc
in
(case (core, poly) of
("native", SOME poly) =>
(case (poly, level) of
(Mangled_Monomorphic, _) =>
if is_type_level_uniform level then
- Native (First_Order, fool, syntax, Mangled_Monomorphic, level)
+ Native (First_Order, fool, Mangled_Monomorphic, level)
else
raise Same.SAME
| (Raw_Monomorphic, _) => raise Same.SAME
- | (poly, All_Types) => Native (First_Order, fool, syntax, poly, All_Types))
+ | (poly, All_Types) => Native (First_Order, fool, poly, All_Types))
| ("native_higher", SOME poly) =>
(case (poly, level) of
(_, Nonmono_Types _) => raise Same.SAME
| (_, Undercover_Types) => raise Same.SAME
| (Mangled_Monomorphic, _) =>
if is_type_level_uniform level then
- Native (Higher_Order THF_With_Choice, fool, syntax, Mangled_Monomorphic, level)
+ Native (Higher_Order THF_With_Choice, With_FOOL syntax, Mangled_Monomorphic, level)
else
raise Same.SAME
| (poly as Raw_Polymorphic _, All_Types) =>
- Native (Higher_Order THF_With_Choice, fool, syntax, poly, All_Types)
+ Native (Higher_Order THF_With_Choice, With_FOOL syntax, poly, All_Types)
| _ => raise Same.SAME))
+ |> validate_syntax
end
fun nonnative_of_string core =
@@ -752,28 +769,28 @@
fun adjust_hologic hologic (Higher_Order hologic') = Higher_Order (min_hologic hologic hologic')
| adjust_hologic _ type_enc = type_enc
-fun adjust_fool Without_FOOL _ = Without_FOOL
- | adjust_fool _ fool = fool
+fun adjust_syntax {with_ite = ite1, with_let = let1} {with_ite = ite2, with_let = let2} =
+ {with_ite = ite1 andalso ite2, with_let = let1 andalso let2}
+
+fun adjust_fool (With_FOOL syntax) (With_FOOL syntax') = With_FOOL (adjust_syntax syntax syntax')
+ | adjust_fool _ _ = Without_FOOL
fun no_type_classes Type_Class_Polymorphic = Raw_Polymorphic With_Phantom_Type_Vars
| no_type_classes poly = poly
-fun adjust_type_enc (THF (fool, Polymorphic, hologic))
- (Native (order, fool', syntax, poly, level)) =
- Native (adjust_hologic hologic order, adjust_fool fool fool', syntax, no_type_classes poly,
- level)
- | adjust_type_enc (THF (fool, Monomorphic, hologic)) (Native (order, fool', syntax, _, level)) =
- Native (adjust_hologic hologic order, adjust_fool fool fool', syntax, Mangled_Monomorphic,
+fun adjust_type_enc (THF (poly, syntax, hologic)) (Native (order, fool, poly', level)) =
+ Native (adjust_hologic hologic order, adjust_fool (With_FOOL syntax) fool,
+ (case poly of Polymorphic => no_type_classes poly' | Monomorphic => Mangled_Monomorphic),
level)
- | adjust_type_enc (TFF (fool, Monomorphic)) (Native (_, fool', syntax, _, level)) =
- Native (First_Order, adjust_fool fool fool', syntax, Mangled_Monomorphic, level)
- | adjust_type_enc (DFG Polymorphic) (Native (_, _, syntax, poly, level)) =
- Native (First_Order, Without_FOOL, syntax, poly, level)
- | adjust_type_enc (DFG Monomorphic) (Native (_, _, syntax, _, level)) =
- Native (First_Order, Without_FOOL, syntax, Mangled_Monomorphic, level)
- | adjust_type_enc (TFF (fool, _)) (Native (_, fool', syntax, poly, level)) =
- Native (First_Order, adjust_fool fool fool', syntax, no_type_classes poly, level)
- | adjust_type_enc format (Native (_, _, _, poly, level)) =
+ | adjust_type_enc (TFF (poly, fool)) (Native (_, fool', poly', level)) =
+ Native (First_Order, adjust_fool fool fool',
+ (case poly of Polymorphic => no_type_classes poly' | Monomorphic => Mangled_Monomorphic),
+ level)
+ | adjust_type_enc (DFG Polymorphic) (Native (_, _, poly, level)) =
+ Native (First_Order, Without_FOOL, poly, level)
+ | adjust_type_enc (DFG Monomorphic) (Native (_, _, _, level)) =
+ Native (First_Order, Without_FOOL, Mangled_Monomorphic, level)
+ | adjust_type_enc format (Native (_, _, poly, level)) =
adjust_type_enc format (Guards (no_type_classes poly, level))
| adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
(if is_type_enc_sound type_enc then Tags else Guards) stuff
@@ -949,8 +966,8 @@
T_args
else
(case type_enc of
- Native (_, _, _, Raw_Polymorphic _, _) => T_args
- | Native (_, _, _, Type_Class_Polymorphic, _) => T_args
+ Native (_, _, Raw_Polymorphic _, _) => T_args
+ | Native (_, _, Type_Class_Polymorphic, _) => T_args
| _ =>
let
fun gen_type_args _ _ [] = []
@@ -1086,7 +1103,7 @@
val tm_args =
tm_args @
(case type_enc of
- Native (_, _, _, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
+ Native (_, _, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
[ATerm ((TYPE_name, ty_args), [])]
| _ => [])
in AAtom (ATerm ((cl, ty_args), tm_args)) end
@@ -1215,6 +1232,7 @@
let
val is_fool = is_type_enc_fool type_enc
val has_ite = has_type_enc_ite type_enc
+ val has_let = has_type_enc_let type_enc
fun tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _])) [] =
(* Eta-expand "!!" and "??", to work around LEO-II, Leo-III, and Satallax parser
limitations. This works in conjunction with special code in "ATP_Problem" that uses the
@@ -1270,7 +1288,7 @@
let val argc = length args in
if has_ite andalso s = "c_If" andalso argc >= 3 then
IConst (`I tptp_ite, T, [])
- else if is_fool andalso s = "c_Let" andalso argc >= 2 then
+ else if has_let andalso s = "c_Let" andalso argc >= 2 then
IConst (`I tptp_let, T, [])
else
(case proxify_const s of
@@ -1881,10 +1899,10 @@
|> class_membs_of_types type_enc add_sorts_on_tvar
|> map (class_atom type_enc)))
#> (case type_enc of
- Native (_, _, _, Type_Class_Polymorphic, _) =>
+ Native (_, _, Type_Class_Polymorphic, _) =>
mk_atyquant AForall (map (fn TVar (z as (_, S)) =>
(AType ((tvar_name z, []), []), map (`make_class) (normalize_classes S) )) Ts)
- | Native (_, _, _, Raw_Polymorphic _, _) =>
+ | Native (_, _, Raw_Polymorphic _, _) =>
mk_atyquant AForall (map (fn TVar (z as _) => (AType ((tvar_name z, []), []), [])) Ts)
| _ => mk_aquant AForall (map (fn TVar z => (tvar_name z, NONE)) Ts)))
@@ -1940,10 +1958,11 @@
in
fold (fn ((helper_s, needs_sound), ths) =>
let
- fun map_syntax_of_type_enc f (Native (order, fool, syntax, polymorphism, type_level)) =
- Native (order, fool, f syntax, polymorphism, type_level)
- | map_syntax_of_type_enc _ type_enc = type_enc
- val remove_ite_syntax = map_syntax_of_type_enc (K {with_ite = false})
+ fun map_syntax f (Native (order, With_FOOL syntax, polymorphism, type_level)) =
+ Native (order, With_FOOL (f syntax), polymorphism, type_level)
+ | map_syntax _ type_enc = type_enc
+ val remove_ite_syntax = map_syntax
+ (fn {with_let, ...} => {with_ite = false, with_let = with_let})
in
if (needs_sound andalso not sound) orelse
(helper_s <> unmangled_s andalso
@@ -2313,7 +2332,7 @@
fun decl_lines_of_classes type_enc =
(case type_enc of
- Native (_, _, _, Raw_Polymorphic phantoms, _) => map (decl_line_of_class phantoms)
+ Native (_, _, Raw_Polymorphic phantoms, _) => map (decl_line_of_class phantoms)
| _ => K [])
fun sym_decl_table_of_facts thy type_enc sym_tab (conjs, facts, extra_tms) =
@@ -2375,7 +2394,7 @@
? (fold (fold add_fact_syms) [conjs, facts]
#> fold add_iterm_syms extra_tms
#> (case type_enc of
- Native (_, _, _, Raw_Polymorphic phantoms, _) =>
+ Native (_, _, Raw_Polymorphic phantoms, _) =>
phantoms = Without_Phantom_Type_Vars ? add_TYPE_const ()
| Native _ => I
| _ => fold add_undefined_const (var_types ())))
@@ -2815,9 +2834,8 @@
if lam_trans = keep_lamsN andalso not (is_type_enc_full_higher_order type_enc) then liftingN
else lam_trans
val simp_options =
- let val simp = not (is_type_enc_fool type_enc) in
- {if_simps = simp, let_simps = simp}
- end
+ {if_simps = not (has_type_enc_ite type_enc),
+ let_simps = not (has_type_enc_let type_enc)}
val (classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) =
translate_formulas simp_options ctxt prem_role format type_enc lam_trans presimp hyp_ts
concl_t facts
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Nov 12 18:47:07 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Nov 12 00:10:16 2021 +0100
@@ -67,6 +67,13 @@
(* ATP configuration *)
+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 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 TH1 = THF (Monomorphic, {with_ite = true, with_let = true}, THF_With_Choice)
+
val default_max_mono_iters = 3 (* FUDGE *)
val default_max_new_mono_instances = 100 (* FUDGE *)
@@ -160,7 +167,6 @@
val term_order =
Attrib.setup_config_string \<^binding>\<open>atp_term_order\<close> (K smartN)
-
(* agsyHOL *)
val agsyhol_config : atp_config =
@@ -172,7 +178,7 @@
prem_role = Hypothesis,
best_slices =
(* FUDGE *)
- K [(1.0, (((60, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
+ K [(1.0, (((60, ""), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -194,7 +200,7 @@
prem_role = Hypothesis,
best_slices = fn _ =>
(* FUDGE *)
- [(1.0, (((100, ""), TFF (Without_FOOL, Polymorphic), "poly_native", liftingN, false), ""))],
+ [(1.0, (((100, ""), TF1, "poly_native", liftingN, false), ""))],
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -294,11 +300,11 @@
val heuristic = Config.get ctxt e_selection_heuristic
val (format, enc, main_lam_trans) =
if string_ord (getenv "E_VERSION", "2.7") <> LESS then
- (THF (With_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher_fool", keep_lamsN)
+ (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher_ite", keep_lamsN)
else if string_ord (getenv "E_VERSION", "2.6") <> LESS then
- (THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN)
+ (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN)
else
- (THF (Without_FOOL, Monomorphic, THF_Lambda_Free), "mono_native_higher", combsN)
+ (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN)
in
(* FUDGE *)
if heuristic = e_smartN then
@@ -357,7 +363,7 @@
prem_role = Hypothesis,
best_slices =
(* FUDGE *)
- K [(1.0, (((40, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
+ K [(1.0, (((40, ""), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -378,7 +384,7 @@
prem_role = Hypothesis,
best_slices =
(* FUDGE *)
- K [(1.0, (((150, ""), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
+ K [(1.0, (((150, ""), THF (Polymorphic, {with_ite = true, with_let = true}, THF_Without_Choice), "mono_native_higher_ite_let", keep_lamsN, false), ""))],
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -401,7 +407,7 @@
prem_role = Hypothesis,
best_slices =
(* FUDGE *)
- K [(1.0, (((150, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
+ K [(1.0, (((150, ""), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -465,35 +471,31 @@
" --proof_extra free --forced_options avatar=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0"
val vampire_config : atp_config =
- let
- val format = TFF (With_FOOL, Polymorphic)
- in
- {exec = (["VAMPIRE_HOME"], ["vampire"]),
- arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => fn _ =>
- [vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^
- " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ File.bash_path problem
- |> sos = sosN ? prefix "--sos on "],
- proof_delims =
- [("=========== Refutation ==========",
- "======= End of refutation =======")] @
- tstp_proof_delims,
- known_failures =
- [(GaveUp, "UNPROVABLE"),
- (GaveUp, "CANNOT PROVE"),
- (Unprovable, "Satisfiability detected"),
- (Unprovable, "Termination reason: Satisfiable"),
- (Interrupted, "Aborted by signal SIGINT")] @
- known_szs_status_failures,
- prem_role = Hypothesis,
- best_slices = fn ctxt =>
- (* FUDGE *)
- [(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 *)}
- end
+ {exec = (["VAMPIRE_HOME"], ["vampire"]),
+ arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => fn _ =>
+ [vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^
+ " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ File.bash_path problem
+ |> sos = sosN ? prefix "--sos on "],
+ proof_delims =
+ [("=========== Refutation ==========",
+ "======= End of refutation =======")] @
+ tstp_proof_delims,
+ known_failures =
+ [(GaveUp, "UNPROVABLE"),
+ (GaveUp, "CANNOT PROVE"),
+ (Unprovable, "Satisfiability detected"),
+ (Unprovable, "Termination reason: Satisfiable"),
+ (Interrupted, "Aborted by signal SIGINT")] @
+ known_szs_status_failures,
+ prem_role = Hypothesis,
+ best_slices = fn ctxt =>
+ (* FUDGE *)
+ [(0.333, (((500, meshN), TX1, "mono_native_fool_ite_let", combs_or_liftingN, false), sosN)),
+ (0.333, (((150, meshN), TX1, "poly_native_fool_ite_let", combs_or_liftingN, false), sosN)),
+ (0.334, (((50, meshN), TX1, "mono_native_fool_ite_let", 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 *)}
val vampire = (vampireN, fn () => vampire_config)
@@ -501,24 +503,20 @@
(* Z3 with TPTP syntax (half experimental, half legacy) *)
val z3_tptp_config : atp_config =
- let
- val format = TFF (Without_FOOL, Monomorphic)
- in
- {exec = (["Z3_TPTP_HOME"], ["z3_tptp"]),
- arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
- ["-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ File.bash_path problem],
- proof_delims = [("SZS status Theorem", "")],
- known_failures = known_szs_status_failures,
- prem_role = Hypothesis,
- best_slices =
- (* FUDGE *)
- K [(0.5, (((250, meshN), format, "mono_native", combsN, false), "")),
- (0.25, (((125, mepoN), format, "mono_native", combsN, false), "")),
- (0.125, (((62, mashN), format, "mono_native", combsN, false), "")),
- (0.125, (((31, meshN), format, "mono_native", combsN, false), ""))],
- best_max_mono_iters = default_max_mono_iters,
- best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
- end
+ {exec = (["Z3_TPTP_HOME"], ["z3_tptp"]),
+ arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
+ ["-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ File.bash_path problem],
+ proof_delims = [("SZS status Theorem", "")],
+ known_failures = known_szs_status_failures,
+ prem_role = Hypothesis,
+ best_slices =
+ (* FUDGE *)
+ K [(0.5, (((250, meshN), TF0, "mono_native", combsN, false), "")),
+ (0.25, (((125, mepoN), TF0, "mono_native", combsN, false), "")),
+ (0.125, (((62, mashN), TF0, "mono_native", combsN, false), "")),
+ (0.125, (((31, meshN), TF0, "mono_native", combsN, false), ""))],
+ best_max_mono_iters = default_max_mono_iters,
+ best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
@@ -527,8 +525,9 @@
val zipperposition_config : atp_config =
let
- val format = THF (Without_FOOL, Polymorphic, THF_Without_Choice)
- val enc = ((512, "meshN"), format, "mono_native_higher", keep_lamsN, false)
+ val format =
+ THF (Polymorphic, {with_ite = true, with_let = false}, THF_Without_Choice)
+ val enc = ((512, "meshN"), format, "mono_native_higher_fool_ite", keep_lamsN, false)
in
{exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => fn _ =>
@@ -627,26 +626,26 @@
val remote_agsyhol =
remotify_atp agsyhol "agsyHOL" ["1.0", "1"]
- (K (((60, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
+ (K (((60, ""), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
val remote_alt_ergo =
remotify_atp alt_ergo "Alt-Ergo" ["0.95.2"]
- (K (((250, ""), TFF (Without_FOOL, Polymorphic), "poly_native", keep_lamsN, false), "") (* FUDGE *))
+ (K (((250, ""), TF1, "poly_native", keep_lamsN, false), "") (* FUDGE *))
val remote_e =
remotify_atp e "E" ["2.0", "1.9.1", "1.8"]
- (K (((750, ""), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "") (* FUDGE *))
+ (K (((750, ""), TF0, "mono_native", combsN, false), "") (* FUDGE *))
val remote_iprover =
remotify_atp iprover "iProver" ["0.99"]
(K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
val remote_leo2 =
remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"]
- (K (((40, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", liftingN, false), "") (* FUDGE *))
+ (K (((40, ""), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", liftingN, false), "") (* FUDGE *))
val remote_leo3 =
remotify_atp leo3 "Leo-III" ["1.1"]
- (K (((150, ""), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *))
+ (K (((150, ""), THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *))
val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??"
val remote_zipperposition =
remotify_atp zipperposition "Zipperpin" ["2.1", "2.0"]
- (K (((512, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
+ (K (((512, ""), THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
(* Dummy prover *)
@@ -669,12 +668,11 @@
val dummy_fof_config = dummy_config Hypothesis dummy_fof_format "mono_guards??" false
val dummy_fof = (dummy_fofN, fn () => dummy_fof_config)
-val dummy_tfx_format = TFF (With_FOOL, Polymorphic)
-val dummy_tfx_config = dummy_config Hypothesis dummy_tfx_format "mono_native_fool" false
+val dummy_tfx_config = dummy_config Hypothesis TX1 "mono_native_fool_ite_let" false
val dummy_tfx = (dummy_tfxN, fn () => dummy_tfx_config)
-val dummy_thf_format = THF (With_FOOL, Polymorphic, THF_With_Choice)
-val dummy_thf_config = dummy_config Hypothesis dummy_thf_format "mono_native_higher_fool" false
+val dummy_thf_config =
+ dummy_config Hypothesis TH1 "mono_native_higher_ite_let" false
val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)