# HG changeset patch # User blanchet # Date 1319886958 -7200 # Node ID 866b075aa99bbe18fe3c4264f91169ced3086693 # Parent d8c8c2fcab2cd19d3ca10b51ea089deccb558b6b added sorted DFG output for coming version of SPASS diff -r d8c8c2fcab2c -r 866b075aa99b src/HOL/TPTP/atp_export.ML --- a/src/HOL/TPTP/atp_export.ML Sat Oct 29 13:15:58 2011 +0200 +++ b/src/HOL/TPTP/atp_export.ML Sat Oct 29 13:15:58 2011 +0200 @@ -115,8 +115,7 @@ val prob_file = File.tmp_path (Path.explode "prob.tptp") val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy spassN - val _ = problem |> tptp_lines_for_atp_problem FOF - |> File.write_list prob_file + val _ = problem |> lines_for_atp_problem FOF |> File.write_list prob_file val command = File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^ " " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^ @@ -189,7 +188,7 @@ val atp_problem = atp_problem |> add_inferences_to_problem infers |> order_problem_facts name_ord - val ss = tptp_lines_for_atp_problem FOF atp_problem + val ss = lines_for_atp_problem FOF atp_problem val _ = app (File.append path) ss in () end diff -r d8c8c2fcab2c -r 866b075aa99b src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Sat Oct 29 13:15:58 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Sat Oct 29 13:15:58 2011 +0200 @@ -25,12 +25,14 @@ datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit datatype thf_flavor = THF_Without_Choice | THF_With_Choice - datatype tptp_format = + + datatype atp_format = CNF | CNF_UEQ | FOF | TFF of tptp_polymorphism * tptp_explicitness | - THF of tptp_polymorphism * tptp_explicitness * thf_flavor + THF of tptp_polymorphism * tptp_explicitness * thf_flavor | + DFG_Sorted datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = @@ -41,6 +43,11 @@ * (string, string ho_type) ho_term option type 'a problem = (string * 'a problem_line list) list + val isabelle_info_prefix : string + val isabelle_info : atp_format -> string -> (string, 'a) ho_term option + val introN : string + val elimN : string + val simpN : string val tptp_cnf : string val tptp_fof : string val tptp_tff : string @@ -92,9 +99,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 : tptp_format -> bool - val is_format_typed : tptp_format -> bool - val tptp_lines_for_atp_problem : tptp_format -> string problem -> string list + val is_format_thf : atp_format -> bool + val is_format_typed : atp_format -> bool + val lines_for_atp_problem : atp_format -> string problem -> string list val ensure_cnf_problem : (string * string) problem -> (string * string) problem val filter_cnf_ueq_problem : @@ -134,12 +141,13 @@ datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit datatype thf_flavor = THF_Without_Choice | THF_With_Choice -datatype tptp_format = +datatype atp_format = CNF | CNF_UEQ | FOF | TFF of tptp_polymorphism * tptp_explicitness | - THF of tptp_polymorphism * tptp_explicitness * thf_flavor + THF of tptp_polymorphism * tptp_explicitness * thf_flavor | + DFG_Sorted datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = @@ -148,6 +156,21 @@ * (string, string ho_type) ho_term option * (string, string ho_type) ho_term option type 'a problem = (string * 'a problem_line list) list +val isabelle_info_prefix = "isabelle_" + +(* Currently, only SPASS supports Isabelle metainformation. *) +fun isabelle_info DFG_Sorted s = + SOME (ATerm ("[]", [ATerm (isabelle_info_prefix ^ s, [])])) + | isabelle_info _ _ = NONE + +val introN = "intro" +val elimN = "elim" +val simpN = "simp" + +fun is_isabelle_info suffix (SOME (ATerm ("[]", [ATerm (s, [])]))) = + s = isabelle_info_prefix ^ suffix + | is_isabelle_info _ _ = false + (* official TPTP syntax *) val tptp_cnf = "cnf" val tptp_fof = "fof" @@ -186,6 +209,10 @@ fun is_tptp_variable s = Char.isUpper (String.sub (s, 0)) val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol) +val atype_of_types = AType (`I tptp_type_of_types, []) +val bool_atype = AType (`I tptp_bool_type, []) +val individual_atype = AType (`I tptp_individual_type, []) + fun raw_polarities_of_conn ANot = (SOME false, NONE) | raw_polarities_of_conn AAnd = (SOME true, SOME true) | raw_polarities_of_conn AOr = (SOME true, SOME true) @@ -228,15 +255,16 @@ | is_format_thf _ = false fun is_format_typed (TFF _) = true | is_format_typed (THF _) = true + | is_format_typed (DFG_Sorted) = true | is_format_typed _ = false -fun string_for_kind Axiom = "axiom" - | string_for_kind Definition = "definition" - | string_for_kind Lemma = "lemma" - | string_for_kind Hypothesis = "hypothesis" - | string_for_kind Conjecture = "conjecture" +fun tptp_string_for_kind Axiom = "axiom" + | tptp_string_for_kind Definition = "definition" + | tptp_string_for_kind Lemma = "lemma" + | tptp_string_for_kind Hypothesis = "hypothesis" + | tptp_string_for_kind Conjecture = "conjecture" -fun string_for_app format func args = +fun tptp_string_for_app format func args = if is_format_thf format then "(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")" else @@ -255,17 +283,21 @@ fun str_for_type format ty = let - fun str _ (AType (s, [])) = s + val dfg = (format = DFG_Sorted) + fun str _ (AType (s, [])) = + if dfg andalso s = tptp_individual_type then "Top" else s | str _ (AType (s, tys)) = let val ss = tys |> map (str false) in if s = tptp_product_type then - ss |> space_implode (" " ^ tptp_product_type ^ " ") - |> length ss > 1 ? enclose "(" ")" + ss |> space_implode + (if dfg then ", " else " " ^ tptp_product_type ^ " ") + |> (not dfg andalso length ss > 1) ? enclose "(" ")" else - string_for_app format s ss + tptp_string_for_app format s ss end | str rhs (AFun (ty1, ty2)) = - str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2 + (str false ty1 |> dfg ? enclose "(" ")") ^ " " ^ + (if dfg then "" else tptp_fun_type ^ " ") ^ str true ty2 |> not rhs ? enclose "(" ")" | str _ (ATyAbs (ss, ty)) = tptp_pi_binder ^ "[" ^ @@ -274,17 +306,16 @@ in str true ty end fun string_for_type (format as THF _) ty = str_for_type format ty - | string_for_type (format as TFF _) ty = str_for_type format (flatten_type ty) - | string_for_type _ _ = raise Fail "unexpected type in untyped format" + | string_for_type format ty = str_for_type format (flatten_type ty) -fun string_for_quantifier AForall = tptp_forall - | string_for_quantifier AExists = tptp_exists +fun tptp_string_for_quantifier AForall = tptp_forall + | tptp_string_for_quantifier AExists = tptp_exists -fun string_for_connective ANot = tptp_not - | string_for_connective AAnd = tptp_and - | string_for_connective AOr = tptp_or - | string_for_connective AImplies = tptp_implies - | string_for_connective AIff = tptp_iff +fun tptp_string_for_connective ANot = tptp_not + | tptp_string_for_connective AAnd = tptp_and + | tptp_string_for_connective AOr = tptp_or + | tptp_string_for_connective AImplies = tptp_implies + | tptp_string_for_connective AIff = tptp_iff fun string_for_bound_var format (s, ty) = s ^ @@ -298,84 +329,193 @@ 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)) = +fun tptp_string_for_term _ (ATerm (s, [])) = s + | tptp_string_for_term format (ATerm (s, ts)) = (if s = tptp_empty_list then (* used for lists in the optional "source" field of a derivation *) - "[" ^ commas (map (string_for_term format) ts) ^ "]" + "[" ^ commas (map (tptp_string_for_term format) ts) ^ "]" else if is_tptp_equal s then - space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts) + space_implode (" " ^ tptp_equal ^ " ") + (map (tptp_string_for_term format) ts) |> is_format_thf format ? enclose "(" ")" else case (s = tptp_ho_forall orelse s = tptp_ho_exists, 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. *) - string_for_formula format + tptp_string_for_formula format (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. *) tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^ - string_for_term format tm ^ "" + tptp_string_for_term format tm ^ "" |> enclose "(" ")" - | _ => string_for_app format s (map (string_for_term format) ts)) - | string_for_term (format as THF _) (AAbs ((s, ty), tm)) = + | _ => tptp_string_for_app format s (map (tptp_string_for_term format) ts)) + | tptp_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" -and string_for_formula format (AQuant (q, xs, phi)) = - string_for_quantifier q ^ + tptp_string_for_term format tm ^ ")" + | tptp_string_for_term _ _ = + raise Fail "unexpected term in first-order format" +and tptp_string_for_formula format (AQuant (q, xs, phi)) = + tptp_string_for_quantifier q ^ "[" ^ commas (map (string_for_bound_var format) xs) ^ "]: " ^ - string_for_formula format phi + tptp_string_for_formula format phi |> enclose "(" ")" - | string_for_formula format + | tptp_string_for_formula format (AConn (ANot, [AAtom (ATerm ("=" (* tptp_equal *), ts))])) = space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ") - (map (string_for_term format) ts) + (map (tptp_string_for_term format) ts) |> is_format_thf format ? enclose "(" ")" - | string_for_formula format (AConn (c, [phi])) = - string_for_connective c ^ " " ^ - (string_for_formula format phi |> is_format_thf format ? enclose "(" ")") + | tptp_string_for_formula format (AConn (c, [phi])) = + tptp_string_for_connective c ^ " " ^ + (tptp_string_for_formula format phi + |> is_format_thf format ? enclose "(" ")") |> enclose "(" ")" - | string_for_formula format (AConn (c, phis)) = - space_implode (" " ^ string_for_connective c ^ " ") - (map (string_for_formula format) phis) + | tptp_string_for_formula format (AConn (c, phis)) = + space_implode (" " ^ tptp_string_for_connective c ^ " ") + (map (tptp_string_for_formula format) phis) |> enclose "(" ")" - | string_for_formula format (AAtom tm) = string_for_term format tm + | tptp_string_for_formula format (AAtom tm) = tptp_string_for_term format tm fun the_source (SOME source) = source | the_source NONE = ATerm ("inference", ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", []))) -fun string_for_format CNF = tptp_cnf - | 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 +fun tptp_string_for_format CNF = tptp_cnf + | tptp_string_for_format CNF_UEQ = tptp_cnf + | tptp_string_for_format FOF = tptp_fof + | tptp_string_for_format (TFF _) = tptp_tff + | tptp_string_for_format (THF _) = tptp_thf + | tptp_string_for_format DFG_Sorted = raise Fail "non-TPTP format" -fun string_for_problem_line format (Decl (ident, sym, ty)) = - string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^ - string_for_type format ty ^ ").\n" - | string_for_problem_line format (Formula (ident, kind, phi, source, info)) = - string_for_format format ^ "(" ^ ident ^ ", " ^ string_for_kind kind ^ - ",\n (" ^ string_for_formula format phi ^ ")" ^ +fun tptp_string_for_problem_line format (Decl (ident, sym, ty)) = + tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ + " : " ^ string_for_type format ty ^ ").\n" + | tptp_string_for_problem_line format + (Formula (ident, kind, phi, source, info)) = + tptp_string_for_format format ^ "(" ^ ident ^ ", " ^ + tptp_string_for_kind kind ^ ",\n (" ^ + tptp_string_for_formula format phi ^ ")" ^ (case (source, info) of (NONE, NONE) => "" - | (SOME tm, NONE) => ", " ^ string_for_term format tm + | (SOME tm, NONE) => ", " ^ tptp_string_for_term format tm | (_, SOME tm) => - ", " ^ string_for_term format (the_source source) ^ - ", " ^ string_for_term format tm) ^ ").\n" -fun tptp_lines_for_atp_problem format problem = - "% This file was generated by Isabelle (most likely Sledgehammer)\n\ - \% " ^ timestamp () ^ "\n" :: + ", " ^ tptp_string_for_term format (the_source source) ^ + ", " ^ tptp_string_for_term format tm) ^ ").\n" + +fun tptp_lines format = maps (fn (_, []) => [] | (heading, lines) => "\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" :: - map (string_for_problem_line format) lines) - problem + map (tptp_string_for_problem_line format) lines) + +fun arity_of_type (AFun (_, ty)) = 1 + arity_of_type ty + | arity_of_type _ = 0 + +fun binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2 + | binder_atypes _ = [] + +fun is_function_type (AFun (_, ty)) = is_function_type ty + | is_function_type (AType (s, _)) = + s <> tptp_type_of_types andalso s <> tptp_bool_type + | is_function_type _ = false + +fun is_predicate_type (AFun (_, ty)) = is_predicate_type ty + | is_predicate_type (AType (s, _)) = (s = tptp_bool_type) + | is_predicate_type _ = false + +fun dfg_string_for_formula info = + let + fun str_for_term simp (ATerm (s, tms)) = + (if is_tptp_equal s then "equal" |> simp ? suffix ":lr" + else if s = tptp_true then "true" + else if s = tptp_false then "false" + else s) ^ + (if null tms then "" + else "(" ^ commas (map (str_for_term false) tms) ^ ")") + | str_for_term _ _ = raise Fail "unexpected term in first-order format" + fun str_for_quant AForall = "forall" + | str_for_quant AExists = "exists" + fun str_for_conn _ ANot = "not" + | str_for_conn _ AAnd = "and" + | str_for_conn _ AOr = "or" + | str_for_conn _ AImplies = "implies" + | str_for_conn simp AIff = "equiv" |> simp ? suffix ":lr" + fun str_for_formula simp (AQuant (q, xs, phi)) = + str_for_quant q ^ "(" ^ "[" ^ + commas (map (string_for_bound_var DFG_Sorted) xs) ^ "], " ^ + str_for_formula simp phi ^ ")" + | str_for_formula simp (AConn (c, phis)) = + str_for_conn simp c ^ "(" ^ + commas (map (str_for_formula false) phis) ^ ")" + | str_for_formula simp (AAtom tm) = str_for_term simp tm + in str_for_formula (is_isabelle_info simpN info) end + +fun dfg_lines problem = + let + fun ary sym ty = + "(" ^ sym ^ ", " ^ string_of_int (arity_of_type ty) ^ ")" + fun fun_typ sym ty = + "function(" ^ sym ^ ", " ^ string_for_type DFG_Sorted ty ^ ")." + fun pred_typ sym ty = + "predicate(" ^ + commas (sym :: map (string_for_type DFG_Sorted) (binder_atypes ty)) ^ ")." + fun formula pred (Formula (ident, kind, phi, _, info)) = + if pred kind then + SOME ("formula(" ^ dfg_string_for_formula info phi ^ ", " ^ ident ^ + ").") + else + NONE + | formula _ _ = NONE + fun filt f = problem |> map (map_filter f o snd) |> flat + val func_aries = + filt (fn Decl (_, sym, ty) => + if is_function_type ty then SOME (ary sym ty) else NONE + | _ => NONE) + |> commas |> enclose "functions [" "]." + val pred_aries = + filt (fn Decl (_, sym, ty) => + if is_predicate_type ty then SOME (ary sym ty) else NONE + | _ => NONE) + |> commas |> enclose "predicates [" "]." + val sorts = + filt (fn Decl (_, sym, AType (s, [])) => + if s = tptp_type_of_types then SOME sym else NONE + | _ => NONE) + |> commas |> enclose "sorts [" "]." + val func_sigs = + filt (fn Decl (_, sym, ty) => + if is_function_type ty then SOME (fun_typ sym ty) else NONE + | _ => NONE) + val pred_sigs = + filt (fn Decl (_, sym, ty) => + if is_predicate_type ty then SOME (pred_typ sym ty) else NONE + | _ => NONE) + val axioms = filt (formula (curry (op <>) Conjecture)) + val conjs = filt (formula (curry (op =) Conjecture)) + fun list_of _ [] = [] + | list_of heading ss = + "list_of_" ^ heading ^ ".\n" :: map (suffix "\n") ss @ + ["end_of_list.\n\n"] + in + "\nbegin_problem(isabelle).\n\n" :: + list_of "descriptions" + ["name({**}).", "author({**}).", "status(unknown).", + "description({**})."] @ + list_of "symbols" [func_aries, pred_aries, sorts] @ + list_of "declarations" (func_sigs @ pred_sigs) @ + list_of "formulae(axioms)" axioms @ + list_of "formulae(conjectures)" conjs @ + ["end_problem.\n"] + end + +fun lines_for_atp_problem format problem = + "% This file was generated by Isabelle (most likely Sledgehammer)\n\ + \% " ^ timestamp () ^ "\n" :: + (if format = DFG_Sorted then dfg_lines else tptp_lines format) problem (** CNF (Metis) and CNF UEQ (Waldmeister) **) @@ -467,11 +607,6 @@ (* TFF allows implicit declarations of types, function symbols, and predicate symbols (with "$i" as the type of individuals), but some provers (e.g., SNARK) require explicit declarations. The situation is similar for THF. *) - -val atype_of_types = AType (`I tptp_type_of_types, []) -val bool_atype = AType (`I tptp_bool_type, []) -val individual_atype = AType (`I tptp_individual_type, []) - fun default_type pred_sym = let fun typ 0 = if pred_sym then bool_atype else individual_atype @@ -548,7 +683,12 @@ unreadable "op_1", "op_2", etc., in the problem files. "eq" is reserved to ensure that "HOL.eq" is correctly mapped to equality (not clear whether this is still necessary). *) -val reserved_nice_names = [tptp_old_equal, "op", "eq"] +val spass_reserved_nice_names = + ["forall", "exists", "le", "ls", "ge", "gs", "plus", "minus", "mult", "fract", + "equal", "true", "false", "or", "and", "not", "implies", "implied", "equiv", + "lr", "def"] +val reserved_nice_names = + [tptp_old_equal, "op", "eq"] @ spass_reserved_nice_names fun readable_name full_name s = if s = full_name then diff -r d8c8c2fcab2c -r 866b075aa99b src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Sat Oct 29 13:15:58 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Sat Oct 29 13:15:58 2011 +0200 @@ -24,8 +24,6 @@ TimedOut | Inappropriate | OutOfResources | - SpassTooOld | - VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput | @@ -81,8 +79,6 @@ TimedOut | Inappropriate | OutOfResources | - SpassTooOld | - VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput | @@ -134,17 +130,6 @@ | string_for_failure Inappropriate = "The problem lies outside the prover's scope." | string_for_failure OutOfResources = "The prover ran out of resources." - | string_for_failure SpassTooOld = - "Isabelle requires a more recent version of SPASS with support for the \ - \TPTP syntax. To install it, download and extract the package \ - \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \ - \\"spass-3.7\" directory's absolute path to " ^ - Path.print (Path.expand (Path.explode "$ISABELLE_HOME_USER/etc/components")) ^ - " on a line of its own." - | string_for_failure VampireTooOld = - "Isabelle requires a more recent version of Vampire. To install it, follow \ - \the instructions from the Sledgehammer manual (\"isabelle doc\ - \ sledgehammer\")." | string_for_failure NoPerl = "Perl" ^ missing_message_tail | string_for_failure NoLibwwwPerl = "The Perl module \"libwww-perl\"" ^ missing_message_tail diff -r d8c8c2fcab2c -r 866b075aa99b src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Sat Oct 29 13:15:58 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sat Oct 29 13:15:58 2011 +0200 @@ -7,7 +7,7 @@ signature ATP_SYSTEMS = sig - type tptp_format = ATP_Problem.tptp_format + type atp_format = ATP_Problem.atp_format type formula_kind = ATP_Problem.formula_kind type failure = ATP_Proof.failure @@ -23,7 +23,7 @@ prem_kind : formula_kind, best_slices : Proof.context - -> (real * (bool * (int * tptp_format * string * string))) list} + -> (real * (bool * (int * atp_format * string * string))) list} val force_sos : bool Config.T val e_smartN : string @@ -46,6 +46,7 @@ val satallaxN : string val snarkN : string val spassN : string + val spass_newN : string val vampireN : string val waldmeisterN : string val z3_tptpN : string @@ -53,7 +54,7 @@ val remote_atp : string -> string -> string list -> (string * string) list -> (failure * string) list -> formula_kind -> formula_kind - -> (Proof.context -> int * tptp_format * string) -> string * atp_config + -> (Proof.context -> int * atp_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 @@ -82,7 +83,7 @@ prem_kind : formula_kind, best_slices : Proof.context - -> (real * (bool * (int * tptp_format * string * string))) list} + -> (real * (bool * (int * atp_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 @@ -130,6 +131,7 @@ val satallaxN = "satallax" val snarkN = "snark" val spassN = "spass" +val spass_newN = "spass_new" val vampireN = "vampire" val waldmeisterN = "waldmeister" val z3_tptpN = "z3_tptp" @@ -315,7 +317,6 @@ (MalformedInput, "Undefined symbol"), (MalformedInput, "Free Variable"), (Unprovable, "No formulae and clauses found in input file"), - (SpassTooOld, "tptp2dfg"), (InternalError, "Please report this error")], conj_sym_kind = Hypothesis, prem_kind = Conjecture, @@ -329,6 +330,25 @@ val spass = (spassN, spass_config) +(* Experimental *) +val spass_new_config : atp_config = + {exec = ("SPASS_HOME", "SPASS"), + required_execs = [], + arguments = #arguments spass_config, + proof_delims = #proof_delims spass_config, + known_failures = #known_failures spass_config, + conj_sym_kind = #conj_sym_kind spass_config, + prem_kind = #prem_kind spass_config, + best_slices = fn ctxt => + (* FUDGE *) + [(0.333, (false, (150, DFG_Sorted, "mono_simple", sosN))) (*, + (0.333, (false, (300, DFG_Sorted, "poly_tags??", sosN))), + (0.334, (true, (50, DFG_Sorted, "mono_simple", no_sosN)))*)] + |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single + else I)} + +val spass_new = (spass_newN, spass_new_config) + (* Vampire *) @@ -359,7 +379,6 @@ (GaveUp, "CANNOT PROVE"), (Unprovable, "Satisfiability detected"), (Unprovable, "Termination reason: Satisfiable"), - (VampireTooOld, "not a valid option"), (Interrupted, "Aborted by signal SIGINT")], conj_sym_kind = Conjecture, prem_kind = Conjecture, @@ -545,9 +564,9 @@ Synchronized.change systems (fn _ => get_systems ()) val atps = - [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] + [e, leo2, pff, phf, satallax, spass, spass_new, 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 end; diff -r d8c8c2fcab2c -r 866b075aa99b src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Sat Oct 29 13:15:58 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Sat Oct 29 13:15:58 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 tptp_format = ATP_Problem.tptp_format + type atp_format = ATP_Problem.atp_format type formula_kind = ATP_Problem.formula_kind type 'a problem = 'a ATP_Problem.problem @@ -86,7 +86,7 @@ val is_type_enc_quasi_sound : type_enc -> bool val is_type_enc_fairly_sound : type_enc -> bool val type_enc_from_string : soundness -> string -> type_enc - val adjust_type_enc : tptp_format -> type_enc -> type_enc + val adjust_type_enc : atp_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 @@ -94,7 +94,7 @@ val helper_table : ((string * bool) * thm list) list val factsN : string val prepare_atp_problem : - Proof.context -> tptp_format -> formula_kind -> formula_kind -> type_enc + Proof.context -> atp_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 @@ -123,20 +123,10 @@ val lambdasN = "lambdas" val smartN = "smart" -val generate_info = false (* experimental *) - -fun isabelle_info s = - if generate_info then SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])])) - else NONE - -val introN = "intro" -val elimN = "elim" -val simpN = "simp" - (* 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 avoid_first_order_dummy_type_vars = true + ghost type variables. *) +val avoid_first_order_ghost_type_vars = true val bound_var_prefix = "B_" val all_bound_var_prefix = "BA_" @@ -313,7 +303,7 @@ tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i)) fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x)) -(* "HOL.eq" and Choice are mapped to the ATP's equivalents *) +(* "HOL.eq" and choice are mapped to the ATP's equivalents *) local val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT fun default c = const_prefix ^ lookup_const c @@ -650,6 +640,8 @@ | 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 DFG_Sorted (Simple_Types (_, _, level)) = + Simple_Types (First_Order, Mangled_Monomorphic, level) | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) = Simple_Types (First_Order, poly, level) | adjust_type_enc format (Simple_Types (_, poly, level)) = @@ -755,7 +747,7 @@ AAtom (ATerm (class, arg :: (case type_enc of Simple_Types (First_Order, Polymorphic, _) => - if avoid_first_order_dummy_type_vars then [ATerm (TYPE_name, [arg])] + if avoid_first_order_ghost_type_vars then [ATerm (TYPE_name, [arg])] else [] | _ => []))) fun formulas_for_types type_enc add_sorts_on_typ Ts = @@ -1545,7 +1537,7 @@ val type_tag = `(make_fixed_const NONE) type_tag_name -fun type_tag_idempotence_fact type_enc = +fun type_tag_idempotence_fact format type_enc = let fun var s = ATerm (`I s, []) fun tag tm = ATerm (type_tag, [var "A", tm]) @@ -1553,7 +1545,7 @@ in Formula (type_tag_idempotence_helper_name, Axiom, eq_formula type_enc [] false (tag tagged_var) tagged_var, - isabelle_info simpN, NONE) + isabelle_info format simpN, NONE) end fun should_specialize_helper type_enc t = @@ -1833,32 +1825,34 @@ |> close_formula_universally type_enc, NONE, case locality of - Intro => isabelle_info introN - | Elim => isabelle_info elimN - | Simp => isabelle_info simpN + Intro => isabelle_info format introN + | Elim => isabelle_info format elimN + | Simp => isabelle_info format simpN | _ => NONE) |> Formula -fun formula_line_for_class_rel_clause type_enc +fun formula_line_for_class_rel_clause format type_enc ({name, subclass, superclass, ...} : class_rel_clause) = let val ty_arg = ATerm (tvar_a_name, []) in Formula (class_rel_clause_prefix ^ ascii_of name, Axiom, AConn (AImplies, [type_class_formula type_enc subclass ty_arg, type_class_formula type_enc superclass ty_arg]) - |> close_formula_universally type_enc, isabelle_info introN, NONE) + |> close_formula_universally type_enc, + isabelle_info format introN, NONE) end fun formula_from_arity_atom type_enc (class, t, args) = ATerm (t, map (fn arg => ATerm (arg, [])) args) |> type_class_formula type_enc class -fun formula_line_for_arity_clause type_enc +fun formula_line_for_arity_clause format type_enc ({name, prem_atoms, concl_atom, ...} : arity_clause) = Formula (arity_clause_prefix ^ name, Axiom, mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms) (formula_from_arity_atom type_enc concl_atom) - |> close_formula_universally type_enc, isabelle_info introN, NONE) + |> close_formula_universally type_enc, + isabelle_info format introN, NONE) fun formula_line_for_conjecture ctxt format mono type_enc ({name, kind, iformula, atomic_types, ...} : translated_formula) = @@ -1883,7 +1877,7 @@ fun decl_line_for_class order s = let val name as (s, _) = `make_type_class s in Decl (sym_decl_prefix ^ s, name, - if order = First_Order andalso avoid_first_order_dummy_type_vars then + if order = First_Order andalso avoid_first_order_ghost_type_vars then ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype)) else AFun (atype_of_types, bool_atype)) @@ -2059,7 +2053,7 @@ (K (K (K (K (K (K true)))))) (SOME true) |> bound_tvars type_enc (atyps_of T) |> close_formula_universally type_enc, - isabelle_info introN, NONE) + isabelle_info format introN, NONE) fun formula_line_for_tags_mono_type ctxt format mono type_enc T = let val x_var = ATerm (`make_bound_var "X", []) in @@ -2069,7 +2063,7 @@ eq_formula type_enc (atyps_of T) false (tag_with_type ctxt format mono type_enc NONE T x_var) x_var, - isabelle_info simpN, NONE) + isabelle_info format simpN, NONE) end fun problem_lines_for_mono_types ctxt format mono type_enc Ts = @@ -2143,7 +2137,7 @@ |> n > 1 ? bound_tvars type_enc (atyps_of T) |> close_formula_universally type_enc |> maybe_negate, - isabelle_info introN, NONE) + isabelle_info format introN, NONE) end fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s @@ -2179,7 +2173,7 @@ in cons (Formula (ident_base ^ "_res", kind, eq (tag_with res_T (cst bounds)) (cst tagged_bounds), - isabelle_info simpN, NONE)) + isabelle_info format simpN, NONE)) end else I @@ -2191,7 +2185,7 @@ cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind, eq (cst (bounds1 @ tag_with arg_T bound :: bounds2)) (cst bounds), - isabelle_info simpN, NONE)) + isabelle_info format simpN, NONE)) | _ => raise Fail "expected nonempty tail" else I @@ -2343,7 +2337,7 @@ |> map (formula_line_for_fact ctxt format helper_prefix I false true mono type_enc) |> (if needs_type_tag_idempotence ctxt type_enc then - cons (type_tag_idempotence_fact type_enc) + cons (type_tag_idempotence_fact format type_enc) else I) (* Reordering these might confuse the proof reconstruction code or the SPASS @@ -2355,8 +2349,10 @@ (not exporter) (not exporter) mono type_enc) (0 upto length facts - 1 ~~ facts)), (class_relsN, - map (formula_line_for_class_rel_clause type_enc) class_rel_clauses), - (aritiesN, map (formula_line_for_arity_clause type_enc) arity_clauses), + map (formula_line_for_class_rel_clause format type_enc) + class_rel_clauses), + (aritiesN, + map (formula_line_for_arity_clause format type_enc) arity_clauses), (helpersN, helper_lines), (conjsN, map (formula_line_for_conjecture ctxt format mono type_enc) conjs), diff -r d8c8c2fcab2c -r 866b075aa99b src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat Oct 29 13:15:58 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat Oct 29 13:15:58 2011 +0200 @@ -799,28 +799,28 @@ is_that_fact thm end) -fun meta_equify (@{const Trueprop} - $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2)) = - Const (@{const_name "=="}, T --> T --> @{typ prop}) $ t1 $ t2 - | meta_equify t = t - -val normalize_simp_prop = - meta_equify - #> map_aterms (fn Var ((s, _), T) => Var ((s, 0), T) | t => t) +val crude_zero_vars = + map_aterms (fn Var ((s, _), T) => Var ((s, 0), T) | t => t) #> map_types (map_type_tvar (fn ((s, _), S) => TVar ((s, 0), S))) fun clasimpset_rule_table_of ctxt = let - fun add loc g f = fold (Termtab.update o rpair loc o g o prop_of o f) - val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> Classical.rep_cs + val thy = Proof_Context.theory_of ctxt + val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy + fun add loc g f = + fold (Termtab.update o rpair loc o g o crude_zero_vars o prop_of o f) + val {safeIs, safeEs, hazIs, hazEs, ...} = + ctxt |> claset_of |> Classical.rep_cs val intros = Item_Net.content safeIs @ Item_Net.content hazIs - val elims = map Classical.classical_rule (Item_Net.content safeEs @ Item_Net.content hazEs) + val elims = + Item_Net.content safeEs @ Item_Net.content hazEs + |> map Classical.classical_rule val simps = ctxt |> simpset_of |> dest_ss |> #simps in Termtab.empty |> add Intro I I intros |> add Elim I I elims |> add Simp I snd simps - |> add Simp normalize_simp_prop snd simps + |> add Simp atomize snd simps end fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths = @@ -833,17 +833,20 @@ fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms val is_chained = member Thm.eq_thm_prop chained_ths val clasimpset_table = clasimpset_rule_table_of ctxt - fun locality_of_theorem global (name: string) th = - if String.isSubstring ".induct" name orelse(*FIXME: use structured name*) + fun locality_of_theorem global name th = + if String.isSubstring ".induct" name orelse (*FIXME: use structured name*) String.isSubstring ".inducts" name then - Induction + Induction else if is_chained th then Chained else if global then case Termtab.lookup clasimpset_table (prop_of th) of SOME loc => loc | NONE => General - else if is_assum th then Assum else Local + else if is_assum th then + Assum + else + Local fun is_good_unnamed_local th = not (Thm.has_name_hint th) andalso forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals diff -r d8c8c2fcab2c -r 866b075aa99b src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Oct 29 13:15:58 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Oct 29 13:15:58 2011 +0200 @@ -659,11 +659,9 @@ arguments ctxt full_proof extra slice_timeout weights ^ " " ^ File.shell_path prob_file val command = "TIMEFORMAT='%3R'; { time " ^ core ^ " ; } 2>&1" - val _ = - atp_problem - |> tptp_lines_for_atp_problem format - |> cons ("% " ^ command ^ "\n") - |> File.write_list prob_file + val _ = atp_problem |> lines_for_atp_problem format + |> cons ("% " ^ command ^ "\n") + |> File.write_list prob_file val conjecture_shape = conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1