--- 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}
--- 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>\<open>bool\<close> 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>\<open>fun\<close>, [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,
--- 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 *)