# HG changeset patch # User blanchet # Date 1304681699 -7200 # Node ID e7af132d48fe1f455c2cba38fb9cbf74df53a7ce # Parent b6a18a14cc5c735b793711056324ddae38e572d2 allow each prover to specify its own formula kind for symbols occurring in the conjecture diff -r b6a18a14cc5c -r e7af132d48fe src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Fri May 06 13:34:59 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Fri May 06 13:34:59 2011 +0200 @@ -23,13 +23,11 @@ * 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 : - formula_kind -> format -> string problem -> string list + val tptp_strings_for_atp_problem : format -> string problem -> string list val nice_atp_problem : bool -> ('a * (string * string) problem_line list) list -> ('a * string problem_line list) list @@ -49,8 +47,6 @@ AConn of connective * ('a, 'b, 'c) formula list | AAtom of 'c -fun mk_anot phi = AConn (ANot, [phi]) - datatype format = Fof | Tff datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = @@ -114,35 +110,27 @@ val default_source = ATerm ("inference", ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", []))) -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 hypothesis_kind format + | string_for_problem_line format (Formula (ident, kind, phi, source, useful_info)) = - let - val (kind, phi) = - if kind = Hypothesis then - (hypothesis_kind, phi |> hypothesis_kind = Conjecture ? mk_anot) - else - (kind, phi) - in - (case format of Fof => "fof" | Tff => "tff") ^ - "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^ - string_for_formula phi ^ ")" ^ - (case (source, useful_info) of - (NONE, NONE) => "" - | (SOME tm, NONE) => ", " ^ string_for_term tm - | (_, SOME tm) => - ", " ^ string_for_term (source |> the_default default_source) ^ - ", " ^ string_for_term tm) ^ ").\n" - end -fun tptp_strings_for_atp_problem hypothesis_kind format problem = + (case format of Fof => "fof" | Tff => "tff") ^ + "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^ + string_for_formula phi ^ ")" ^ + (case (source, useful_info) of + (NONE, NONE) => "" + | (SOME tm, NONE) => ", " ^ string_for_term tm + | (_, SOME tm) => + ", " ^ string_for_term (source |> the_default default_source) ^ + ", " ^ string_for_term tm) ^ ").\n" +fun tptp_strings_for_atp_problem 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 hypothesis_kind format) lines) + map (string_for_problem_line format) lines) problem fun is_atp_variable s = Char.isUpper (String.sub (s, 0)) diff -r b6a18a14cc5c -r e7af132d48fe src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Fri May 06 13:34:59 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri May 06 13:34:59 2011 +0200 @@ -19,7 +19,8 @@ -> string, proof_delims : (string * string) list, known_failures : (failure * string) list, - hypothesis_kind : formula_kind, + conj_sym_kind : formula_kind, + prem_kind : formula_kind, formats : format list, best_slices : Proof.context -> (real * (bool * int)) list, best_type_systems : string list} @@ -41,7 +42,7 @@ val remote_prefix : string val remote_atp : string -> string -> string list -> (string * string) list - -> (failure * string) list -> formula_kind -> format list + -> (failure * string) list -> formula_kind -> formula_kind -> format list -> (Proof.context -> int) -> string list -> string * atp_config val add_atp : string * atp_config -> theory -> theory val get_atp : theory -> string -> atp_config @@ -67,7 +68,8 @@ -> string, proof_delims : (string * string) list, known_failures : (failure * string) list, - hypothesis_kind : formula_kind, + conj_sym_kind : formula_kind, + prem_kind : formula_kind, formats : format list, best_slices : Proof.context -> (real * (bool * int)) list, best_type_systems : string list} @@ -201,7 +203,8 @@ "# Cannot determine problem status within resource limit"), (OutOfResources, "SZS status: ResourceOut"), (OutOfResources, "SZS status ResourceOut")], - hypothesis_kind = Conjecture, + conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *) + prem_kind = Conjecture, formats = [Fof], best_slices = fn ctxt => if effective_e_weight_method ctxt = e_slicesN then @@ -239,7 +242,8 @@ (MalformedInput, "Free Variable"), (SpassTooOld, "tptp2dfg"), (InternalError, "Please report this error")], - hypothesis_kind = Conjecture, + conj_sym_kind = Axiom, (* FIXME: try out Hypothesis *) + prem_kind = Conjecture, formats = [Fof], best_slices = K [(0.66667, (false, 150 (* FUDGE *))) (* with SOS *), @@ -276,7 +280,8 @@ (Unprovable, "Termination reason: Satisfiable"), (VampireTooOld, "not a valid option"), (Interrupted, "Aborted by signal SIGINT")], - hypothesis_kind = Conjecture, + conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *) + prem_kind = Conjecture, formats = [Fof], best_slices = K [(0.66667, (false, 450 (* FUDGE *))) (* with SOS *), @@ -301,7 +306,8 @@ (IncompleteUnprovable, "SZS status Satisfiable"), (ProofMissing, "\nunsat"), (ProofMissing, "SZS status Unsatisfiable")], - hypothesis_kind = Hypothesis, + conj_sym_kind = Hypothesis, + prem_kind = Hypothesis, formats = [Fof], best_slices = K [(1.0, (false, 250 (* FUDGE *)))], best_type_systems = [] (* FIXME *)} @@ -342,8 +348,8 @@ val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *) fun remote_config system_name system_versions proof_delims known_failures - hypothesis_kind formats best_max_relevant best_type_systems - : atp_config = + conj_sym_kind prem_kind formats best_max_relevant + best_type_systems : atp_config = {exec = ("ISABELLE_ATP", "scripts/remote_atp"), required_execs = [], arguments = fn _ => fn _ => fn timeout => fn _ => @@ -355,7 +361,8 @@ [(IncompleteUnprovable, "says Unknown"), (IncompleteUnprovable, "says GaveUp"), (TimedOut, "says Timeout")], - hypothesis_kind = hypothesis_kind, + conj_sym_kind = conj_sym_kind, + prem_kind = prem_kind, formats = formats, best_slices = fn ctxt => [(1.0, (false, best_max_relevant ctxt))], best_type_systems = best_type_systems} @@ -363,18 +370,18 @@ fun int_average f xs = fold (Integer.add o f) xs 0 div length xs fun remotify_config system_name system_versions - ({proof_delims, known_failures, hypothesis_kind, formats, - best_slices, best_type_systems, ...} : atp_config) - : atp_config = + ({proof_delims, known_failures, conj_sym_kind, prem_kind, formats, + best_slices, best_type_systems, ...} : atp_config) : atp_config = remote_config system_name system_versions proof_delims known_failures - hypothesis_kind formats (int_average (snd o snd) o best_slices) - best_type_systems + conj_sym_kind prem_kind formats + (int_average (snd o snd) o best_slices) best_type_systems fun remote_atp name system_name system_versions proof_delims known_failures - hypothesis_kind formats best_max_relevant best_type_systems = + conj_sym_kind prem_kind formats best_max_relevant best_type_systems = (remote_prefix ^ name, remote_config system_name system_versions proof_delims known_failures - hypothesis_kind formats best_max_relevant best_type_systems) + conj_sym_kind prem_kind formats best_max_relevant + best_type_systems) fun remotify_atp (name, config) system_name system_versions = (remote_prefix ^ name, remotify_config system_name system_versions config) @@ -383,14 +390,14 @@ 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) - Conjecture [Tff] (K 200 (* FUDGE *)) ["simple"] + Axiom Conjecture [Tff] (K 200 (* FUDGE *)) ["simple"] val remote_sine_e = - remote_atp sine_eN "SInE" ["0.4"] [] [] Conjecture [Fof] (K 500 (* FUDGE *)) - ["args", "preds", "tags"] + remote_atp sine_eN "SInE" ["0.4"] [] [] Axiom Conjecture [Fof] + (K 500 (* FUDGE *)) ["args", "preds", "tags"] val remote_snark = remote_atp snarkN "SNARK" ["20080805r024"] - [("refutation.", "end_refutation.")] [] Conjecture [Tff, Fof] - (K 250 (* FUDGE *)) ["simple"] + [("refutation.", "end_refutation.")] [] Hypothesis Conjecture + [Tff, Fof] (K 250 (* FUDGE *)) ["simple"] (* Setup *) diff -r b6a18a14cc5c -r e7af132d48fe src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 06 13:34:59 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 06 13:34:59 2011 +0200 @@ -9,6 +9,7 @@ signature SLEDGEHAMMER_ATP_TRANSLATE = sig type 'a fo_term = 'a ATP_Problem.fo_term + type formula_kind = ATP_Problem.formula_kind type 'a problem = 'a ATP_Problem.problem type locality = Sledgehammer_Filter.locality @@ -41,7 +42,8 @@ Proof.context -> bool -> (string * locality) * thm -> translated_formula option * ((string * locality) * thm) val prepare_atp_problem : - Proof.context -> type_system -> bool -> term list -> term + Proof.context -> 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 @@ -215,6 +217,7 @@ |> 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 @@ -452,10 +455,21 @@ NONE | (_, formula) => SOME formula -fun make_conjecture ctxt ts = +fun make_conjecture ctxt prem_kind ts = let val last = length ts - 1 in - map2 (fn j => make_formula ctxt true true (string_of_int j) Chained - (if j = last then Conjecture else Hypothesis)) + map2 (fn j => fn t => + let + val (kind, maybe_negate) = + if j = last then + (Conjecture, I) + else + (prem_kind, + if prem_kind = Conjecture then update_combformula mk_anot + else I) + in + make_formula ctxt true true (string_of_int j) Chained kind t + |> maybe_negate + end) (0 upto last) ts end @@ -750,7 +764,7 @@ fun translate_atp_fact ctxt keep_trivial = `(make_fact ctxt keep_trivial true true o apsnd prop_of) -fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts = +fun translate_formulas ctxt prem_kind type_sys hyp_ts concl_t rich_facts = let val thy = Proof_Context.theory_of ctxt val fact_ts = map (prop_of o snd o snd) rich_facts @@ -767,7 +781,7 @@ val subs = tfree_classes_of_terms all_ts val supers = tvar_classes_of_terms all_ts val tycons = type_consts_of_terms thy all_ts - val conjs = make_conjecture ctxt (hyp_ts @ [concl_t]) + val conjs = make_conjecture ctxt prem_kind (hyp_ts @ [concl_t]) val (supers', arity_clauses) = if level_of_type_sys type_sys = No_Types then ([], []) else make_arity_clauses thy tycons supers @@ -985,9 +999,12 @@ fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false -fun formula_line_for_sym_decl ctxt nonmono_Ts type_sys n s j +fun formula_line_for_sym_decl ctxt conj_sym_kind nonmono_Ts type_sys n s j (s', T_args, T, _, ary, in_conj) = let + val (kind, maybe_negate) = + if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot) + else (Axiom, I) val (arg_Ts, res_T) = n_ary_strip_type ary T val bound_names = 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int) @@ -998,18 +1015,19 @@ else NONE) in Formula (sym_decl_prefix ^ s ^ - (if n > 1 then "_" ^ string_of_int j else ""), - if in_conj then Hypothesis else Axiom, + (if n > 1 then "_" ^ string_of_int j else ""), kind, CombConst ((s, s'), T, T_args) |> fold (curry (CombApp o swap)) bound_tms |> type_pred_combatom ctxt nonmono_Ts type_sys res_T |> mk_aquant AForall (bound_names ~~ bound_Ts) |> formula_from_combformula ctxt nonmono_Ts type_sys - |> close_formula_universally, + |> close_formula_universally + |> maybe_negate, NONE, NONE) end -fun problem_lines_for_sym_decls ctxt nonmono_Ts type_sys (s, decls) = +fun problem_lines_for_sym_decls ctxt conj_sym_kind nonmono_Ts type_sys + (s, decls) = case type_sys of Simple _ => map (decl_line_for_sym s) decls | _ => @@ -1030,13 +1048,15 @@ decls |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys o result_type_of_decl) in - map2 (formula_line_for_sym_decl ctxt nonmono_Ts type_sys n s) - (0 upto length decls - 1) decls + (0 upto length decls - 1, decls) + |-> map2 (formula_line_for_sym_decl ctxt conj_sym_kind nonmono_Ts type_sys + n s) end -fun problem_lines_for_sym_decl_table ctxt nonmono_Ts type_sys sym_decl_tab = - Symtab.fold_rev (append o problem_lines_for_sym_decls ctxt nonmono_Ts - type_sys) +fun problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys + sym_decl_tab = + Symtab.fold_rev (append o problem_lines_for_sym_decls ctxt conj_sym_kind + nonmono_Ts type_sys) sym_decl_tab [] fun add_tff_types_in_formula (AQuant (_, xs, phi)) = @@ -1070,10 +1090,11 @@ if heading = needle then j else offset_of_heading_in_problem needle problem (j + length lines) -fun prepare_atp_problem ctxt type_sys explicit_apply hyp_ts concl_t facts = +fun prepare_atp_problem ctxt 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 type_sys hyp_ts concl_t facts + translate_formulas ctxt prem_kind type_sys hyp_ts concl_t facts val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply val nonmono_Ts = [] |> fold (add_nonmonotonic_types_for_facts ctxt type_sys) [facts, conjs] @@ -1085,7 +1106,7 @@ val sym_decl_lines = (conjs, facts) (* FIXME: what if "True_or_False" is among helpers? *) |> sym_decl_table_for_facts type_sys repaired_sym_tab - |> problem_lines_for_sym_decl_table ctxt nonmono_Ts type_sys + |> problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys (* Reordering these might confuse the proof reconstruction code or the SPASS Flotter hack. *) val problem = diff -r b6a18a14cc5c -r e7af132d48fe src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 06 13:34:59 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 06 13:34:59 2011 +0200 @@ -364,8 +364,8 @@ fun run_atp auto name ({exec, required_execs, arguments, proof_delims, known_failures, - hypothesis_kind, formats, best_slices, best_type_systems, ...} - : atp_config) + conj_sym_kind, prem_kind, formats, best_slices, best_type_systems, + ...} : atp_config) ({debug, verbose, overlord, type_sys, max_relevant, monomorphize_limit, explicit_apply, isar_proof, isar_shrink_factor, slicing, timeout, ...} : params) @@ -470,8 +470,8 @@ () val (atp_problem, pool, conjecture_offset, facts_offset, fact_names) = - prepare_atp_problem ctxt type_sys explicit_apply hyp_ts - concl_t facts + prepare_atp_problem ctxt 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 ^ " " ^ @@ -484,7 +484,7 @@ "exec " ^ core) ^ " 2>&1" val _ = atp_problem - |> tptp_strings_for_atp_problem hypothesis_kind format + |> tptp_strings_for_atp_problem format |> cons ("% " ^ command ^ "\n") |> File.write_list prob_file val conjecture_shape = diff -r b6a18a14cc5c -r e7af132d48fe src/HOL/ex/tptp_export.ML --- a/src/HOL/ex/tptp_export.ML Fri May 06 13:34:59 2011 +0200 +++ b/src/HOL/ex/tptp_export.ML Fri May 06 13:34:59 2011 +0200 @@ -104,8 +104,8 @@ else Sledgehammer_ATP_Translate.Const_Arg_Types) val explicit_apply = false val (atp_problem, _, _, _, _) = - Sledgehammer_ATP_Translate.prepare_atp_problem ctxt type_sys - explicit_apply [] @{prop False} facts + Sledgehammer_ATP_Translate.prepare_atp_problem ctxt 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), @@ -114,8 +114,7 @@ infers |> map (apsnd (filter (member (op = o apsnd fst) infers))) val atp_problem = atp_problem |> add_inferences_to_problem infers val ss = - ATP_Problem.tptp_strings_for_atp_problem ATP_Problem.Hypothesis - ATP_Problem.Fof atp_problem + ATP_Problem.tptp_strings_for_atp_problem ATP_Problem.Fof atp_problem val _ = app (File.append path) ss in () end