# HG changeset patch # User blanchet # Date 1306068661 -7200 # Node ID 0134d6650092f9e02141c1b4c62b9605d5a50927 # Parent c124032ac96fd554ca8e007da4c725a44bcb20f9 added support for remote Waldmeister diff -r c124032ac96f -r 0134d6650092 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Sun May 22 14:50:32 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Sun May 22 14:51:01 2011 +0200 @@ -15,7 +15,7 @@ AConn of connective * ('a, 'b, 'c) formula list | AAtom of 'c - datatype format = UEQ | FOF | TFF + datatype format = CNF_UEQ | FOF | TFF datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = Decl of string * 'a * 'a list * 'a | @@ -23,18 +23,20 @@ * string fo_term option * string fo_term option type 'a problem = (string * 'a problem_line list) list -(* official TPTP syntax *) + (* official TPTP syntax *) val tptp_special_prefix : string val tptp_false : string val tptp_true : string val tptp_tff_type_of_types : string val tptp_tff_bool_type : string val tptp_tff_individual_type : string + val is_atp_variable : string -> bool 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 : format -> string problem -> string list + val filter_cnf_ueq_problem : + (string * string) problem -> (string * string) problem val nice_atp_problem : bool -> ('a * (string * string) problem_line list) list -> ('a * string problem_line list) list @@ -54,7 +56,7 @@ AConn of connective * ('a, 'b, 'c) formula list | AAtom of 'c -datatype format = UEQ | FOF | TFF +datatype format = CNF_UEQ | FOF | TFF datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = Decl of string * 'a * 'a list * 'a | @@ -70,6 +72,8 @@ val tptp_tff_bool_type = "$o" val tptp_tff_individual_type = "$i" +fun is_atp_variable s = Char.isUpper (String.sub (s, 0)) + val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now (* This hash function is recommended in Compilers: Principles, Techniques, and @@ -129,12 +133,11 @@ 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 format - (Formula (ident, kind, phi, source, useful_info)) = - (case format of UEQ => "cnf" | FOF => "fof" | TFF => "tff") ^ + | string_for_problem_line format (Formula (ident, kind, phi, source, info)) = + (case format of CNF_UEQ => "cnf" | FOF => "fof" | TFF => "tff") ^ "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^ string_for_formula format phi ^ ")" ^ - (case (source, useful_info) of + (case (source, info) of (NONE, NONE) => "" | (SOME tm, NONE) => ", " ^ string_for_term tm | (_, SOME tm) => @@ -149,7 +152,37 @@ map (string_for_problem_line format) lines) problem -fun is_atp_variable s = Char.isUpper (String.sub (s, 0)) + +(** CNF UEQ (Waldmeister) **) + +exception LOST_CONJECTURE of unit + +fun is_problem_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true + | is_problem_line_negated _ = false + +fun is_problem_line_cnf_ueq + (Formula (_, _, AAtom (ATerm (("equal", _), _)), _, _)) = true + | is_problem_line_cnf_ueq _ = false + +fun open_formula (AQuant (AForall, _, phi)) = open_formula phi + | open_formula phi = phi +fun open_non_conjecture_line (line as Formula (_, Conjecture, _, _, _)) = line + | open_non_conjecture_line (Formula (ident, kind, phi, source, info)) = + Formula (ident, kind, open_formula phi, source, info) + | open_non_conjecture_line line = line + +fun negate_conjecture_line (Formula (ident, Conjecture, phi, source, info)) = + Formula (ident, Hypothesis, AConn (ANot, [phi]), source, info) + | negate_conjecture_line line = line + +val filter_cnf_ueq_problem = + map (apsnd (map open_non_conjecture_line + #> filter is_problem_line_cnf_ueq + #> map negate_conjecture_line)) + #> (fn problem => + let + val conjs = problem |> maps snd |> filter is_problem_line_negated + in if length conjs = 1 then problem else [] end) (** Nice names **) @@ -178,14 +211,15 @@ problem files. "equal" is reserved by some ATPs. "eq" is reserved to ensure that "HOL.eq" is correctly mapped to equality. *) val reserved_nice_names = ["op", "equal", "eq"] + fun readable_name full_name s = if s = full_name then s else s |> no_qualifiers |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0))) - (* SNARK doesn't like sort (type) names that end with digits. We make - an effort to avoid this here. *) + (* SNARK 20080805r024 doesn't like sort (type) names that end with + digits. We make an effort to avoid this here. *) |> (fn s => if Char.isDigit (String.sub (s, size s - 1)) then s ^ "_" else s) |> (fn s => @@ -209,7 +243,8 @@ val nice_prefix = readable_name full_name desired_name fun add j = let - (* The trailing "_" is for SNARK (cf. comment above). *) + (* The trailing "_" is for SNARK 20080805r024 (see comment + above). *) val nice_name = nice_prefix ^ (if j = 0 then "" else "_" ^ string_of_int j ^ "_") in @@ -240,9 +275,8 @@ ##>> 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 (ident, kind, phi, source, useful_info)) = - nice_formula phi - #>> (fn phi => Formula (ident, kind, phi, source, useful_info)) + | nice_problem_line (Formula (ident, kind, phi, source, info)) = + nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info)) fun nice_problem problem = pool_map (fn (heading, lines) => pool_map nice_problem_line lines #>> pair heading) problem diff -r c124032ac96f -r 0134d6650092 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Sun May 22 14:50:32 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sun May 22 14:51:01 2011 +0200 @@ -413,7 +413,7 @@ remote_atp sine_eN "SInE" ["0.4"] [] [] Axiom Conjecture [FOF] (K (500, ["poly_tags_heavy!", "poly_tags_heavy"]) (* FUDGE *)) val remote_snark = - remote_atp snarkN "SNARK" ["20080805r024"] + remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"] [("refutation.", "end_refutation.")] [] Hypothesis Conjecture [TFF, FOF] (K (250, ["simple"]) (* FUDGE *)) val remote_waldmeister = diff -r c124032ac96f -r 0134d6650092 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 22 14:50:32 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 22 14:51:01 2011 +0200 @@ -9,6 +9,7 @@ signature SLEDGEHAMMER_ATP_TRANSLATE = sig type 'a fo_term = 'a ATP_Problem.fo_term + type format = ATP_Problem.format type formula_kind = ATP_Problem.formula_kind type 'a problem = 'a ATP_Problem.problem type locality = Sledgehammer_Filter.locality @@ -44,8 +45,8 @@ Proof.context -> bool -> (string * locality) * thm -> translated_formula option * ((string * locality) * thm) val prepare_atp_problem : - Proof.context -> formula_kind -> formula_kind -> type_system -> bool - -> term list -> term + Proof.context -> format -> formula_kind -> formula_kind -> type_system + -> bool -> term list -> term -> (translated_formula option * ((string * 'a) * thm)) list -> string problem * string Symtab.table * int * int * (string * 'a) list vector * int list * int Symtab.table @@ -908,8 +909,8 @@ | Simp => simp_info | _ => NONE) -fun formula_line_for_class_rel_clause (ClassRelClause {name, subclass, - superclass, ...}) = +fun formula_line_for_class_rel_clause + (ClassRelClause {name, subclass, superclass, ...}) = let val ty_arg = ATerm (`I "T", []) in Formula (class_rel_clause_prefix ^ ascii_of name, Axiom, AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), @@ -922,8 +923,8 @@ | fo_literal_from_arity_literal (TVarLit (c, sort)) = (false, ATerm (c, [ATerm (sort, [])])) -fun formula_line_for_arity_clause (ArityClause {name, prem_lits, concl_lits, - ...}) = +fun formula_line_for_arity_clause + (ArityClause {name, prem_lits, concl_lits, ...}) = Formula (arity_clause_prefix ^ ascii_of name, Axiom, mk_ahorn (map (formula_from_fo_literal o apfst not o fo_literal_from_arity_literal) prem_lits) @@ -935,8 +936,8 @@ ({name, kind, combformula, ...} : translated_formula) = Formula (conjecture_prefix ^ name, kind, formula_from_combformula ctxt nonmono_Ts type_sys - is_var_nonmonotonic_in_formula false - (close_combformula_universally combformula) + is_var_nonmonotonic_in_formula false + (close_combformula_universally combformula) |> close_formula_universally, NONE, NONE) fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) = @@ -1183,6 +1184,11 @@ level = Nonmonotonic_Types orelse level = Finite_Types | should_add_ti_ti_helper _ = false +fun offset_of_heading_in_problem _ [] j = j + | offset_of_heading_in_problem needle ((heading, lines) :: problem) j = + if heading = needle then j + else offset_of_heading_in_problem needle problem (j + length lines) + val type_declsN = "Types" val sym_declsN = "Symbol types" val factsN = "Relevant facts" @@ -1192,13 +1198,8 @@ val conjsN = "Conjectures" val free_typesN = "Type variables" -fun offset_of_heading_in_problem _ [] j = j - | offset_of_heading_in_problem needle ((heading, lines) :: problem) j = - if heading = needle then j - else offset_of_heading_in_problem needle problem (j + length lines) - -fun prepare_atp_problem ctxt conj_sym_kind prem_kind type_sys explicit_apply - hyp_ts concl_t facts = +fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys + explicit_apply hyp_ts concl_t facts = let val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = translate_formulas ctxt prem_kind type_sys hyp_ts concl_t facts @@ -1223,7 +1224,10 @@ val helper_lines = map (formula_line_for_fact ctxt helper_prefix lavish_nonmono_Ts type_sys) (0 upto length helpers - 1 ~~ helpers) - |> should_add_ti_ti_helper type_sys ? cons (ti_ti_helper_fact ()) + |> (if should_add_ti_ti_helper type_sys then + cons (ti_ti_helper_fact ()) + else + I) (* Reordering these might confuse the proof reconstruction code or the SPASS Flotter hack. *) val problem = @@ -1243,6 +1247,8 @@ cons (type_declsN, map decl_line_for_tff_type (tff_types_in_problem problem)) | _ => I) + val problem = + problem |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I) val (problem, pool) = problem |> nice_atp_problem (Config.get ctxt readable_names) val helpers_offset = offset_of_heading_in_problem helpersN problem 0 diff -r c124032ac96f -r 0134d6650092 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 22 14:50:32 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 22 14:51:01 2011 +0200 @@ -413,8 +413,15 @@ (* We could return (TFF, type_sys) in all cases but this would require the TFF provers to accept problems in which constants are implicitly declared. Today neither SNARK nor ToFoF-E satisfy this criterion. *) - if member (op =) formats FOF then (FOF, type_sys) - else (TFF, Simple_Types All_Types) + if member (op =) formats FOF then + (FOF, type_sys) + else if member (op =) formats CNF_UEQ then + (CNF_UEQ, case type_sys of + Tags _ => type_sys + | _ => Preds (polymorphism_of_type_sys type_sys, + Const_Arg_Types, Light)) + else + (TFF, Simple_Types All_Types) fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) = adjust_dumb_type_sys formats type_sys | determine_format_and_type_sys best_type_systems formats @@ -535,8 +542,8 @@ () val (atp_problem, pool, conjecture_offset, facts_offset, fact_names, typed_helpers, sym_tab) = - prepare_atp_problem ctxt conj_sym_kind prem_kind type_sys - explicit_apply hyp_ts concl_t facts + prepare_atp_problem ctxt format conj_sym_kind prem_kind + type_sys explicit_apply hyp_ts concl_t facts fun weights () = atp_problem_weights atp_problem val core = File.shell_path command ^ " " ^ diff -r c124032ac96f -r 0134d6650092 src/HOL/ex/tptp_export.ML --- a/src/HOL/ex/tptp_export.ML Sun May 22 14:50:32 2011 +0200 +++ b/src/HOL/ex/tptp_export.ML Sun May 22 14:51:01 2011 +0200 @@ -104,8 +104,9 @@ Sledgehammer_ATP_Translate.Heavy) val explicit_apply = false val (atp_problem, _, _, _, _, _, _) = - Sledgehammer_ATP_Translate.prepare_atp_problem ctxt ATP_Problem.Axiom - ATP_Problem.Axiom type_sys explicit_apply [] @{prop False} facts + Sledgehammer_ATP_Translate.prepare_atp_problem ctxt ATP_Problem.FOF + ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply [] + @{prop False} facts val infers = facts0 |> map (fn (_, (_, th)) => (fact_name_of (Thm.get_name_hint th),