# HG changeset patch # User immler@in.tum.de # Date 1244041001 -7200 # Node ID c231efe693ce95b999da60c0e6f07c1a2eaec3d5 # Parent d8537ba165b52d8e3866b916e23a74d1652c4b4a include chain-ths in every prover-call diff -r d8537ba165b5 -r c231efe693ce src/HOL/Tools/atp_wrapper.ML --- a/src/HOL/Tools/atp_wrapper.ML Wed Jun 03 16:56:41 2009 +0200 +++ b/src/HOL/Tools/atp_wrapper.ML Wed Jun 03 16:56:41 2009 +0200 @@ -68,13 +68,13 @@ case axiom_clauses of NONE => relevance_filter goal goal_cls | SOME axcls => axcls - val (thm_names, clauses) = preparer goal_cls the_axiom_clauses thy + val (thm_names, clauses) = preparer goal_cls chain_ths the_axiom_clauses thy val the_const_counts = case const_counts of NONE => ResHolClause.count_constants( case axiom_clauses of NONE => clauses - | SOME axcls => #2(preparer goal_cls (relevance_filter goal goal_cls) thy) + | SOME axcls => #2(preparer goal_cls chain_ths (relevance_filter goal goal_cls) thy) ) | SOME ccs => ccs val _ = writer fname the_const_counts clauses diff -r d8537ba165b5 -r c231efe693ce src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Wed Jun 03 16:56:41 2009 +0200 +++ b/src/HOL/Tools/res_atp.ML Wed Jun 03 16:56:41 2009 +0200 @@ -8,7 +8,7 @@ val type_consts_of_terms : theory -> term list -> string list val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list -> (thm * (string * int)) list - val prepare_clauses : bool -> thm list -> + val prepare_clauses : bool -> thm list -> thm list -> (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> theory -> ResHolClause.axiom_name vector * (ResHolClause.clause list * ResHolClause.clause list * ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list) @@ -403,23 +403,20 @@ fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ Display.string_of_thm th); (* get lemmas from claset, simpset, atpset and extra supplied rules *) -fun get_clasimp_atp_lemmas ctxt user_thms = +fun get_clasimp_atp_lemmas ctxt = let val included_thms = - if include_all - then (tap (fn ths => Output.debug - (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems"))) - (name_thm_pairs ctxt)) - else - let val atpset_thms = - if include_atpset then ResAxioms.atpset_rules_of ctxt - else [] - val _ = (Output.debug (fn () => "ATP theorems: "); app display_thm atpset_thms) - in atpset_thms end - val user_rules = filter check_named - (map ResAxioms.pairname - (if null user_thms then whitelist else user_thms)) + if include_all + then (tap (fn ths => Output.debug + (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems"))) + (name_thm_pairs ctxt)) + else + let val atpset_thms = + if include_atpset then ResAxioms.atpset_rules_of ctxt + else [] + val _ = (Output.debug (fn () => "ATP theorems: "); app display_thm atpset_thms) + in atpset_thms end in - (filter check_named included_thms, user_rules) + filter check_named included_thms end; (***************************************************************) @@ -521,19 +518,20 @@ fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls = let val thy = ProofContext.theory_of ctxt - val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths + val included_thms = get_clasimp_atp_lemmas ctxt val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique |> restrict_to_logic thy (isFO thy goal_cls) |> remove_unwanted_clauses - val white_cls = ResAxioms.cnf_rules_pairs thy white_thms - (*clauses relevant to goal gl*) in - white_cls @ relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls) + relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls) end; (* prepare and count clauses before writing *) -fun prepare_clauses dfg goal_cls axcls thy = +fun prepare_clauses dfg goal_cls chain_ths axcls thy = let + val white_thms = filter check_named (map ResAxioms.pairname (if null chain_ths then whitelist else chain_ths)) + val white_cls = ResAxioms.cnf_rules_pairs thy white_thms + val axcls = white_cls @ axcls val ccls = subtract_cls goal_cls axcls val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls val ccltms = map prop_of ccls diff -r d8537ba165b5 -r c231efe693ce src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Wed Jun 03 16:56:41 2009 +0200 +++ b/src/HOL/Tools/res_reconstruct.ML Wed Jun 03 16:56:41 2009 +0200 @@ -528,6 +528,10 @@ in get_axiom_names thm_names (get_step_nums proofextract) end; + + (*Used to label theorems chained into the sledgehammer call*) + val chained_hint = "CHAINED"; + val nochained = filter_out (fn y => y = chained_hint) (* metis-command *) fun metis_line [] = "apply metis" @@ -536,13 +540,11 @@ (* atp_minimize [atp=] *) fun minimize_line _ [] = "" | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^ - (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^ space_implode " " lemmas) + (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^ + space_implode " " (nochained lemmas)) - (*Used to label theorems chained into the sledgehammer call*) - val chained_hint = "CHAINED"; fun sendback_metis_nochained lemmas = - let val nochained = filter_out (fn y => y = chained_hint) - in (Markup.markup Markup.sendback o metis_line) (nochained lemmas) end + (Markup.markup Markup.sendback o metis_line) (nochained lemmas) fun lemma_list_tstp name result = let val lemmas = extract_lemmas get_step_nums_tstp result in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas end;