# HG changeset patch # User blanchet # Date 1304267845 -7200 # Node ID 78414ec6fa4e7c2854138496173b84f93987c76f # Parent a8a80a2a34be4d078b5b5065e21eb412c528d5ce made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support diff -r a8a80a2a34be -r 78414ec6fa4e src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Sun May 01 18:37:25 2011 +0200 @@ -15,20 +15,21 @@ AConn of connective * ('a, 'b, 'c) formula list | AAtom of 'c - datatype logic = Fof | Tff + datatype format = Fof | Tff datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = Decl of string * 'a * 'a list * 'a | - Formula of logic * string * formula_kind * ('a, 'a, 'a fo_term) formula + Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula * string fo_term option * string fo_term option type 'a problem = (string * 'a problem_line list) list + val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula val timestamp : unit -> string val hashw : word * word -> word val hashw_string : string * word -> word val is_atp_variable : string -> bool val tptp_strings_for_atp_problem : - bool -> (string * string problem_line list) list -> string list + formula_kind -> format -> string problem -> string list val nice_atp_problem : bool -> ('a * (string * string) problem_line list) list -> ('a * string problem_line list) list @@ -48,11 +49,13 @@ AConn of connective * ('a, 'b, 'c) formula list | AAtom of 'c -datatype logic = Fof | Tff +fun mk_anot phi = AConn (ANot, [phi]) + +datatype format = Fof | Tff datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = Decl of string * 'a * 'a list * 'a | - Formula of logic * string * formula_kind * ('a, 'a, 'a fo_term) formula + Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula * string fo_term option * string fo_term option type 'a problem = (string * 'a problem_line list) list @@ -108,19 +111,19 @@ | string_for_symbol_type arg_tys res_ty = string_for_symbol_type ["(" ^ space_implode " * " arg_tys ^ ")"] res_ty -fun string_for_problem_line _ (Decl (ident, sym, arg_tys, res_ty)) = +fun string_for_problem_line _ _ (Decl (ident, sym, arg_tys, res_ty)) = "tff(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^ string_for_symbol_type arg_tys res_ty ^ ").\n" - | string_for_problem_line use_conjecture_for_hypotheses - (Formula (logic, ident, kind, phi, source, useful_info)) = + | string_for_problem_line hypothesis_kind format + (Formula (ident, kind, phi, source, useful_info)) = let val (kind, phi) = - if kind = Hypothesis andalso use_conjecture_for_hypotheses then - (Conjecture, AConn (ANot, [phi])) + if kind = Hypothesis then + (hypothesis_kind, phi |> hypothesis_kind = Conjecture ? mk_anot) else (kind, phi) in - (case logic of Fof => "fof" | Tff => "tff") ^ + (case format of Fof => "fof" | Tff => "tff") ^ "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^ string_for_formula phi ^ ")" ^ (case (source, useful_info) of @@ -130,13 +133,13 @@ ", " ^ string_for_term (source |> the_default (ATerm ("[]", []))) ^ ", " ^ string_for_term tm) ^ ").\n" end -fun tptp_strings_for_atp_problem use_conjecture_for_hypotheses problem = +fun tptp_strings_for_atp_problem hypothesis_kind format problem = "% This file was generated by Isabelle (most likely Sledgehammer)\n\ \% " ^ timestamp () ^ "\n" :: maps (fn (_, []) => [] | (heading, lines) => "\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" :: - map (string_for_problem_line use_conjecture_for_hypotheses) lines) + map (string_for_problem_line hypothesis_kind format) lines) problem fun is_atp_variable s = Char.isUpper (String.sub (s, 0)) @@ -221,9 +224,9 @@ ##>> pool_map nice_name arg_tys ##>> nice_name res_ty #>> (fn ((sym, arg_tys), res_ty) => Decl (ident, sym, arg_tys, res_ty)) - | nice_problem_line (Formula (logic, ident, kind, phi, source, useful_info)) = + | nice_problem_line (Formula (ident, kind, phi, source, useful_info)) = nice_formula phi - #>> (fn phi => Formula (logic, ident, kind, phi, source, useful_info)) + #>> (fn phi => Formula (ident, kind, phi, source, useful_info)) fun nice_problem problem = pool_map (fn (heading, lines) => pool_map nice_problem_line lines #>> pair heading) problem diff -r a8a80a2a34be -r 78414ec6fa4e src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sun May 01 18:37:25 2011 +0200 @@ -7,6 +7,8 @@ signature ATP_SYSTEMS = sig + type format = ATP_Problem.format + type formula_kind = ATP_Problem.formula_kind type failure = ATP_Proof.failure type atp_config = @@ -16,7 +18,8 @@ slices: unit -> (real * (bool * int)) list, proof_delims: (string * string) list, known_failures: (failure * string) list, - use_conjecture_for_hypotheses: bool} + hypothesis_kind: formula_kind, + formats: format list} datatype e_weight_method = E_Slices | E_Auto | E_Fun_Weight | E_Sym_Offset_Weight @@ -40,7 +43,8 @@ val remote_prefix : string val remote_atp : string -> string -> string list -> (string * string) list - -> (failure * string) list -> (unit -> int) -> bool -> string * atp_config + -> (failure * string) list -> (unit -> int) -> formula_kind -> format list + -> string * atp_config val add_atp : string * atp_config -> theory -> theory val get_atp : theory -> string -> atp_config val supported_atps : theory -> string list @@ -52,6 +56,7 @@ structure ATP_Systems : ATP_SYSTEMS = struct +open ATP_Problem open ATP_Proof (* ATP configuration *) @@ -63,7 +68,8 @@ slices: unit -> (real * (bool * int)) list, proof_delims: (string * string) list, known_failures: (failure * string) list, - use_conjecture_for_hypotheses: bool} + hypothesis_kind: formula_kind, + formats: format list} val known_perl_failures = [(CantConnect, "HTTP error"), @@ -188,7 +194,8 @@ "# Cannot determine problem status within resource limit"), (OutOfResources, "SZS status: ResourceOut"), (OutOfResources, "SZS status ResourceOut")], - use_conjecture_for_hypotheses = true} + hypothesis_kind = Conjecture, + formats = [Fof]} val e = (eN, e_config) @@ -216,7 +223,8 @@ (MalformedInput, "Free Variable"), (SpassTooOld, "tptp2dfg"), (InternalError, "Please report this error")], - use_conjecture_for_hypotheses = true} + hypothesis_kind = Conjecture, + formats = [Fof]} val spass = (spassN, spass_config) @@ -249,7 +257,8 @@ (Unprovable, "Termination reason: Satisfiable"), (VampireTooOld, "not a valid option"), (Interrupted, "Aborted by signal SIGINT")], - use_conjecture_for_hypotheses = true} + hypothesis_kind = Conjecture, + formats = [Fof]} val vampire = (vampireN, vampire_config) @@ -269,7 +278,8 @@ (IncompleteUnprovable, "SZS status Satisfiable"), (ProofMissing, "\nunsat"), (ProofMissing, "SZS status Unsatisfiable")], - use_conjecture_for_hypotheses = false} + hypothesis_kind = Hypothesis, + formats = [Fof]} val z3_atp = (z3_atpN, z3_atp_config) @@ -307,8 +317,7 @@ val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *) fun remote_config system_name system_versions proof_delims known_failures - default_max_relevant use_conjecture_for_hypotheses - : atp_config = + default_max_relevant hypothesis_kind formats : atp_config = {exec = ("ISABELLE_ATP", "scripts/remote_atp"), required_execs = [], arguments = fn _ => fn timeout => fn _ => @@ -320,21 +329,22 @@ known_failures @ known_perl_failures @ [(IncompleteUnprovable, "says Unknown"), (TimedOut, "says Timeout")], - use_conjecture_for_hypotheses = use_conjecture_for_hypotheses} + hypothesis_kind = hypothesis_kind, + formats = formats} fun int_average f xs = fold (Integer.add o f) xs 0 div length xs fun remotify_config system_name system_versions - ({proof_delims, slices, known_failures, use_conjecture_for_hypotheses, - ...} : atp_config) : atp_config = + ({proof_delims, slices, known_failures, hypothesis_kind, + formats, ...} : atp_config) : atp_config = remote_config system_name system_versions proof_delims known_failures - (int_average (snd o snd) o slices) use_conjecture_for_hypotheses + (int_average (snd o snd) o slices) hypothesis_kind formats fun remote_atp name system_name system_versions proof_delims known_failures - default_max_relevant use_conjecture_for_hypotheses = + default_max_relevant hypothesis_kind formats = (remote_prefix ^ name, remote_config system_name system_versions proof_delims known_failures - default_max_relevant use_conjecture_for_hypotheses) + default_max_relevant hypothesis_kind formats) fun remotify_atp (name, config) system_name system_versions = (remote_prefix ^ name, remotify_config system_name system_versions config) @@ -343,12 +353,13 @@ val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"] val remote_tofof_e = remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config) - (K 200 (* FUDGE *)) true + (K 200 (* FUDGE *)) Conjecture [Tff] val remote_sine_e = - remote_atp sine_eN "SInE" ["0.4"] [] [] (K 500 (* FUDGE *)) true + remote_atp sine_eN "SInE" ["0.4"] [] [] (K 500 (* FUDGE *)) Conjecture [Fof] val remote_snark = remote_atp snarkN "SNARK" ["20080805r024"] - [("refutation.", "end_refutation.")] [] (K 250 (* FUDGE *)) true + [("refutation.", "end_refutation.")] [] (K 250 (* FUDGE *)) + Conjecture [Tff, Fof] (* Setup *) diff -r a8a80a2a34be -r 78414ec6fa4e src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:25 2011 +0200 @@ -156,7 +156,6 @@ |> filter (fn TyLitVar _ => kind <> Conjecture | TyLitFree _ => kind = Conjecture) -fun mk_anot phi = AConn (ANot, [phi]) fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) fun mk_aconns c phis = let val (phis', phi') = split_last phis in @@ -532,7 +531,7 @@ fun var s = ATerm (`I s, []) fun tag tm = ATerm (`I type_tag_name, [var "X", tm]) in - Formula (Fof, helper_prefix ^ ascii_of "ti_ti", Axiom, + Formula (helper_prefix ^ ascii_of "ti_ti", Axiom, AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")])) |> close_formula_universally, NONE, NONE) end @@ -690,22 +689,18 @@ (close_combformula_universally combformula)) |> close_formula_universally -fun logic_for_type_sys Many_Typed = Tff - | logic_for_type_sys _ = Fof - (* Each fact is given a unique fact number to avoid name clashes (e.g., because of monomorphization). The TPTP explicitly forbids name clashes, and some of the remote provers might care. *) fun formula_line_for_fact ctxt prefix type_sys (j, formula as {name, kind, ...}) = - Formula (logic_for_type_sys type_sys, - prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind, + Formula (prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind, formula_for_fact ctxt type_sys formula, NONE, NONE) fun formula_line_for_class_rel_clause (ClassRelClause {name, subclass, superclass, ...}) = let val ty_arg = ATerm (`I "T", []) in - Formula (Fof, class_rel_clause_prefix ^ ascii_of name, Axiom, + Formula (class_rel_clause_prefix ^ ascii_of name, Axiom, AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), AAtom (ATerm (superclass, [ty_arg]))]) |> close_formula_universally, NONE, NONE) @@ -718,7 +713,7 @@ fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits, ...}) = - Formula (Fof, arity_clause_prefix ^ ascii_of name, Axiom, + Formula (arity_clause_prefix ^ ascii_of name, Axiom, mk_ahorn (map (formula_from_fo_literal o apfst not o fo_literal_from_arity_literal) premLits) (formula_from_fo_literal @@ -727,7 +722,7 @@ fun formula_line_for_conjecture ctxt type_sys ({name, kind, combformula, ...} : translated_formula) = - Formula (logic_for_type_sys type_sys, conjecture_prefix ^ name, kind, + Formula (conjecture_prefix ^ name, kind, formula_from_combformula ctxt type_sys (close_combformula_universally combformula) |> close_formula_universally, NONE, NONE) @@ -737,7 +732,7 @@ |> map fo_literal_from_type_literal fun formula_line_for_free_type j lit = - Formula (Fof, tfree_prefix ^ string_of_int j, Hypothesis, + Formula (tfree_prefix ^ string_of_int j, Hypothesis, formula_from_fo_literal lit, NONE, NONE) fun formula_lines_for_free_types type_sys facts = let @@ -803,7 +798,7 @@ val freshener = case type_sys of Args _ => string_of_int j ^ "_" | _ => "" in - Formula (Fof, sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom, + Formula (sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom, CombConst ((s, s'), T, T_args) |> fold (curry (CombApp o swap)) bound_tms |> type_pred_combatom type_sys res_T @@ -837,7 +832,7 @@ fun add_tff_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) = union (op =) (res_T :: arg_Ts) - | add_tff_types_in_problem_line (Formula (_, _, _, phi, _, _)) = + | add_tff_types_in_problem_line (Formula (_, _, phi, _, _)) = add_tff_types_in_formula phi fun tff_types_in_problem problem = @@ -914,7 +909,7 @@ fun add_term_weights weight (ATerm (s, tms)) = (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight) #> fold (add_term_weights weight) tms -fun add_problem_line_weights weight (Formula (_, _, _, phi, _, _)) = +fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) = formula_fold (add_term_weights weight) phi | add_problem_line_weights _ _ = I diff -r a8a80a2a34be -r 78414ec6fa4e src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 01 18:37:25 2011 +0200 @@ -340,7 +340,7 @@ fun run_atp auto name ({exec, required_execs, arguments, slices, proof_delims, known_failures, - use_conjecture_for_hypotheses, ...} : atp_config) + hypothesis_kind, ...} : atp_config) ({debug, verbose, overlord, type_sys, max_relevant, monomorphize, monomorphize_limit, explicit_apply, isar_proof, isar_shrink_factor, slicing, timeout, ...} : params) @@ -348,6 +348,7 @@ let val thy = Proof.theory_of state val ctxt = Proof.context_of state + val format = if type_sys = Many_Typed then Tff else Fof val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal val (dest_dir, problem_prefix) = if overlord then overlord_file_location_for_prover name @@ -452,7 +453,7 @@ "exec " ^ core) ^ " 2>&1" val _ = atp_problem - |> tptp_strings_for_atp_problem use_conjecture_for_hypotheses + |> tptp_strings_for_atp_problem hypothesis_kind format |> cons ("% " ^ command ^ "\n") |> File.write_list prob_file val conjecture_shape =