# HG changeset patch # User blanchet # Date 1708949437 -3600 # Node ID 4031aafc2ddac08a6de2d12ffb3f8f0701097bd4 # Parent bf377e10ff3b7b0081470512b0d97dd85a10ef3b deal with new-style Vampire skolemization in reconstructed Isar proofs diff -r bf377e10ff3b -r 4031aafc2dda src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Feb 25 20:40:21 2024 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Feb 26 13:10:37 2024 +0100 @@ -239,8 +239,14 @@ fun slack_fastype_of t = fastype_of t handle TERM _ => Type_Infer.anyT \<^sort>\type\ -val spass_skolem_prefix = "sk" (* "skc" or "skf" *) -val vampire_skolem_prefix = "sK" +val spass_skolem_prefixes = ["skc", "skf"] +val zipperposition_skolem_prefix = "sk_" + +fun is_spass_skolem s = + exists (fn pre => String.isPrefix pre s) spass_skolem_prefixes + +fun is_reverse_skolem s = + exists (fn pre => String.isPrefix pre s) (zipperposition_skolem_prefix :: spass_skolem_prefixes) val zip_internal_ite_prefix = "zip_internal_ite_" @@ -299,20 +305,34 @@ val opt_T' = SOME (map slack_fastype_of args ---> the_default dummyT opt_T) val func = do_term opt_T' (ATerm ((s, tys), [])) in foldl1 (op $) (func :: args) end - else if s = tptp_or then HOLogic.disj - else if s = tptp_and then HOLogic.conj - else if s = tptp_implies then HOLogic.imp - else if s = tptp_iff orelse s = tptp_equal then HOLogic.eq_const dummyT - else if s = tptp_not_iff orelse s = tptp_not_equal then \<^term>\\x y. x \ y\ - else if s = tptp_if then \<^term>\\P Q. Q \ P\ - else if s = tptp_not_and then \<^term>\\P Q. \ (P \ Q)\ - else if s = tptp_not_or then \<^term>\\P Q. \ (P \ Q)\ - else if s = tptp_not then HOLogic.Not - else if s = tptp_ho_forall then HOLogic.all_const dummyT - else if s = tptp_ho_exists then HOLogic.exists_const dummyT - else if s = tptp_hilbert_choice then HOLogic.choice_const dummyT - else if s = tptp_hilbert_the then \<^term>\The\ - else if String.isPrefix zip_internal_ite_prefix s then If_const dummyT + else if s = tptp_or then + HOLogic.disj + else if s = tptp_and then + HOLogic.conj + else if s = tptp_implies then + HOLogic.imp + else if s = tptp_iff orelse s = tptp_equal then + HOLogic.eq_const dummyT + else if s = tptp_not_iff orelse s = tptp_not_equal then + \<^term>\\x y. x \ y\ + else if s = tptp_if then + \<^term>\\P Q. Q \ P\ + else if s = tptp_not_and then + \<^term>\\P Q. \ (P \ Q)\ + else if s = tptp_not_or then + \<^term>\\P Q. \ (P \ Q)\ + else if s = tptp_not then + HOLogic.Not + else if s = tptp_ho_forall then + HOLogic.all_const dummyT + else if s = tptp_ho_exists then + HOLogic.exists_const dummyT + else if s = tptp_hilbert_choice then + HOLogic.choice_const dummyT + else if s = tptp_hilbert_the then + \<^term>\The\ + else if String.isPrefix zip_internal_ite_prefix s then + If_const dummyT else (case unprefix_and_unascii const_prefix s of SOME s' => @@ -420,12 +440,7 @@ end | NONE => (* a free or schematic variable *) let - val term_ts = - map (do_term [] NONE) us - (* SPASS (3.8ds) and Vampire (2.6) pass arguments to Skolem functions in reverse - order, which is incompatible with "metis"'s new skolemizer. *) - |> exists (fn pre => String.isPrefix pre s) - [spass_skolem_prefix, vampire_skolem_prefix] ? rev + val term_ts = map (do_term [] NONE) us |> is_reverse_skolem s ? rev val ts = term_ts @ extra_ts val T = (case tys of @@ -708,10 +723,8 @@ | add_skolem_args t = (case strip_comb t of (Free (s, _), args as _ :: _) => - if String.isPrefix spass_skolem_prefix s then - insert (op =) (s, take_prefix is_Var args) - else - fold add_skolem_args args + if is_spass_skolem s then insert (op =) (s, take_prefix is_Var args) + else fold add_skolem_args args | (u, args as _ :: _) => fold add_skolem_args (u :: args) | _ => I) @@ -725,7 +738,7 @@ fun introduce_spass_skolems proof = let - fun add_skolem (Free (s, _)) = String.isPrefix spass_skolem_prefix s ? insert (op =) s + fun add_skolem (Free (s, _)) = is_spass_skolem s ? insert (op =) s | add_skolem _ = I (* union-find would be faster *) @@ -740,7 +753,7 @@ rise to several clauses are skolemized together. *) val skoXss = map (fn ((_, ss), _, t, _, _) => Term.fold_aterms add_skolem t ss) input_steps val groups0 = Graph.strong_conn (fold add_cycle skoXss Graph.empty) - val groups = filter (exists (String.isPrefix spass_skolem_prefix)) groups0 + val groups = filter (exists is_spass_skolem) groups0 val skoXss_input_steps = skoXss ~~ input_steps @@ -759,8 +772,7 @@ |> map (HOLogic.dest_Trueprop #> rename_skolem_args) |> Library.foldr1 s_conj |> HOLogic.mk_Trueprop) - val skos = - fold (union (op =) o filter (String.isPrefix spass_skolem_prefix) o fst) skoXss_steps [] + val skos = fold (union (op =) o filter is_spass_skolem o fst) skoXss_steps [] val deps = map (snd #> #1) skoXss_steps in [(name0, Unknown, unskolemize_spass_term skos t, spass_pre_skolemize_rule, deps), diff -r bf377e10ff3b -r 4031aafc2dda src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Feb 25 20:40:21 2024 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 26 13:10:37 2024 +0100 @@ -52,6 +52,7 @@ val e_skolemize_rule = "skolemize" val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg" val satallax_skolemize_rule = "tab_ex" +val vampire_choice_axiom_rule = "choice_axiom" val vampire_skolemisation_rule = "skolemisation" val veriT_la_generic_rule = "la_generic" val veriT_simp_arith_rule = "simp_arith" @@ -62,7 +63,7 @@ val symbol_introduction_rules = [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, - spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule, + spass_skolemize_rule, vampire_choice_axiom_rule, vampire_skolemisation_rule, z3_skolemize_rule, zipperposition_cnf_rule, zipperposition_define_rule] @ veriT_skolemize_rules fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule)