--- a/src/Doc/Sledgehammer/document/root.tex Tue May 22 11:08:37 2018 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Tue May 22 17:15:02 2018 +0200
@@ -768,6 +768,10 @@
Be aware that E-Par is experimental software. It has been known to generate
zombie processes. Use at your own risks.
+\item[\labelitemi] \textbf{\textit{ehoh}:} Ehoh is an experimental version of
+E that supports a $\lambda$-free fragment of higher-order logic. Use at your
+own risks.
+
\item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure
instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}.
To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the
--- a/src/HOL/Tools/ATP/atp_problem.ML Tue May 22 11:08:37 2018 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue May 22 17:15:02 2018 +0200
@@ -32,7 +32,7 @@
gen_simp : bool}
datatype polymorphism = Monomorphic | Polymorphic
- datatype thf_choice = THF_Without_Choice | THF_With_Choice
+ datatype thf_choice = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
datatype atp_format =
CNF |
@@ -188,7 +188,7 @@
gen_simp : bool}
datatype polymorphism = Monomorphic | Polymorphic
-datatype thf_choice = THF_Without_Choice | THF_With_Choice
+datatype thf_choice = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
datatype atp_format =
CNF |
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue May 22 11:08:37 2018 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue May 22 17:15:02 2018 +0200
@@ -162,6 +162,9 @@
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
+ | is_type_enc_full_higher_order _ = false
fun is_type_enc_higher_order (Native (Higher_Order _, _, _)) = true
| is_type_enc_higher_order _ = false
@@ -668,17 +671,22 @@
| _ => raise Same.SAME))
handle Same.SAME => error ("Unknown type encoding: " ^ quote s)
-fun adjust_order THF_Without_Choice (Higher_Order _) =
- Higher_Order THF_Without_Choice
- | adjust_order _ type_enc = type_enc
+fun min_hologic THF_Lambda_Free _ = THF_Lambda_Free
+ | min_hologic _ THF_Lambda_Free = THF_Lambda_Free
+ | min_hologic THF_Without_Choice _ = THF_Without_Choice
+ | min_hologic _ THF_Without_Choice = THF_Without_Choice
+ | min_hologic _ _ = THF_With_Choice
+
+fun adjust_hologic hologic (Higher_Order hologic') = Higher_Order (min_hologic hologic hologic')
+ | adjust_hologic _ type_enc = type_enc
fun no_type_classes Type_Class_Polymorphic = Raw_Polymorphic With_Phantom_Type_Vars
| no_type_classes poly = poly
-fun adjust_type_enc (THF (Polymorphic, choice)) (Native (order, poly, level)) =
- Native (adjust_order choice order, no_type_classes poly, level)
- | adjust_type_enc (THF (Monomorphic, choice)) (Native (order, _, level)) =
- Native (adjust_order choice order, Mangled_Monomorphic, level)
+fun adjust_type_enc (THF (Polymorphic, hologic)) (Native (order, poly, level)) =
+ Native (adjust_hologic hologic order, no_type_classes poly, level)
+ | adjust_type_enc (THF (Monomorphic, hologic)) (Native (order, _, level)) =
+ Native (adjust_hologic hologic order, Mangled_Monomorphic, level)
| adjust_type_enc (TFF Monomorphic) (Native (_, _, level)) =
Native (First_Order, Mangled_Monomorphic, level)
| adjust_type_enc (DFG Polymorphic) (Native (_, poly, level)) =
@@ -881,14 +889,15 @@
fun raw_atp_type_of_typ type_enc =
let
fun term (Type (s, Ts)) =
- AType ((case (is_type_enc_higher_order type_enc, s) of
- (true, @{type_name bool}) => `I tptp_bool_type
- | (true, @{type_name fun}) => `I tptp_fun_type
- | _ =>
- if s = fused_infinite_type_name andalso is_type_enc_native type_enc then
- `I tptp_individual_type
- else
- `make_fixed_type_const s, []), map term Ts)
+ AType
+ ((if s = @{type_name fun} andalso is_type_enc_higher_order type_enc then
+ `I tptp_fun_type
+ else if s = @{type_name bool} andalso is_type_enc_full_higher_order type_enc then
+ `I tptp_bool_type
+ else if s = fused_infinite_type_name andalso is_type_enc_native type_enc then
+ `I tptp_individual_type
+ else
+ `make_fixed_type_const s, []), map term Ts)
| term (TFree (s, _)) = AType ((`make_tfree s, []), [])
| term (TVar z) = AType ((tvar_name z, []), [])
in term end
@@ -927,13 +936,22 @@
if is_type_enc_polymorphic type_enc then to_poly_atype
else to_mangled_atype
fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
+ fun to_ho (ty as AType (((s, _), _), tys)) =
+ if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
+ | to_ho _ = raise Fail "unexpected type"
+ fun to_lfho (ty as AType (((s, _), _), tys)) =
+ if s = tptp_fun_type then to_afun to_ho to_lfho tys
+ else if pred_sym then bool_atype
+ else to_atype ty
+ | to_lfho _ = raise Fail "unexpected type"
fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
| to_fo ary (AType (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
| to_fo _ _ = raise Fail "unexpected type"
- fun to_ho (ty as AType (((s, _), _), tys)) =
- if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
- | to_ho _ = raise Fail "unexpected type"
- in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
+ in
+ if is_type_enc_full_higher_order type_enc then to_ho
+ else if is_type_enc_higher_order type_enc then to_lfho
+ else to_fo ary
+ end
fun native_atp_type_of_typ type_enc pred_sym ary =
native_atp_type_of_raw_atp_type type_enc pred_sym ary o raw_atp_type_of_typ type_enc
@@ -1082,7 +1100,7 @@
| intro top_level args (IConst (name as (s, _), T, T_args)) =
(case proxify_const s of
SOME proxy_base =>
- if top_level orelse is_type_enc_higher_order type_enc then
+ if top_level orelse is_type_enc_full_higher_order type_enc then
(case (top_level, s) of
(_, "c_False") => IConst (`I tptp_false, T, [])
| (_, "c_True") => IConst (`I tptp_true, T, [])
@@ -1238,7 +1256,7 @@
|> transform_elim_prop
|> Object_Logic.atomize_term ctxt
val need_trueprop = (fastype_of t = @{typ bool})
- val is_ho = is_type_enc_higher_order type_enc
+ val is_ho = is_type_enc_full_higher_order type_enc
in
t |> need_trueprop ? HOLogic.mk_Trueprop
|> (if is_ho then unextensionalize_def
@@ -1251,7 +1269,7 @@
(* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "=" for technical
reasons. *)
fun should_use_iff_for_eq CNF _ = false
- | should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format)
+ | should_use_iff_for_eq (THF _) format = not (is_type_enc_full_higher_order format)
| should_use_iff_for_eq _ _ = true
fun make_formula ctxt format type_enc iff_for_eq name stature role t =
@@ -1393,7 +1411,7 @@
|> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [], in_conj = false})) @
([tptp_equal, tptp_old_equal]
|> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [], in_conj = false}))
- |> not (is_type_enc_higher_order type_enc)
+ |> not (is_type_enc_full_higher_order type_enc)
? cons (prefixed_predicator_name,
{pred_sym = true, min_ary = 1, max_ary = 1, types = [], in_conj = false})
@@ -1592,7 +1610,8 @@
if is_pred_sym sym_tab s then tm else predicatify completish tm
| _ => predicatify completish tm)
val do_iterm =
- not (is_type_enc_higher_order type_enc) ? (introduce_app_ops #> introduce_predicators)
+ (not (is_type_enc_higher_order type_enc) ? introduce_app_ops)
+ #> (not (is_type_enc_full_higher_order type_enc) ? introduce_predicators)
#> filter_type_args_in_iterm thy ctrss type_enc
in update_iformula (formula_map do_iterm) end
@@ -2595,7 +2614,7 @@
else
Sufficient_App_Op_And_Predicator
val lam_trans =
- if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then liftingN
+ if lam_trans = keep_lamsN andalso not (is_type_enc_full_higher_order type_enc) then liftingN
else lam_trans
val (classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) =
translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts
--- a/src/HOL/Tools/ATP/atp_proof.ML Tue May 22 11:08:37 2018 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue May 22 17:15:02 2018 +0200
@@ -54,6 +54,7 @@
val e_parN : string
val e_sineN : string
val e_tofofN : string
+ val ehohN : string
val iproverN : string
val iprover_eqN : string
val leo2N : string
@@ -124,6 +125,7 @@
val e_parN = "e_par"
val e_sineN = "e_sine"
val e_tofofN = "e_tofof"
+val ehohN = "ehoh"
val iproverN = "iprover"
val iprover_eqN = "iprover_eq"
val leo2N = "leo2"
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue May 22 11:08:37 2018 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue May 22 17:15:02 2018 +0200
@@ -353,6 +353,32 @@
val e_par = (e_parN, fn () => e_par_config)
+(* Ehoh *)
+
+val ehoh_thf0 = THF (Monomorphic, THF_Lambda_Free)
+
+val ehoh_config : atp_config =
+ {exec = fn _ => (["E_HOME"], ["eprover"]),
+ arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
+ "--auto-schedule --tstp-in --tstp-out --silent --cpu-limit=" ^
+ string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ file_name,
+ proof_delims =
+ [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
+ tstp_proof_delims,
+ known_failures =
+ [(TimedOut, "Failure: Resource limit exceeded (time)"),
+ (TimedOut, "time limit exceeded")] @
+ known_szs_status_failures,
+ prem_role = Conjecture,
+ best_slices =
+ (* FUDGE *)
+ K [(1.0, (((500, ""), ehoh_thf0, "mono_native_higher", liftingN, false), ""))],
+ best_max_mono_iters = default_max_mono_iters,
+ best_max_new_mono_instances = default_max_new_mono_instances}
+
+val ehoh = (ehohN, fn () => ehoh_config)
+
+
(* iProver *)
val iprover_config : atp_config =
@@ -792,10 +818,11 @@
end
val atps =
- [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, leo3, satallax, spass, vampire,
- z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e, remote_e_sine,
- remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_leo3, remote_satallax,
- remote_vampire, remote_snark, remote_pirate, remote_waldmeister, remote_waldmeister_new]
+ [agsyhol, alt_ergo, e, e_males, e_par, ehoh, iprover, iprover_eq, leo2, leo3, satallax, spass,
+ vampire, z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e,
+ remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_leo3,
+ remote_satallax, remote_vampire, remote_snark, remote_pirate, remote_waldmeister,
+ remote_waldmeister_new]
val _ = Theory.setup (fold add_atp atps)