# HG changeset patch # User blanchet # Date 1315325616 -7200 # Node ID 265174356212176778ef9b353fe4c57c779cd414 # Parent 3c73f40689782e81fe9b694dccc0c02d23a09e7d added dummy polymorphic THF system diff -r 3c73f4068978 -r 265174356212 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Sep 06 18:07:44 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Sep 06 18:13:36 2011 +0200 @@ -22,15 +22,15 @@ AFun of 'a ho_type * 'a ho_type | ATyAbs of 'a list * 'a ho_type - datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic - datatype tff_explicitness = TFF_Implicit | TFF_Explicit + datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic + datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit datatype thf_flavor = THF_Without_Choice | THF_With_Choice - datatype format = + datatype tptp_format = CNF | CNF_UEQ | FOF | - TFF of tff_polymorphism * tff_explicitness | - THF0 of thf_flavor + TFF of tptp_polymorphism * tptp_explicitness | + THF of tptp_polymorphism * tptp_explicitness * thf_flavor datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = @@ -92,9 +92,9 @@ bool option -> (bool option -> 'c -> 'd -> 'd) -> ('a, 'b, 'c) formula -> 'd -> 'd val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula - val is_format_thf : format -> bool - val is_format_typed : format -> bool - val tptp_lines_for_atp_problem : format -> string problem -> string list + val is_format_thf : tptp_format -> bool + val is_format_typed : tptp_format -> bool + val tptp_lines_for_atp_problem : tptp_format -> string problem -> string list val ensure_cnf_problem : (string * string) problem -> (string * string) problem val filter_cnf_ueq_problem : @@ -130,16 +130,16 @@ AFun of 'a ho_type * 'a ho_type | ATyAbs of 'a list * 'a ho_type -datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic -datatype tff_explicitness = TFF_Implicit | TFF_Explicit +datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic +datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit datatype thf_flavor = THF_Without_Choice | THF_With_Choice -datatype format = +datatype tptp_format = CNF | CNF_UEQ | FOF | - TFF of tff_polymorphism * tff_explicitness | - THF0 of thf_flavor + TFF of tptp_polymorphism * tptp_explicitness | + THF of tptp_polymorphism * tptp_explicitness * thf_flavor datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = @@ -224,10 +224,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 (THF0 _) = true +fun is_format_thf (THF _) = true | is_format_thf _ = false fun is_format_typed (TFF _) = true - | is_format_typed (THF0 _) = true + | is_format_typed (THF _) = true | is_format_typed _ = false fun string_for_kind Axiom = "axiom" @@ -266,7 +266,7 @@ ss) ^ "]: " ^ str false ty in str true ty end -fun string_for_type (THF0 _) ty = str_for_type ty +fun string_for_type (THF _) ty = str_for_type ty | string_for_type (TFF _) ty = str_for_type (flatten_type ty) | string_for_type _ _ = raise Fail "unexpected type in untyped format" @@ -288,6 +288,9 @@ else "") +fun is_format_with_choice (THF (_, _, THF_With_Choice)) = true + | is_format_with_choice _ = false + fun string_for_term _ (ATerm (s, [])) = s | string_for_term format (ATerm (s, ts)) = if s = tptp_empty_list then @@ -298,7 +301,7 @@ |> is_format_thf format ? enclose "(" ")" else (case (s = tptp_ho_forall orelse s = tptp_ho_exists, - s = tptp_choice andalso format = THF0 THF_With_Choice, ts) of + s = tptp_choice andalso is_format_with_choice format, 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. *) @@ -306,8 +309,8 @@ (AQuant (if s = tptp_ho_forall then AForall else AExists, [(s', SOME ty)], AAtom tm)) | (_, true, [AAbs ((s', ty), tm)]) => - (*There is code in ATP_Translate to ensure that Eps is always applied - to an abstraction*) + (* There is code in "ATP_Translate" to ensure that "Eps" is always + applied to an abstraction. *) tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^ string_for_term format tm ^ "" |> enclose "(" ")" @@ -319,7 +322,7 @@ else s ^ "(" ^ commas ss ^ ")" end) - | string_for_term (format as THF0 _) (AAbs ((s, ty), tm)) = + | string_for_term (format as THF _) (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" @@ -352,7 +355,7 @@ | string_for_format CNF_UEQ = tptp_cnf | string_for_format FOF = tptp_fof | string_for_format (TFF _) = tptp_tff - | string_for_format (THF0 _) = tptp_thf + | string_for_format (THF _) = tptp_thf fun string_for_problem_line format (Decl (ident, sym, ty)) = string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^ diff -r 3c73f4068978 -r 265174356212 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Sep 06 18:07:44 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Sep 06 18:13:36 2011 +0200 @@ -7,7 +7,7 @@ signature ATP_SYSTEMS = sig - type format = ATP_Problem.format + type tptp_format = ATP_Problem.tptp_format type formula_kind = ATP_Problem.formula_kind type failure = ATP_Proof.failure @@ -22,7 +22,8 @@ conj_sym_kind : formula_kind, prem_kind : formula_kind, best_slices : - Proof.context -> (real * (bool * (int * format * string * string))) list} + Proof.context + -> (real * (bool * (int * tptp_format * string * string))) list} val force_sos : bool Config.T val e_smartN : string @@ -41,6 +42,7 @@ val e_tofofN : string val leo2N : string val pffN : string + val phfN : string val satallaxN : string val snarkN : string val spassN : string @@ -51,7 +53,7 @@ val remote_atp : string -> string -> string list -> (string * string) list -> (failure * string) list -> formula_kind -> formula_kind - -> (Proof.context -> int * format * string) -> string * atp_config + -> (Proof.context -> int * tptp_format * string) -> string * atp_config val add_atp : string * atp_config -> theory -> theory val get_atp : theory -> string -> atp_config val supported_atps : theory -> string list @@ -79,7 +81,8 @@ conj_sym_kind : formula_kind, prem_kind : formula_kind, best_slices : - Proof.context -> (real * (bool * (int * format * string * string))) list} + Proof.context + -> (real * (bool * (int * tptp_format * string * string))) list} (* "best_slices" must be found empirically, taking a wholistic approach since the ATPs are run in parallel. The "real" components give the faction of the @@ -105,6 +108,7 @@ val e_tofofN = "e_tofof" val leo2N = "leo2" val pffN = "pff" +val phfN = "phf" val satallaxN = "satallax" val snarkN = "snark" val spassN = "spass" @@ -230,6 +234,8 @@ (* LEO-II *) +val leo2_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice) + val leo2_config : atp_config = {exec = ("LEO2_HOME", "leo"), required_execs = [], @@ -243,10 +249,8 @@ prem_kind = Hypothesis, best_slices = fn ctxt => (* FUDGE *) - [(0.667, (false, (150, THF0 THF_Without_Choice, - "mono_simple_higher", sosN))), - (0.333, (true, (50, THF0 THF_Without_Choice, - "mono_simple_higher", no_sosN)))] + [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", sosN))), + (0.333, (true, (50, leo2_thf0, "mono_simple_higher", no_sosN)))] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -255,6 +259,8 @@ (* Satallax *) +val satallax_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice) + val satallax_config : atp_config = {exec = ("SATALLAX_HOME", "satallax"), required_execs = [], @@ -266,8 +272,8 @@ conj_sym_kind = Axiom, prem_kind = Hypothesis, best_slices = - K [(1.0, (true, (100, THF0 THF_With_Choice, "mono_simple_higher", "")))] - (* FUDGE *)} + (* FUDGE *) + K [(1.0, (true, (100, satallax_thf0, "mono_simple_higher", "")))]} val satallax = (satallaxN, satallax_config) @@ -314,7 +320,7 @@ fun is_old_vampire_version () = string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER -val vampire_tff = TFF (TFF_Monomorphic, TFF_Implicit) +val vampire_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit) val vampire_config : atp_config = {exec = ("VAMPIRE_HOME", "vampire"), @@ -347,9 +353,9 @@ (0.333, (false, (500, FOF, "mono_tags?", sosN))), (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))] else - [(0.333, (false, (150, vampire_tff, "poly_guards", sosN))), - (0.333, (false, (500, vampire_tff, "mono_simple", sosN))), - (0.334, (true, (50, vampire_tff, "mono_simple", no_sosN)))]) + [(0.333, (false, (150, vampire_tff0, "poly_guards", sosN))), + (0.333, (false, (500, vampire_tff0, "mono_simple", sosN))), + (0.334, (true, (50, vampire_tff0, "mono_simple", no_sosN)))]) |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -358,7 +364,7 @@ (* Z3 with TPTP syntax *) -val z3_tff = TFF (TFF_Monomorphic, TFF_Implicit) +val z3_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit) val z3_tptp_config : atp_config = {exec = ("Z3_HOME", "z3"), @@ -377,18 +383,17 @@ prem_kind = Hypothesis, best_slices = (* FUDGE *) - K [(0.5, (false, (250, z3_tff, "mono_simple", ""))), - (0.25, (false, (125, z3_tff, "mono_simple", ""))), - (0.125, (false, (62, z3_tff, "mono_simple", ""))), - (0.125, (false, (31, z3_tff, "mono_simple", "")))]} + K [(0.5, (false, (250, z3_tff0, "mono_simple", ""))), + (0.25, (false, (125, z3_tff0, "mono_simple", ""))), + (0.125, (false, (62, z3_tff0, "mono_simple", ""))), + (0.125, (false, (31, z3_tff0, "mono_simple", "")))]} val z3_tptp = (z3_tptpN, z3_tptp_config) -(* Not really a prover: Experimental PFF (Polymorphic TFF) output *) -val poly_tff = TFF (TFF_Polymorphic, TFF_Implicit) +(* Not really a prover: Experimental Polymorphic TFF and THF output *) -val pff_config : atp_config = +fun dummy_config format type_enc : atp_config = {exec = ("ISABELLE_ATP", "scripts/dummy_atp"), required_execs = [], arguments = K (K (K (K (K "")))), @@ -396,10 +401,16 @@ known_failures = [(GaveUp, "SZS status Unknown")], conj_sym_kind = Hypothesis, prem_kind = Hypothesis, - best_slices = K [(1.0, (false, (200, poly_tff, "poly_simple", "")))]} + best_slices = K [(1.0, (false, (200, format, type_enc, "")))]} +val pff_format = TFF (TPTP_Polymorphic, TPTP_Implicit) +val pff_config = dummy_config pff_format "poly_simple" val pff = (pffN, pff_config) +val phf_format = THF (TPTP_Polymorphic, TPTP_Implicit, THF_With_Choice) +val phf_config = dummy_config phf_format "poly_simple_higher" +val phf = (phfN, phf_config) + (* Remote ATP invocation via SystemOnTPTP *) @@ -475,34 +486,33 @@ (remote_prefix ^ name, remotify_config system_name system_versions best_slice config) -val dumb_tff = TFF (TFF_Monomorphic, TFF_Explicit) +val explicit_tff0 = TFF (TPTP_Monomorphic, TPTP_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, THF0 THF_Without_Choice, - "mono_simple_higher") (* FUDGE *)) + (K (100, leo2_thf0, "mono_simple_higher") (* FUDGE *)) val remote_satallax = remotify_atp satallax "Satallax" ["2.1", "2.0", "2"] - (K (100, THF0 THF_With_Choice, - "mono_simple_higher") (* FUDGE *)) + (K (100, satallax_thf0, "mono_simple_higher") (* FUDGE *)) val remote_vampire = remotify_atp vampire "Vampire" ["1.8"] (K (250, FOF, "mono_guards?") (* FUDGE *)) val remote_z3_tptp = - remotify_atp z3_tptp "Z3" ["3.0"] (K (250, z3_tff, "mono_simple") (* FUDGE *)) + remotify_atp z3_tptp "Z3" ["3.0"] + (K (250, z3_tff0, "mono_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, dumb_tff, "mono_simple") (* FUDGE *)) + (K (100, explicit_tff0, "mono_simple") (* FUDGE *)) val remote_e_tofof = remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom - Hypothesis (K (150, dumb_tff, "mono_simple") (* FUDGE *)) + Hypothesis (K (150, explicit_tff0, "mono_simple") (* FUDGE *)) val remote_waldmeister = remote_atp waldmeisterN "Waldmeister" ["710"] [("#START OF PROOF", "Proved Goals:")] @@ -532,7 +542,7 @@ Synchronized.change systems (fn _ => get_systems ()) val atps = - [e, leo2, pff, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2, + [e, leo2, pff, phf, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark, remote_e_tofof, remote_waldmeister] val setup = fold add_atp atps diff -r 3c73f4068978 -r 265174356212 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Sep 06 18:07:44 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Sep 06 18:13:36 2011 +0200 @@ -11,7 +11,7 @@ type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term type connective = ATP_Problem.connective type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula - type format = ATP_Problem.format + type tptp_format = ATP_Problem.tptp_format type formula_kind = ATP_Problem.formula_kind type 'a problem = 'a ATP_Problem.problem @@ -92,7 +92,7 @@ val level_of_type_enc : type_enc -> type_level val is_type_enc_quasi_sound : type_enc -> bool val is_type_enc_fairly_sound : type_enc -> bool - val adjust_type_enc : format -> type_enc -> type_enc + val adjust_type_enc : tptp_format -> type_enc -> type_enc val mk_aconns : connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula val unmangled_const : string -> string * (string, 'b) ho_term list @@ -100,7 +100,7 @@ val helper_table : ((string * bool) * thm list) list val factsN : string val prepare_atp_problem : - Proof.context -> format -> formula_kind -> formula_kind -> type_enc + Proof.context -> tptp_format -> formula_kind -> formula_kind -> type_enc -> bool -> string -> bool -> bool -> term list -> term -> ((string * locality) * term) list -> string problem * string Symtab.table * int * int @@ -142,7 +142,7 @@ (* TFF1 is still in development, and it is still unclear whether symbols will be allowed to have types like "$tType > $o" (i.e., "![A : $tType] : $o"), with "dummy" type variables. *) -val exploit_tff1_dummy_type_vars = false +val avoid_first_order_dummy_type_vars = true val bound_var_prefix = "B_" val all_bound_var_prefix = "BA_" @@ -325,8 +325,8 @@ fun default c = const_prefix ^ lookup_const c in fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal - | make_fixed_const (SOME (THF0 THF_With_Choice)) c = - if c = choice_const then tptp_choice else default c + | make_fixed_const (SOME (THF (_, _, THF_With_Choice))) c = + if c = choice_const then tptp_choice else default c | make_fixed_const _ c = default c end @@ -587,7 +587,9 @@ | _ => raise Same.SAME) | ("simple_higher", (SOME poly, _, Nonuniform)) => (case (poly, level) of - (_, Noninf_Nonmono_Types _) => raise Same.SAME + (Polymorphic, All_Types) => + Simple_Types (Higher_Order, Polymorphic, All_Types) + | (_, Noninf_Nonmono_Types _) => raise Same.SAME | (Mangled_Monomorphic, _) => Simple_Types (Higher_Order, Mangled_Monomorphic, level) | _ => raise Same.SAME) @@ -631,12 +633,13 @@ | is_type_level_monotonicity_based Fin_Nonmono_Types = true | is_type_level_monotonicity_based _ = false -fun adjust_type_enc (THF0 _) (Simple_Types (order, Polymorphic, level)) = +fun adjust_type_enc (THF (TPTP_Monomorphic, _, _)) + (Simple_Types (order, _, level)) = Simple_Types (order, Mangled_Monomorphic, level) - | adjust_type_enc (THF0 _) type_enc = type_enc - | adjust_type_enc (TFF (TFF_Monomorphic, _)) (Simple_Types (_, _, level)) = + | adjust_type_enc (THF _) type_enc = type_enc + | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) = Simple_Types (First_Order, Mangled_Monomorphic, level) - | adjust_type_enc (TFF (_, _)) (Simple_Types (_, poly, level)) = + | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) = Simple_Types (First_Order, poly, level) | adjust_type_enc format (Simple_Types (_, poly, level)) = adjust_type_enc format (Guards (poly, level, Uniform)) @@ -746,8 +749,9 @@ fun type_class_formula type_enc class arg = AAtom (ATerm (class, arg :: (case type_enc of - Simple_Types (_, Polymorphic, _) => - if exploit_tff1_dummy_type_vars then [] else [ATerm (TYPE_name, [arg])] + Simple_Types (First_Order, Polymorphic, _) => + if avoid_first_order_dummy_type_vars then [ATerm (TYPE_name, [arg])] + else [] | _ => []))) fun formulas_for_types type_enc add_sorts_on_typ Ts = [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts @@ -1779,18 +1783,19 @@ (** Symbol declarations **) -fun decl_line_for_class s = +fun decl_line_for_class order s = let val name as (s, _) = `make_type_class s in Decl (sym_decl_prefix ^ s, name, - if exploit_tff1_dummy_type_vars then - AFun (atype_of_types, bool_atype) + if order = First_Order andalso avoid_first_order_dummy_type_vars then + ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype)) else - ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype))) + AFun (atype_of_types, bool_atype)) end fun decl_lines_for_classes type_enc classes = case type_enc of - Simple_Types (_, Polymorphic, _) => map decl_line_for_class classes + Simple_Types (order, Polymorphic, _) => + map (decl_line_for_class order) classes | _ => [] fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab @@ -2232,7 +2237,8 @@ CNF => ensure_cnf_problem | CNF_UEQ => filter_cnf_ueq_problem | FOF => I - | TFF (_, TFF_Implicit) => I + | TFF (_, TPTP_Implicit) => I + | THF (_, TPTP_Implicit, _) => I | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix implicit_declsN) val (problem, pool) = problem |> nice_atp_problem readable_names