# HG changeset patch # User blanchet # Date 1597917166 -7200 # Node ID 585b877df6986b30950e31c0654bd8e74fd44cbd # Parent 618a0ab13868cec46937cb499c252fc291481ef0 basic integration of Zipperposition 2.0 diff -r 618a0ab13868 -r 585b877df698 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Thu Aug 20 11:52:45 2020 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Thu Aug 20 11:52:46 2020 +0200 @@ -836,10 +836,12 @@ to the directory that contains the \texttt{z3\_tptp} executable. \item[\labelitemi] \textbf{\textit{zipperposition}:} Zipperposition -\cite{cruanes-2014} is a first-order resolution prover developed by Simon +\cite{cruanes-2014} is a higher-order superposition prover developed by Simon Cruanes and colleagues. To use Zipperposition, set the environment variable \texttt{ZIPPERPOSITION\_HOME} to the directory that contains the -\texttt{zipperposition} executable. +\texttt{zipperposition} executable and \texttt{ZIPPERPOSITION\_VERSION} to the +version number (e.g., ``2.0.1''). Sledgehammer has been tested with version +2.0.1. \end{enum} \end{sloppy} diff -r 618a0ab13868 -r 585b877df698 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Aug 20 11:52:45 2020 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Aug 20 11:52:46 2020 +0200 @@ -883,9 +883,6 @@ end) end -val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *) -val fused_infinite_type = Type (fused_infinite_type_name, []) - fun raw_atp_type_of_typ type_enc = let fun term (Type (s, Ts)) = @@ -894,8 +891,6 @@ `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, []), []) @@ -1389,15 +1384,6 @@ end | should_tag_with_type _ _ _ _ _ _ = false -fun fused_type ctxt mono level = - let - val should_encode = should_encode_type ctxt mono level - fun fuse 0 T = if should_encode T then T else fused_infinite_type - | fuse ary (Type (\<^type_name>\fun\, [T1, T2])) = - fuse 0 T1 --> fuse (ary - 1) T2 - | fuse _ _ = raise Fail "expected function type" - in fuse end - (** predicators and application operators **) type sym_info = @@ -1946,10 +1932,9 @@ ATerm ((name, ty_args), tm_args @ args) end -fun do_bound_type ctxt mono type_enc = +fun do_bound_type type_enc = (case type_enc of - Native (_, _, level) => - fused_type ctxt mono level 0 #> native_atp_type_of_typ type_enc false 0 #> SOME + Native _ => native_atp_type_of_typ type_enc false 0 #> SOME | _ => K NONE) fun tag_with_type ctxt mono type_enc pos T tm = @@ -2011,10 +1996,9 @@ let val phi = phi |> do_formula pos val universal = Option.map (q = AExists ? not) pos - val do_bound_type = do_bound_type ctxt mono type_enc in AQuant (q, xs |> map (apsnd (fn NONE => NONE - | SOME T => do_bound_type T)), + | SOME T => do_bound_type type_enc T)), (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd)) (map_filter (fn (_, NONE) => NONE @@ -2286,7 +2270,7 @@ | 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)) -fun decl_line_of_sym ctxt mono type_enc s (s', T_args, T, pred_sym, ary, _) = +fun decl_line_of_sym ctxt type_enc s (s', T_args, T, pred_sym, ary, _) = let val thy = Proof_Context.theory_of ctxt val (T, T_args) = @@ -2302,10 +2286,8 @@ | NONE => raise Fail "unexpected type arguments") in Sym_Decl (sym_decl_prefix ^ s, (s, s'), - T |> fused_type ctxt mono (level_of_type_enc type_enc) ary - |> native_atp_type_of_typ type_enc pred_sym ary - |> not (null T_args) - ? curry APi (map (tvar_name o dest_TVar) T_args)) + T |> native_atp_type_of_typ type_enc pred_sym ary + |> not (null T_args) ? curry APi (map (tvar_name o dest_TVar) T_args)) end fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I) @@ -2387,7 +2369,7 @@ fun lines_of_sym_decls ctxt generate_info mono type_enc (s, decls) = (case type_enc of - Native _ => [decl_line_of_sym ctxt mono type_enc s (hd decls)] + Native _ => [decl_line_of_sym ctxt type_enc s (hd decls)] | Guards (_, level) => let val thy = Proof_Context.theory_of ctxt @@ -2489,10 +2471,9 @@ val tm2 = list_app (do_const name2) (first_bounds @ [last_bound]) |> filter_ty_args - val do_bound_type = do_bound_type ctxt mono type_enc val eq = - eq_formula type_enc (atomic_types_of T) (map (apsnd do_bound_type) bounds) false - (atp_term_of tm1) (atp_term_of tm2) + eq_formula type_enc (atomic_types_of T) + (map (apsnd (do_bound_type type_enc)) bounds) false (atp_term_of tm1) (atp_term_of tm2) in ([tm1, tm2], [Formula ((uncurried_alias_eq_prefix ^ s2, ""), role, eq |> maybe_negate, NONE, diff -r 618a0ab13868 -r 585b877df698 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Thu Aug 20 11:52:45 2020 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Aug 20 11:52:46 2020 +0200 @@ -558,17 +558,23 @@ (* Zipperposition *) +val zipperposition_blsimp = "--mode ho-pragmatic --max-inferences 3 --ho-max-app-projections 0 --ho-max-elims 0 --ho-max-rigid-imitations 2 --ho-max-identifications 0 --ho-unif-max-depth 2 --boolean-reasoning no-cases --ext-rules ext-family --ext-rules-max-depth 1 --kbo-weight-fun invdocc --ho-prim-enum tf --ho-prim-enum-early-bird true --tptp-def-as-rewrite --ho-unif-level pragmatic-framework -q '1|const|conjecture-relative-var(1,s,f)' -q '1|prefer-processed|pnrefined(1,1,1,2,2,2,0.5)' -q '1|prefer-sos|staggered(1)' -q '2|prefer-fo|default' -q '1|prefer-neg-unit|orient-lmax(2,1,2,1,1)' -q '2|prefer-easy-ho|conjecture-relative-struct(1.5,3.5,2,3)' --ho-elim-leibniz 2 --ho-fixpoint-decider true --ho-pattern-decider false --ho-solid-decider true --ho-max-solidification 12 --select e-selection11 --solve-formulas true --sup-at-vars false --sup-at-var-headed false --lazy-cnf true --lazy-cnf-kind simp --lazy-cnf-renaming-threshold 4 --sine 50 --sine-tolerance 1.7 --sine-depth-max 3 --sine-depth-min 1 --sine-trim-implications true --ho-selection-restriction none --sup-from-var-headed false --sine-trim-implications true" +val zipperposition_s6 = "--tptp-def-as-rewrite --rewrite-before-cnf true --mode ho-competitive --boolean-reasoning no-cases --ext-rules off --ho-prim-enum none --recognize-injectivity true --ho-elim-leibniz off --ho-unif-level full-framework --no-max-vars -q '3|const|conjecture-relative-var(1.02,l,f)' -q '1|prefer-ho-steps|conjecture-relative-var(1,s,f)' -q '1|prefer-processed|fifo' -q '3|by-app-var-num|pnrefined(2,1,1,1,2,2,2)' --select ho-selection5 --prec-gen-fun unary_first --solid-subsumption false --ignore-orphans false --ho-solid-decider true --ho-fixpoint-decider true --ho-pattern-decider true --sup-at-vars false --sup-at-var-headed false --sup-from-var-headed false --ho-neg-ext-simpl true" +val zipperposition_cdots = "--mode ho-competitive --boolean-reasoning cases-simpl --ext-rules ext-family --ext-rules-max-depth 1 --ho-prim-enum pragmatic --ho-prim-max 1 --bool-subterm-selection A --avatar off --recognize-injectivity true --ho-elim-leibniz 1 --ho-unif-level full-framework --no-max-vars -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-selection7 --ho-choice-inst true --sine 50 --sine-tolerance 2 --sine-depth-max 4 --sine-depth-min 1 --scan-clause-ac true --lambdasup 0 --kbo-weight-fun invfreqrank" + val zipperposition_config : atp_config = {exec = K (["ZIPPERPOSITION_HOME"], ["zipperposition"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => - "-print none -proof tstp -print-types -timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ - file_name, + arguments = fn _ => fn _ => fn extra_options => fn timeout => fn file_name => fn _ => + "--input tptp --output tptp --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name + |> extra_options <> "" ? prefix (extra_options ^ " "), proof_delims = tstp_proof_delims, known_failures = known_szs_status_failures, - prem_role = Hypothesis, + prem_role = Conjecture, best_slices = fn _ => (* FUDGE *) - [(1.0, (((250, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], + [(0.333, (((128, "meshN"), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)), + (0.333, (((32, "meshN"), THF (Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), zipperposition_s6)), + (0.334, (((512, "meshN"), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_cdots))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} @@ -629,7 +635,7 @@ error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n(Available systems: " ^ commas_quote syss ^ ".)"))) -val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *) +val max_remote_secs = 1000 (* give Geoff Sutcliffe's servers a break *) fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice = {exec = K (["ISABELLE_ATP"], ["scripts/remote_atp"]), @@ -691,8 +697,8 @@ (K (((400, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), remote_vampire_command) (* FUDGE *)) val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??" val remote_zipperposition = - remotify_atp zipperposition "Zipperpin" ["1.5"] - (K (((250, ""), THF (Monomorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *)) + remotify_atp zipperposition "Zipperpin" ["2.0"] + (K (((512, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) (* Setup *)