--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sat Oct 15 16:34:19 2022 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Oct 17 13:04:00 2022 +0200
@@ -2256,7 +2256,7 @@
(* Each fact is given a unique fact number to avoid name clashes (e.g., because
of monomorphization). The TPTP forbids name clashes, and some of the remote
provers might care. *)
-fun line_of_fact ctxt generate_info prefix encode alt freshen pos mono type_enc rank
+fun line_of_fact ctxt generate_isabelle_info prefix encode alt freshen pos mono type_enc rank
(j, {name, stature = (_, status), role, iformula, atomic_types}) =
Formula ((prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
encode name, alt name),
@@ -2266,22 +2266,22 @@
should_guard_var_in_formula (if pos then SOME true else NONE)
|> close_formula_universally
|> bound_tvars type_enc true atomic_types,
- NONE, isabelle_info generate_info (string_of_status status) (rank j))
+ NONE, isabelle_info generate_isabelle_info (string_of_status status) (rank j))
-fun lines_of_subclass generate_info type_enc sub super =
+fun lines_of_subclass generate_isabelle_info type_enc sub super =
Formula ((subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, ""), Axiom,
AConn (AImplies,
[sub, super] |> map (fn s => class_atom type_enc (s, tvar_a)))
|> bound_tvars type_enc false [tvar_a],
- NONE, isabelle_info generate_info inductiveN helper_rank)
+ NONE, isabelle_info generate_isabelle_info inductiveN helper_rank)
-fun lines_of_subclass_pair generate_info type_enc (sub, supers) =
+fun lines_of_subclass_pair generate_isabelle_info type_enc (sub, supers) =
if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
[Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub, map (`make_class) supers)]
else
- map (lines_of_subclass generate_info type_enc sub) supers
+ map (lines_of_subclass generate_isabelle_info type_enc sub) supers
-fun line_of_tcon_clause generate_info type_enc (name, prems, (cl, T)) =
+fun line_of_tcon_clause generate_isabelle_info type_enc (name, prems, (cl, T)) =
if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
Class_Memb (class_memb_prefix ^ name,
map (fn (cls, T) => (T |> dest_TVar |> tvar_name, map (`make_class) cls)) prems,
@@ -2291,7 +2291,7 @@
mk_ahorn (maps (class_atoms type_enc) prems)
(class_atom type_enc (cl, T))
|> bound_tvars type_enc true (snd (dest_Type T)),
- NONE, isabelle_info generate_info inductiveN helper_rank)
+ NONE, isabelle_info generate_isabelle_info inductiveN helper_rank)
fun line_of_conjecture ctxt mono type_enc ({name, role, iformula, atomic_types, ...} : ifact) =
Formula ((conjecture_prefix ^ name, ""), role,
@@ -2486,7 +2486,7 @@
? fold (add_fact_monotonic_types ctxt mono type_enc) facts
end
-fun line_of_guards_mono_type ctxt generate_info mono type_enc T =
+fun line_of_guards_mono_type ctxt generate_isabelle_info mono type_enc T =
Formula ((guards_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""),
Axiom,
IConst (`make_bound_var "X", T, [])
@@ -2496,21 +2496,21 @@
(SOME true)
|> close_formula_universally
|> bound_tvars type_enc true (atomic_types_of T),
- NONE, isabelle_info generate_info inductiveN helper_rank)
+ NONE, isabelle_info generate_isabelle_info inductiveN helper_rank)
-fun line_of_tags_mono_type ctxt generate_info mono type_enc T =
+fun line_of_tags_mono_type ctxt generate_isabelle_info mono type_enc T =
let val x_var = ATerm ((`make_bound_var "X", []), []) in
Formula ((tags_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""), Axiom,
eq_formula type_enc (atomic_types_of T) [] false
(tag_with_type ctxt mono type_enc NONE T x_var) x_var,
- NONE, isabelle_info generate_info non_rec_defN helper_rank)
+ NONE, isabelle_info generate_isabelle_info non_rec_defN helper_rank)
end
-fun lines_of_mono_types ctxt generate_info mono type_enc =
+fun lines_of_mono_types ctxt generate_isabelle_info mono type_enc =
(case type_enc of
Native _ => K []
- | Guards _ => map (line_of_guards_mono_type ctxt generate_info mono type_enc)
- | Tags _ => map (line_of_tags_mono_type ctxt generate_info mono type_enc))
+ | Guards _ => map (line_of_guards_mono_type ctxt generate_isabelle_info mono type_enc)
+ | Tags _ => map (line_of_tags_mono_type ctxt generate_isabelle_info mono type_enc))
fun decl_line_of_sym ctxt type_enc s (s', T_args, T, pred_sym, ary, _) =
let
@@ -2534,7 +2534,7 @@
fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I)
-fun line_of_guards_sym_decl ctxt generate_info mono type_enc n s j
+fun line_of_guards_sym_decl ctxt generate_isabelle_info mono type_enc n s j
(s', T_args, T, _, ary, in_conj) =
let
val thy = Proof_Context.theory_of ctxt
@@ -2563,10 +2563,10 @@
|> close_formula_universally
|> bound_tvars type_enc (n > 1) (atomic_types_of T)
|> maybe_negate,
- NONE, isabelle_info generate_info inductiveN helper_rank)
+ NONE, isabelle_info generate_isabelle_info inductiveN helper_rank)
end
-fun lines_of_tags_sym_decl ctxt generate_info mono type_enc n s
+fun lines_of_tags_sym_decl ctxt generate_isabelle_info mono type_enc n s
(j, (s', T_args, T, pred_sym, ary, in_conj)) =
let
val thy = Proof_Context.theory_of ctxt
@@ -2583,7 +2583,7 @@
val tag_with = tag_with_type ctxt mono type_enc NONE
fun formula c =
[Formula ((ident, ""), role, eq (tag_with res_T c) c, NONE,
- isabelle_info generate_info non_rec_defN helper_rank)]
+ isabelle_info generate_isabelle_info non_rec_defN helper_rank)]
in
if pred_sym orelse not (should_encode_type ctxt mono level res_T) then
[]
@@ -2608,7 +2608,7 @@
end
| rationalize_decls _ decls = decls
-fun lines_of_sym_decls ctxt generate_info mono type_enc (s, decls) =
+fun lines_of_sym_decls ctxt generate_isabelle_info mono type_enc (s, decls) =
(case type_enc of
Native _ => [decl_line_of_sym ctxt type_enc s (hd decls)]
| Guards (_, level) =>
@@ -2618,7 +2618,7 @@
val n = length decls
val decls = decls |> filter (should_encode_type ctxt mono level o result_type_of_decl)
in
- map_index (uncurry (line_of_guards_sym_decl ctxt generate_info mono type_enc n s)) decls
+ map_index (uncurry (line_of_guards_sym_decl ctxt generate_isabelle_info mono type_enc n s)) decls
end
| Tags (_, level) =>
if is_type_level_uniform level then
@@ -2626,14 +2626,14 @@
else
let val n = length decls in
map_index I decls
- |> maps (lines_of_tags_sym_decl ctxt generate_info mono type_enc n s)
+ |> maps (lines_of_tags_sym_decl ctxt generate_isabelle_info mono type_enc n s)
end)
-fun lines_of_sym_decl_table ctxt generate_info mono type_enc mono_Ts sym_decl_tab =
+fun lines_of_sym_decl_table ctxt generate_isabelle_info mono type_enc mono_Ts sym_decl_tab =
let
val syms = sym_decl_tab |> Symtab.dest |> sort_by fst
- val mono_lines = lines_of_mono_types ctxt generate_info mono type_enc mono_Ts
- val decl_lines = maps (lines_of_sym_decls ctxt generate_info mono type_enc) syms
+ val mono_lines = lines_of_mono_types ctxt generate_isabelle_info mono type_enc mono_Ts
+ val decl_lines = maps (lines_of_sym_decls ctxt generate_isabelle_info mono type_enc) syms
in mono_lines @ decl_lines end
fun datatypes_of_sym_table ctxt ctrss (DFG Polymorphic) (type_enc as Native _) uncurried_aliases
@@ -2680,8 +2680,8 @@
fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
-fun do_uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab base_s0
- types in_conj =
+fun do_uncurried_alias_lines_of_sym ctxt generate_isabelle_info ctrss mono type_enc sym_tab0 sym_tab
+ base_s0 types in_conj =
let
fun do_alias ary =
let
@@ -2717,31 +2717,32 @@
in
([tm1, tm2],
[Formula ((uncurried_alias_eq_prefix ^ s2, ""), role, eq |> maybe_negate, NONE,
- isabelle_info generate_info non_rec_defN helper_rank)])
+ isabelle_info generate_isabelle_info non_rec_defN helper_rank)])
|> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
else pair_append (do_alias (ary - 1)))
end
in do_alias end
-fun uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab
+fun uncurried_alias_lines_of_sym ctxt generate_isabelle_info ctrss mono type_enc sym_tab0 sym_tab
(s, {min_ary, types, in_conj, ...} : sym_info) =
(case unprefix_and_unascii const_prefix s of
SOME mangled_s =>
if String.isSubstring uncurried_alias_sep mangled_s then
let val base_s0 = mangled_s |> unmangled_invert_const in
- do_uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab
- base_s0 types in_conj min_ary
+ do_uncurried_alias_lines_of_sym ctxt generate_isabelle_info ctrss mono type_enc sym_tab0
+ sym_tab base_s0 types in_conj min_ary
end
else
([], [])
| NONE => ([], []))
-fun uncurried_alias_lines_of_sym_table ctxt generate_info ctrss mono type_enc uncurried_aliases
- sym_tab0 sym_tab =
+fun uncurried_alias_lines_of_sym_table ctxt generate_isabelle_info ctrss mono type_enc
+ uncurried_aliases sym_tab0 sym_tab =
([], [])
|> uncurried_aliases
? Symtab.fold_rev (pair_append
- o uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab)
+ o uncurried_alias_lines_of_sym ctxt generate_isabelle_info ctrss mono type_enc sym_tab0
+ sym_tab)
sym_tab
val implicit_declsN = "Could-be-implicit typings"
@@ -2820,7 +2821,7 @@
val app_op_and_predicator_threshold = 45
-fun generate_atp_problem ctxt generate_info format prem_role type_enc mode lam_trans
+fun generate_atp_problem ctxt generate_isabelle_info format prem_role type_enc mode lam_trans
uncurried_aliases readable_names presimp hyp_ts concl_t facts =
let
val thy = Proof_Context.theory_of ctxt
@@ -2857,8 +2858,8 @@
val (ho_stuff, sym_tab) =
sym_table_of_facts ctxt type_enc Min_App_Op conjs facts
val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
- uncurried_alias_lines_of_sym_table ctxt generate_info ctrss mono type_enc uncurried_aliases
- sym_tab0 sym_tab
+ uncurried_alias_lines_of_sym_table ctxt generate_isabelle_info ctrss mono type_enc
+ uncurried_aliases sym_tab0 sym_tab
val (_, sym_tab) =
(ho_stuff, sym_tab)
|> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false)
@@ -2873,7 +2874,7 @@
val sym_decl_lines =
(conjs, helpers @ facts, uncurried_alias_eq_tms)
|> sym_decl_table_of_facts thy type_enc sym_tab
- |> lines_of_sym_decl_table ctxt generate_info mono type_enc mono_Ts
+ |> lines_of_sym_decl_table ctxt generate_isabelle_info mono type_enc mono_Ts
val datatype_decl_lines = map decl_line_of_datatype datatypes
val decl_lines = class_decl_lines @ sym_decl_lines @ datatype_decl_lines
val num_facts = length facts
@@ -2881,14 +2882,14 @@
val pos = mode <> Exporter
val rank_of = rank_of_fact_num num_facts
val fact_lines = facts
- |> map_index (line_of_fact ctxt generate_info fact_prefix ascii_of I freshen pos mono type_enc
- rank_of)
+ |> map_index (line_of_fact ctxt generate_isabelle_info fact_prefix ascii_of I freshen pos mono
+ type_enc rank_of)
- val subclass_lines = maps (lines_of_subclass_pair generate_info type_enc) subclass_pairs
- val tcon_lines = map (line_of_tcon_clause generate_info type_enc) tcon_clauses
+ val subclass_lines = maps (lines_of_subclass_pair generate_isabelle_info type_enc) subclass_pairs
+ val tcon_lines = map (line_of_tcon_clause generate_isabelle_info type_enc) tcon_clauses
val helper_lines = helpers
- |> map_index (line_of_fact ctxt generate_info helper_prefix I (K "") false true mono type_enc
- (K default_rank))
+ |> map_index (line_of_fact ctxt generate_isabelle_info helper_prefix I (K "") false true mono
+ type_enc (K default_rank))
val free_type_lines = lines_of_free_types type_enc (facts @ conjs)
val conj_lines = map (line_of_conjecture ctxt mono type_enc) conjs
(* Reordering these might confuse the proof reconstruction code. *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Sat Oct 15 16:34:19 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Oct 17 13:04:00 2022 +0200
@@ -19,6 +19,7 @@
proof_delims : (string * string) list,
known_failures : (atp_failure * string) list,
prem_role : atp_formula_role,
+ generate_isabelle_info : bool,
good_slices : Proof.context -> (base_slice * atp_slice) list,
good_max_mono_iters : int,
good_max_new_mono_instances : int}
@@ -33,8 +34,8 @@
val spass_H2SOS : string
val isabelle_scala_function: string list * string list
val remote_atp : string -> string -> string list -> (string * string) list ->
- (atp_failure * string) list -> atp_formula_role -> (Proof.context -> base_slice * atp_slice) ->
- string * (unit -> atp_config)
+ (atp_failure * string) list -> atp_formula_role -> bool ->
+ (Proof.context -> base_slice * atp_slice) -> string * (unit -> atp_config)
val add_atp : string * (unit -> atp_config) -> theory -> theory
val get_atp : theory -> string -> (unit -> atp_config)
val is_atp_installed : theory -> string -> bool
@@ -79,6 +80,7 @@
proof_delims : (string * string) list,
known_failures : (atp_failure * string) list,
prem_role : atp_formula_role,
+ generate_isabelle_info : bool,
good_slices : Proof.context -> (base_slice * atp_slice) list,
good_max_mono_iters : int,
good_max_new_mono_instances : int}
@@ -137,6 +139,7 @@
proof_delims = tstp_proof_delims,
known_failures = known_szs_status_failures,
prem_role = Hypothesis,
+ generate_isabelle_info = false,
good_slices =
(* FUDGE *)
K [((2, 60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))],
@@ -159,6 +162,7 @@
(TimedOut, ": Timeout"),
(GaveUp, ": Unknown")],
prem_role = Hypothesis,
+ generate_isabelle_info = false,
good_slices =
(* FUDGE *)
K [((1000 (* infinity *), 100, meshN), (TF1, "poly_native", liftingN, false, ""))],
@@ -184,6 +188,7 @@
(TimedOut, "time limit exceeded")] @
known_szs_status_failures,
prem_role = Conjecture,
+ generate_isabelle_info = false,
good_slices =
let
val (format, type_enc, lam_trans, extra_options) =
@@ -221,6 +226,7 @@
[(ProofIncomplete, "% SZS output start CNFRefutation")] @
known_szs_status_failures,
prem_role = Hypothesis,
+ generate_isabelle_info = false,
good_slices =
(* FUDGE *)
K [((2, 32, meshN), (TF0, "mono_native", liftingN, false, "")),
@@ -250,6 +256,7 @@
(GaveUp, "No.of.Axioms")] @
known_szs_status_failures,
prem_role = Hypothesis,
+ generate_isabelle_info = false,
good_slices =
(* FUDGE *)
K [((2, 40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))],
@@ -271,6 +278,7 @@
proof_delims = tstp_proof_delims,
known_failures = known_szs_status_failures,
prem_role = Hypothesis,
+ generate_isabelle_info = false,
good_slices =
(* FUDGE *)
K [((6, 512, meshN), (TH0, "mono_native_higher", keep_lamsN, false, "")),
@@ -295,6 +303,7 @@
[("% SZS output start Proof", "% SZS output end Proof")],
known_failures = known_szs_status_failures,
prem_role = Hypothesis,
+ generate_isabelle_info = false,
good_slices =
(* FUDGE *)
K [((12, 256, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))],
@@ -314,37 +323,34 @@
val spass_H2SOS = "-Heuristic=2 -SOS"
val spass_config : atp_config =
- let
- val format = DFG Monomorphic
- in
- {exec = (["SPASS_HOME"], ["SPASS"]),
- arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn problem =>
- ["-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^
- "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem
- |> extra_options <> "" ? prefix (extra_options ^ " ")],
- proof_delims = [("Here is a proof", "Formulae used in the proof")],
- known_failures =
- [(GaveUp, "SPASS beiseite: Completion found"),
- (TimedOut, "SPASS beiseite: Ran out of time"),
- (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
- (MalformedInput, "Undefined symbol"),
- (MalformedInput, "Free Variable"),
- (Unprovable, "No formulae and clauses found in input file"),
- (InternalError, "Please report this error")],
- prem_role = Conjecture,
- good_slices =
- (* FUDGE *)
- K [((2, 150, meshN), (format, "mono_native", combsN, true, "")),
- ((2, 500, meshN), (format, "mono_native", liftingN, true, spass_H2SOS)),
- ((2, 50, meshN), (format, "mono_native", liftingN, true, spass_H2LR0LT0)),
- ((2, 250, meshN), (format, "mono_native", combsN, true, spass_H2NuVS0)),
- ((2, 1000, mepoN), (format, "mono_native", liftingN, true, spass_H1SOS)),
- ((2, 150, meshN), (format, "poly_guards??", liftingN, false, spass_H2NuVS0Red2)),
- ((2, 300, meshN), (format, "mono_native", combsN, true, spass_H2SOS)),
- ((2, 100, meshN), (format, "mono_native", combs_and_liftingN, true, spass_H2))],
- good_max_mono_iters = default_max_mono_iters,
- good_max_new_mono_instances = default_max_new_mono_instances}
- end
+ {exec = (["SPASS_HOME"], ["SPASS"]),
+ arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn problem =>
+ ["-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^
+ "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem
+ |> extra_options <> "" ? prefix (extra_options ^ " ")],
+ proof_delims = [("Here is a proof", "Formulae used in the proof")],
+ known_failures =
+ [(GaveUp, "SPASS beiseite: Completion found"),
+ (TimedOut, "SPASS beiseite: Ran out of time"),
+ (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
+ (MalformedInput, "Undefined symbol"),
+ (MalformedInput, "Free Variable"),
+ (Unprovable, "No formulae and clauses found in input file"),
+ (InternalError, "Please report this error")],
+ prem_role = Conjecture,
+ generate_isabelle_info = true,
+ good_slices =
+ (* FUDGE *)
+ K [((2, 150, meshN), (DFG Monomorphic, "mono_native", combsN, true, "")),
+ ((2, 500, meshN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H2SOS)),
+ ((2, 50, meshN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H2LR0LT0)),
+ ((2, 250, meshN), (DFG Monomorphic, "mono_native", combsN, true, spass_H2NuVS0)),
+ ((2, 1000, mepoN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H1SOS)),
+ ((2, 150, meshN), (DFG Monomorphic, "poly_guards??", liftingN, false, spass_H2NuVS0Red2)),
+ ((2, 300, meshN), (DFG Monomorphic, "mono_native", combsN, true, spass_H2SOS)),
+ ((2, 100, meshN), (DFG Monomorphic, "mono_native", combs_and_liftingN, true, spass_H2))],
+ good_max_mono_iters = default_max_mono_iters,
+ good_max_new_mono_instances = default_max_new_mono_instances}
val spass = (spassN, fn () => spass_config)
@@ -378,6 +384,7 @@
(Interrupted, "Aborted by signal SIGINT")] @
known_szs_status_failures,
prem_role = Hypothesis,
+ generate_isabelle_info = false,
good_slices =
(* FUDGE *)
K [((2, 512, meshN), (TX1, "mono_native_fool", combsN, false, sosN)),
@@ -410,6 +417,7 @@
[(TimedOut, "SZS status ResourceOut")] @ (* odd way of timing out *)
known_szs_status_failures,
prem_role = Hypothesis,
+ generate_isabelle_info = true,
good_slices =
K [((1, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=1 --ho-unif-max-depth=1 --ho-max-elims=0 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --boolean-reasoning=bool-hoist --bool-hoist-simpl=true --bool-select=LI --recognize-injectivity=true --ext-rules=ext-family --ext-rules-max-depth=1 --ho-choice-inst=true --ho-prim-enum=none --ho-elim-leibniz=0 --interpret-bool-funs=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --ho-unif-level=pragmatic-framework --select=bb+e-selection2 --post-cnf-lambda-lifting=true -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" -q \"6|prefer-processed|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|fifo\" -q \"4|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-struct(1,5,2,3)\" --avatar=off --recognize-injectivity=true --ho-neg-ext=true --e-timeout=2 --ho-pattern-decider=true --ho-fixpoint-decider=true --e-max-derived=50 --ignore-orphans=true --e-auto=true --presaturate=true --e-call-point=0.1")), (* sh5_sh1.sh *)
((1, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=2 --ho-unif-max-depth=1 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection16 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true --ho-unif-level=pragmatic-framework --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=lambda-def-invfreqrank --e-call-point=0.1")), (* sh8_shallow_sine.sh *)
@@ -472,7 +480,8 @@
val isabelle_scala_function = (["SCALA_HOME"], ["bin/scala"])
-fun remote_config system_name system_versions proof_delims known_failures prem_role good_slice =
+fun remote_config system_name system_versions proof_delims known_failures prem_role
+ generate_isabelle_info good_slice =
{exec = isabelle_scala_function,
arguments = fn _ => fn _ => fn command => fn timeout => fn problem =>
[the_remote_system system_name system_versions,
@@ -481,17 +490,21 @@
proof_delims = union (op =) tstp_proof_delims proof_delims,
known_failures = known_failures @ known_says_failures,
prem_role = prem_role,
+ generate_isabelle_info = generate_isabelle_info,
good_slices = fn ctxt => [good_slice ctxt],
good_max_mono_iters = default_max_mono_iters,
good_max_new_mono_instances = default_max_new_mono_instances} : atp_config
fun remotify_config system_name system_versions good_slice
- ({proof_delims, known_failures, prem_role, ...} : atp_config) =
- remote_config system_name system_versions proof_delims known_failures prem_role good_slice
+ ({proof_delims, known_failures, prem_role, generate_isabelle_info, ...} : atp_config) =
+ remote_config system_name system_versions proof_delims known_failures prem_role
+ generate_isabelle_info good_slice
-fun remote_atp name system_name system_versions proof_delims known_failures prem_role good_slice =
+fun remote_atp name system_name system_versions proof_delims known_failures prem_role
+ generate_isabelle_info good_slice =
(remote_prefix ^ name, fn () =>
- remote_config system_name system_versions proof_delims known_failures prem_role good_slice)
+ remote_config system_name system_versions proof_delims known_failures prem_role
+ generate_isabelle_info good_slice)
fun remotify_atp (name, config) system_name system_versions good_slice =
(remote_prefix ^ name, remotify_config system_name system_versions good_slice o config)
@@ -501,7 +514,7 @@
(Inappropriate, "**** Unexpected end of file."),
(Crashed, "Unrecoverable Segmentation Fault")]
@ known_szs_status_failures)
- Hypothesis
+ Hypothesis false
(K ((1000 (* infinity *), 50, meshN), (CNF_UEQ, type_enc, combsN, false, "")) (* FUDGE *))
val remote_agsyhol =
@@ -536,6 +549,7 @@
proof_delims = [],
known_failures = known_szs_status_failures,
prem_role = prem_role,
+ generate_isabelle_info = false,
good_slices =
K [((2, 256, "mepo"), (format, type_enc,
if is_format_higher_order format then keep_lamsN else combsN, uncurried_aliases, ""))],