# HG changeset patch # User blanchet # Date 1306852716 -7200 # Node ID 93ec303e19173e50723692002e651a2b0635fd9a # Parent b0b30df60056772828c49c0d47a0a2826cea9eab more work on new metis that exploits the powerful new type encodings diff -r b0b30df60056 -r 93ec303e1917 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue May 31 16:38:36 2011 +0200 @@ -17,7 +17,7 @@ datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type - datatype format = CNF_UEQ | FOF | TFF | THF + datatype format = CNF | CNF_UEQ | FOF | TFF | THF datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = Decl of string * 'a * 'a ho_type | @@ -71,6 +71,8 @@ val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula val is_format_typed : format -> bool val tptp_strings_for_atp_problem : format -> string problem -> string list + val ensure_cnf_problem : + (string * string) problem -> (string * string) problem val filter_cnf_ueq_problem : (string * string) problem -> (string * string) problem val declare_undeclared_syms_in_atp_problem : @@ -99,7 +101,7 @@ datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type -datatype format = CNF_UEQ | FOF | TFF | THF +datatype format = CNF | CNF_UEQ | FOF | TFF | THF datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = Decl of string * 'a * 'a ho_type | @@ -256,7 +258,8 @@ val default_source = ATerm ("inference", ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", []))) -fun string_for_format CNF_UEQ = tptp_cnf +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 @@ -306,6 +309,8 @@ Formula (ident, Hypothesis, mk_anot phi, source, info) | negate_conjecture_line line = line +fun ensure_cnf_problem problem = problem |> map (apsnd (map open_formula_line)) + fun filter_cnf_ueq_problem problem = problem |> map (apsnd (map open_formula_line diff -r b0b30df60056 -r 93ec303e1917 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200 @@ -52,7 +52,6 @@ type translated_formula - val readable_names : bool Config.T val type_tag_name : string val bound_var_prefix : string val schematic_var_prefix: string @@ -113,7 +112,7 @@ val type_consts_of_terms : theory -> term list -> string list val prepare_atp_problem : Proof.context -> format -> formula_kind -> formula_kind -> type_system - -> bool option -> term list -> term + -> bool option -> 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 @@ -144,13 +143,6 @@ val elim_info = useful_isabelle_info "elim" val simp_info = useful_isabelle_info "simp" -(* Readable names are often much shorter, especially if types are mangled in - names. Also, the logic for generating legal SNARK sort names is only - implemented for readable names. Finally, readable names are, well, more - readable. For these reason, they are enabled by default. *) -val readable_names = - Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true) - val type_tag_name = "ti" val bound_var_prefix = "B_" @@ -1734,7 +1726,7 @@ val free_typesN = "Type variables" fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys - explicit_apply hyp_ts concl_t facts = + explicit_apply readable_names hyp_ts concl_t facts = let val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t facts @@ -1781,14 +1773,16 @@ formula_lines_for_free_types format type_sys (facts @ conjs))] val problem = problem - |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I) + |> (case format of + CNF => ensure_cnf_problem + | CNF_UEQ => filter_cnf_ueq_problem + | _ => I) |> (if is_format_typed format then declare_undeclared_syms_in_atp_problem type_decl_prefix implicit_declsN else I) - val (problem, pool) = - problem |> nice_atp_problem (Config.get ctxt readable_names) + val (problem, pool) = problem |> nice_atp_problem readable_names val helpers_offset = offset_of_heading_in_problem helpersN problem 0 val typed_helpers = map_filter (fn (j, {name, ...}) => diff -r b0b30df60056 -r 93ec303e1917 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue May 31 16:38:36 2011 +0200 @@ -401,7 +401,7 @@ fun resolve_inf ctxt mode skolem_params thpairs atm th1 th2 = let val thy = Proof_Context.theory_of ctxt - val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 + val (i_th1, i_th2) = pairself (lookth thpairs) (th1, th2) val _ = trace_msg ctxt (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) val _ = trace_msg ctxt (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) in @@ -521,6 +521,7 @@ | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1 (*if not equality, ignore head to skip the hBOOL predicate*) | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*) + | path_finder New tm ps t = path_finder HO tm ps t (* ### *) fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx = let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm in (tm, nt $ tm_rslt) end diff -r b0b30df60056 -r 93ec303e1917 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue May 31 16:38:36 2011 +0200 @@ -78,18 +78,14 @@ (Thm.get_name_hint th, Meson_Clausify.cnf_axiom ctxt new_skolemizer j th)) (0 upto length ths0 - 1) ths0 - val thss = map (snd o snd) th_cls_pairs + val ths = maps (snd o snd) th_cls_pairs val dischargers = map (fst o snd) th_cls_pairs val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") - val _ = app (app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th))) thss - val (mode, {axioms, tfrees, old_skolems}) = - prepare_metis_problem ctxt mode cls thss - val _ = if null tfrees then () - else (trace_msg ctxt (fn () => "TFREE CLAUSES"); - app (fn TyLitFree ((s, _), (s', _)) => - trace_msg ctxt (fn () => s ^ "(" ^ s' ^ ")")) tfrees) + val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths + val (mode, {axioms, old_skolems, ...}) = + prepare_metis_problem ctxt mode cls ths val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS") val thms = map #1 axioms val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms diff -r b0b30df60056 -r 93ec303e1917 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200 @@ -25,12 +25,13 @@ val reveal_old_skolem_terms : (string * term) list -> term -> term val string_of_mode : mode -> string val prepare_metis_problem : - Proof.context -> mode -> thm list -> thm list list -> mode * metis_problem + Proof.context -> mode -> thm list -> thm list -> mode * metis_problem end structure Metis_Translate : METIS_TRANSLATE = struct +open ATP_Problem open ATP_Translate val metis_generated_var_prefix = "_" @@ -282,21 +283,54 @@ val class_rel_clauses = make_class_rel_clauses thy subs supers' in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses end +fun metis_name_from_atp s = + if is_tptp_equal s then "=" + else if s = predicator_name then "{}" + else if s = app_op_name then "." + else s +fun metis_term_from_atp (ATerm (s, tms)) = + if is_tptp_variable s then Metis_Term.Var s + else Metis_Term.Fn (metis_name_from_atp s, map metis_term_from_atp tms) +fun metis_atom_from_atp (AAtom (ATerm (s, tms))) = + (metis_name_from_atp s, map metis_term_from_atp tms) + | metis_atom_from_atp _ = raise Fail "not CNF -- expected atom" +fun metis_literal_from_atp (AConn (ANot, [phi])) = + (false, metis_atom_from_atp phi) + | metis_literal_from_atp phi = (true, metis_atom_from_atp phi) +fun metis_literals_from_atp (AConn (AOr, [phi1, phi2])) = + uncurry (union (op =)) (pairself metis_literals_from_atp (phi1, phi2)) + | metis_literals_from_atp phi = [metis_literal_from_atp phi] +fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) = + let val j = ident |> unprefix conjecture_prefix |> Int.fromString |> the in + (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList + |> Metis_Thm.axiom, + Meson.make_meta_clause (nth clauses j)) + end + | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula" + (* Function to generate metis clauses, including comb and type clauses *) -fun prepare_metis_problem ctxt New conj_clauses fact_clausess = +fun prepare_metis_problem ctxt New conj_clauses fact_clauses = let - val x = 1 - in - error "Not implemented yet" - end - | prepare_metis_problem ctxt mode conj_clauses fact_clausess = + val type_sys = Preds (Polymorphic, (* Nonmonotonic_Types FIXME ### *) No_Types, Light) + val explicit_apply = NONE + val clauses = conj_clauses @ fact_clauses + val (atp_problem, pool, _, _, _, _, sym_tab) = + prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys + explicit_apply false (map prop_of clauses) + @{prop False} [] + (* val _ = tracing (PolyML.makestring atp_problem) FIXME ### *) + val axioms = + atp_problem + |> maps (map_filter (try (metis_axiom_from_atp clauses)) o snd) + in (New, {axioms = axioms, tfrees = [], old_skolems = [] (* FIXME ### *)}) end + | prepare_metis_problem ctxt mode conj_clauses fact_clauses = let val thy = Proof_Context.theory_of ctxt (* The modes FO and FT are sticky. HO can be downgraded to FO. *) val mode = if mode = HO andalso forall (forall (is_quasi_fol_clause thy)) - (conj_clauses :: fact_clausess) then + [conj_clauses, fact_clauses] then FO else mode @@ -321,7 +355,7 @@ {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []} |> fold (add_thm true o `Meson.make_meta_clause) conj_clauses |> add_tfrees - |> fold (fold (add_thm false o `Meson.make_meta_clause)) fact_clausess + |> fold (add_thm false o `Meson.make_meta_clause) fact_clauses val clause_lists = map (Metis_Thm.clause o #1) (#axioms problem) fun is_used c = exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists @@ -343,8 +377,7 @@ if needs_full_types andalso mode <> FT then [] else map prepare_helper thms) in problem |> fold (add_thm false) helper_ths end - val type_ths = - type_ext thy (maps (map prop_of) (conj_clauses :: fact_clausess)) + val type_ths = type_ext thy (map prop_of (conj_clauses @ fact_clauses)) in (mode, fold add_type_thm type_ths problem) end end; diff -r b0b30df60056 -r 93ec303e1917 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 31 16:38:36 2011 +0200 @@ -63,6 +63,10 @@ type prover = params -> (string -> minimize_command) -> prover_problem -> prover_result + val dest_dir : string Config.T + val problem_prefix : string Config.T + val measure_run_time : bool Config.T + val atp_readable_names : bool Config.T val smt_triggers : bool Config.T val smt_weights : bool Config.T val smt_weight_min_facts : int Config.T @@ -90,9 +94,6 @@ val atp_relevance_fudge : relevance_fudge val smt_relevance_fudge : relevance_fudge val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge - val dest_dir : string Config.T - val problem_prefix : string Config.T - val measure_run_time : bool Config.T val weight_smt_fact : Proof.context -> int -> ((string * locality) * thm) * int -> (string * locality) * (int option * thm) @@ -335,16 +336,20 @@ (* configuration attributes *) +(* Empty string means create files in Isabelle's temporary files directory. *) val dest_dir = Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "") - (* Empty string means create files in Isabelle's temporary files directory. *) - val problem_prefix = Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob") - val measure_run_time = Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false) +(* In addition to being easier to read, readable names are often much shorter, + especially if types are mangled in names. For these reason, they are enabled + by default. *) +val atp_readable_names = + Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true) + val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true) val smt_weights = @@ -661,7 +666,8 @@ val (atp_problem, pool, conjecture_offset, facts_offset, fact_names, typed_helpers, sym_tab) = prepare_atp_problem ctxt format conj_sym_kind prem_kind - type_sys explicit_apply hyp_ts concl_t facts + type_sys explicit_apply + (Config.get ctxt atp_readable_names) hyp_ts concl_t facts fun weights () = atp_problem_weights atp_problem val core = File.shell_path command ^ " " ^