# HG changeset patch # User blanchet # Date 1314713254 -7200 # Node ID 0a1dfc6365e98908f9cb7a3b0f7a0862607216ed # Parent e74aa9d9162be071cb3a1bfc52e288dfad6a5e01 first step towards polymorphic TFF + changed defaults for Vampire diff -r e74aa9d9162b -r 0a1dfc6365e9 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 30 16:04:23 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 30 16:07:34 2011 +0200 @@ -19,14 +19,15 @@ datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type - datatype tff_flavor = Implicit | Explicit - datatype thf_flavor = Without_Choice | With_Choice + datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic + datatype tff_explicitness = TFF_Implicit | TFF_Explicit + datatype thf_flavor = THF_Without_Choice | THF_With_Choice datatype format = CNF | CNF_UEQ | FOF | - TFF of tff_flavor | - THF of thf_flavor + TFF of tff_polymorphism * tff_explicitness | + THF0 of thf_flavor datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = @@ -119,15 +120,16 @@ datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type -datatype tff_flavor = Implicit | Explicit -datatype thf_flavor = Without_Choice | With_Choice +datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic +datatype tff_explicitness = TFF_Implicit | TFF_Explicit +datatype thf_flavor = THF_Without_Choice | THF_With_Choice datatype format = CNF | CNF_UEQ | FOF | - TFF of tff_flavor | - THF of thf_flavor + TFF of tff_polymorphism * tff_explicitness | + THF0 of thf_flavor datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = @@ -211,10 +213,10 @@ | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis) | formula_map f (AAtom tm) = AAtom (f tm) -fun is_format_thf (THF _) = true +fun is_format_thf (THF0 _) = true | is_format_thf _ = false fun is_format_typed (TFF _) = true - | is_format_typed (THF _) = true + | is_format_typed (THF0 _) = true | is_format_typed _ = false fun string_for_kind Axiom = "axiom" @@ -228,7 +230,7 @@ raise Fail "unexpected higher-order type in first-order format" | strip_tff_type (AType s) = ([], s) -fun string_for_type (THF _) ty = +fun string_for_type (THF0 _) ty = let fun aux _ (AType s) = s | aux rhs (AFun (ty1, ty2)) = @@ -270,7 +272,7 @@ |> is_format_thf format ? enclose "(" ")" else (case (s = tptp_ho_forall orelse s = tptp_ho_exists, - s = tptp_choice andalso format = THF With_Choice, ts) of + s = tptp_choice andalso format = THF0 THF_With_Choice, ts) of (true, _, [AAbs ((s', ty), tm)]) => (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever possible, to work around LEO-II 1.2.8 parser limitation. *) @@ -291,7 +293,7 @@ else s ^ "(" ^ commas ss ^ ")" end) - | string_for_term (format as THF _) (AAbs ((s, ty), tm)) = + | string_for_term (format as THF0 _) (AAbs ((s, ty), tm)) = "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "] : " ^ string_for_term format tm ^ ")" | string_for_term _ _ = raise Fail "unexpected term in first-order format" @@ -324,7 +326,7 @@ | string_for_format CNF_UEQ = tptp_cnf | string_for_format FOF = tptp_fof | string_for_format (TFF _) = tptp_tff - | string_for_format (THF _) = tptp_thf + | string_for_format (THF0 _) = tptp_thf fun string_for_problem_line format (Decl (ident, sym, ty)) = string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^ diff -r e74aa9d9162b -r 0a1dfc6365e9 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 30 16:04:23 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 30 16:07:34 2011 +0200 @@ -241,8 +241,8 @@ prem_kind = Hypothesis, best_slices = fn ctxt => (* FUDGE *) - [(0.667, (false, (150, THF Without_Choice, "simple_higher", sosN))), - (0.333, (true, (50, THF Without_Choice, "simple_higher", no_sosN)))] + [(0.667, (false, (150, THF0 THF_Without_Choice, "simple_higher", sosN))), + (0.333, (true, (50, THF0 THF_Without_Choice, "simple_higher", no_sosN)))] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -262,7 +262,8 @@ conj_sym_kind = Axiom, prem_kind = Hypothesis, best_slices = - K [(1.0, (true, (100, THF With_Choice, "simple_higher", "")))] (* FUDGE *)} + K [(1.0, (true, (100, THF0 THF_With_Choice, "simple_higher", "")))] + (* FUDGE *)} val satallax = (satallaxN, satallax_config) @@ -309,6 +310,8 @@ fun is_old_vampire_version () = string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER +val vampire_tff = TFF (TFF_Monomorphic, TFF_Implicit) + val vampire_config : atp_config = {exec = ("VAMPIRE_HOME", "vampire"), required_execs = [], @@ -340,9 +343,9 @@ (0.333, (false, (500, FOF, "mono_tags?", sosN))), (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))] else - [(0.333, (false, (150, TFF Implicit, "poly_guards", sosN))), - (0.333, (false, (500, TFF Implicit, "simple", sosN))), - (0.334, (true, (50, TFF Implicit, "simple", no_sosN)))]) + [(0.333, (false, (150, vampire_tff, "poly_guards", sosN))), + (0.333, (false, (500, vampire_tff, "simple", sosN))), + (0.334, (true, (50, vampire_tff, "simple", no_sosN)))]) |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -351,6 +354,8 @@ (* Z3 with TPTP syntax *) +val z3_tff = TFF (TFF_Monomorphic, TFF_Implicit) + val z3_tptp_config : atp_config = {exec = ("Z3_HOME", "z3"), required_execs = [], @@ -368,10 +373,10 @@ prem_kind = Hypothesis, best_slices = (* FUDGE *) - K [(0.5, (false, (250, FOF, "mono_guards?", ""))), - (0.25, (false, (125, FOF, "mono_guards?", ""))), - (0.125, (false, (62, TFF Implicit, "simple", ""))), - (0.125, (false, (31, TFF Implicit, "simple", "")))]} + K [(0.5, (false, (250, z3_tff, "simple", ""))), + (0.25, (false, (125, z3_tff, "simple", ""))), + (0.125, (false, (62, z3_tff, "simple", ""))), + (0.125, (false, (31, z3_tff, "simple", "")))]} val z3_tptp = (z3_tptpN, z3_tptp_config) @@ -381,7 +386,8 @@ val systems = Synchronized.var "atp_systems" ([] : string list) fun get_systems () = - case Isabelle_System.bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of + case Isabelle_System.bash_output + "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of (output, 0) => split_lines output | (output, _) => error (case extract_known_failure known_perl_failures output of @@ -449,31 +455,32 @@ (remote_prefix ^ name, remotify_config system_name system_versions best_slice config) +val dumb_tff = TFF (TFF_Monomorphic, TFF_Explicit) + val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"] (K (750, FOF, "mono_tags?") (* FUDGE *)) val remote_leo2 = remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"] - (K (100, THF Without_Choice, "simple_higher") (* FUDGE *)) + (K (100, THF0 THF_Without_Choice, "simple_higher") (* FUDGE *)) val remote_satallax = remotify_atp satallax "Satallax" ["2.1", "2.0", "2"] - (K (100, THF With_Choice, "simple_higher") (* FUDGE *)) + (K (100, THF0 THF_With_Choice, "simple_higher") (* FUDGE *)) val remote_vampire = remotify_atp vampire "Vampire" ["1.8"] - (K (250, TFF Implicit, "simple") (* FUDGE *)) + (K (250, FOF, "mono_guards?") (* FUDGE *)) val remote_z3_tptp = - remotify_atp z3_tptp "Z3" ["3.0"] - (K (250, TFF Implicit, "simple") (* FUDGE *)) + remotify_atp z3_tptp "Z3" ["3.0"] (K (250, z3_tff, "simple") (* FUDGE *)) val remote_e_sine = remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *)) val remote_snark = remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"] [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis - (K (100, TFF Explicit, "simple") (* FUDGE *)) + (K (100, dumb_tff, "simple") (* FUDGE *)) val remote_e_tofof = - remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) - Axiom Hypothesis (K (150, TFF Explicit, "simple") (* FUDGE *)) + remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom + Hypothesis (K (150, dumb_tff, "simple") (* FUDGE *)) val remote_waldmeister = remote_atp waldmeisterN "Waldmeister" ["710"] [("#START OF PROOF", "Proved Goals:")] diff -r e74aa9d9162b -r 0a1dfc6365e9 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 30 16:04:23 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 30 16:07:34 2011 +0200 @@ -320,7 +320,7 @@ fun default c = const_prefix ^ lookup_const c in fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal - | make_fixed_const (SOME (THF With_Choice)) c = + | make_fixed_const (SOME (THF0 THF_With_Choice)) c = if c = choice_const then tptp_choice else default c | make_fixed_const _ c = default c end @@ -625,7 +625,7 @@ | is_type_level_monotonicity_based Fin_Nonmono_Types = true | is_type_level_monotonicity_based _ = false -fun adjust_type_enc (THF _) type_enc = type_enc +fun adjust_type_enc (THF0 _) type_enc = type_enc | adjust_type_enc (TFF _) (Simple_Types (_, level)) = Simple_Types (First_Order, level) | adjust_type_enc format (Simple_Types (_, level)) = @@ -889,16 +889,17 @@ if is_tptp_equal s andalso length args = 2 then IConst (`I tptp_equal, T, []) else - (* Use a proxy even for partially applied THF equality, because - the LEO-II and Satallax parsers complain about not being - able to infer the type of "=". *) + (* Use a proxy even for partially applied THF0 equality, + because the LEO-II and Satallax parsers complain about not + being able to infer the type of "=". *) IConst (proxy_base |>> prefix const_prefix, T, T_args) | _ => IConst (name, T, []) else IConst (proxy_base |>> prefix const_prefix, T, T_args) | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args - else IConst (name, T, T_args)) + else + IConst (name, T, T_args)) | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm) | intro _ _ tm = tm in intro true [] end @@ -2177,12 +2178,10 @@ |> (case format of CNF => ensure_cnf_problem | CNF_UEQ => filter_cnf_ueq_problem - | _ => I) - |> (if is_format_typed format andalso format <> TFF Implicit then - declare_undeclared_syms_in_atp_problem type_decl_prefix - implicit_declsN - else - I) + | FOF => I + | TFF (_, TFF_Implicit) => I + | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix + implicit_declsN) val (problem, pool) = problem |> nice_atp_problem readable_names val helpers_offset = offset_of_heading_in_problem helpersN problem 0 val typed_helpers =