# HG changeset patch # User blanchet # Date 1269856860 -7200 # Node ID 8256d5a185bd7735155e0a7db41e3fda942ca45c # Parent eb44a5d40b9ef673698789f383344db82813abbe added "respect_no_atp" and "convergence" options to Sledgehammer; these were previously hard-coded in "sledgehammer_fact_filter.ML" diff -r eb44a5d40b9e -r 8256d5a185bd src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Sun Mar 28 18:39:27 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Mar 29 12:01:00 2010 +0200 @@ -14,9 +14,10 @@ verbose: bool, atps: string list, full_types: bool, + respect_no_atp: bool, relevance_threshold: real, + convergence: real, higher_order: bool option, - respect_no_atp: bool, follow_defs: bool, isar_proof: bool, timeout: Time.time, @@ -56,15 +57,16 @@ (** parameters, problems, results, and provers **) -(* TODO: "theory_const", "blacklist_filter", "convergence" *) +(* TODO: "theory_const" *) type params = {debug: bool, verbose: bool, atps: string list, full_types: bool, + respect_no_atp: bool, relevance_threshold: real, + convergence: real, higher_order: bool option, - respect_no_atp: bool, follow_defs: bool, isar_proof: bool, timeout: Time.time, diff -r eb44a5d40b9e -r 8256d5a185bd src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Sun Mar 28 18:39:27 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Mon Mar 29 12:01:00 2010 +0200 @@ -159,11 +159,12 @@ fun generic_tptp_prover (name, {command, arguments, failure_strs, max_new_clauses, add_theory_const, supports_isar_proofs}) - (params as {relevance_threshold, higher_order, follow_defs, isar_proof, - ...}) timeout = + (params as {respect_no_atp, relevance_threshold, convergence, + higher_order, follow_defs, isar_proof, ...}) timeout = generic_prover - (get_relevant_facts relevance_threshold higher_order follow_defs - max_new_clauses add_theory_const) + (get_relevant_facts respect_no_atp relevance_threshold convergence + higher_order follow_defs max_new_clauses + add_theory_const) (prepare_clauses higher_order false) write_tptp_file command (arguments timeout) failure_strs (if supports_isar_proofs andalso isar_proof then structured_isar_proof @@ -212,11 +213,12 @@ fun generic_dfg_prover (name, ({command, arguments, failure_strs, max_new_clauses, add_theory_const, ...} : prover_config)) - (params as {relevance_threshold, higher_order, follow_defs, ...}) - timeout = + (params as {respect_no_atp, relevance_threshold, convergence, + higher_order, follow_defs, isar_proof, ...}) timeout = generic_prover - (get_relevant_facts relevance_threshold higher_order follow_defs - max_new_clauses add_theory_const) + (get_relevant_facts respect_no_atp relevance_threshold convergence + higher_order follow_defs max_new_clauses + add_theory_const) (prepare_clauses higher_order true) write_dfg_file command (arguments timeout) failure_strs (metis_lemma_list true) name params; diff -r eb44a5d40b9e -r 8256d5a185bd src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sun Mar 28 18:39:27 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Mar 29 12:01:00 2010 +0200 @@ -18,8 +18,8 @@ val tfree_classes_of_terms : term list -> string list val type_consts_of_terms : theory -> term list -> string list val get_relevant_facts : - real -> bool option -> bool -> int -> bool -> relevance_override - -> Proof.context * (thm list * 'a) -> thm list + bool -> real -> real -> bool option -> bool -> int -> bool + -> relevance_override -> Proof.context * (thm list * 'a) -> thm list -> (thm * (string * int)) list val prepare_clauses : bool option -> bool -> thm list -> thm list -> (thm * (axiom_name * hol_clause_id)) list -> @@ -41,17 +41,6 @@ del: Facts.ref list, only: bool} -(********************************************************************) -(* some settings for both background automatic ATP calling procedure*) -(* and also explicit ATP invocation methods *) -(********************************************************************) - -(*** background linkup ***) -val run_blacklist_filter = true; - -(*** relevance filter parameters ***) -val convergence = 3.2; (*Higher numbers allow longer inference chains*) - (***************************************************************) (* Relevance Filtering *) (***************************************************************) @@ -263,7 +252,7 @@ end end; -fun relevant_clauses ctxt follow_defs max_new +fun relevant_clauses ctxt convergence follow_defs max_new (relevance_override as {add, del, only}) thy ctab p rel_consts = let val add_thms = maps (ProofContext.get_fact ctxt) add @@ -277,8 +266,9 @@ in trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels)); map #1 newrels @ - relevant_clauses ctxt follow_defs max_new relevance_override thy ctab - newp rel_consts' (more_rejects @ rejects) + relevant_clauses ctxt convergence follow_defs max_new + relevance_override thy ctab newp rel_consts' + (more_rejects @ rejects) end | relevant (newrels, rejects) ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) = @@ -298,7 +288,7 @@ relevant ([],[]) end; -fun relevance_filter ctxt relevance_threshold follow_defs max_new +fun relevance_filter ctxt relevance_threshold convergence follow_defs max_new add_theory_const relevance_override thy axioms goals = if relevance_threshold > 0.0 then let @@ -309,8 +299,8 @@ trace_msg (fn () => "Initial constants: " ^ commas (Symtab.keys goal_const_tab)) val relevant = - relevant_clauses ctxt follow_defs max_new relevance_override thy - const_tab relevance_threshold goal_const_tab + relevant_clauses ctxt convergence follow_defs max_new relevance_override + thy const_tab relevance_threshold goal_const_tab (map (pair_consts_typs_axiom add_theory_const thy) axioms) in @@ -384,7 +374,7 @@ filter (not o known) c_clauses end; -fun all_valid_thms ctxt = +fun all_valid_thms respect_no_atp ctxt = let val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt); val local_facts = ProofContext.facts_of ctxt; @@ -404,7 +394,7 @@ val ths = filter_out bad_for_atp ths0; in if Facts.is_concealed facts name orelse null ths orelse - run_blacklist_filter andalso is_package_def name then I + respect_no_atp andalso is_package_def name then I else (case find_first check_thms [name1, name2, name] of NONE => I @@ -427,13 +417,14 @@ fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a; (*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*) -fun name_thm_pairs ctxt = +fun name_thm_pairs respect_no_atp ctxt = let - val (mults, singles) = List.partition is_multi (all_valid_thms ctxt) + val (mults, singles) = + List.partition is_multi (all_valid_thms respect_no_atp ctxt) val ps = [] |> fold add_multi_names mults |> fold add_single_names singles in - if run_blacklist_filter then + if respect_no_atp then let val blacklist = No_ATPs.get ctxt |> map (`Thm.full_prop_of) |> Termtab.make @@ -447,11 +438,11 @@ (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false) | check_named _ = true; -fun get_all_lemmas ctxt = +fun get_all_lemmas respect_no_atp ctxt = let val included_thms = tap (fn ths => trace_msg (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems"))) - (name_thm_pairs ctxt) + (name_thm_pairs respect_no_atp ctxt) in filter check_named included_thms end; @@ -548,18 +539,18 @@ NONE => forall (Meson.is_fol_term thy) (map prop_of goal_cls) | SOME b => not b -fun get_relevant_facts relevance_threshold higher_order follow_defs max_new - add_theory_const relevance_override - (ctxt, (chain_ths, th)) goal_cls = +fun get_relevant_facts respect_no_atp relevance_threshold convergence + higher_order follow_defs max_new add_theory_const + relevance_override (ctxt, (chain_ths, th)) goal_cls = let val thy = ProofContext.theory_of ctxt val is_FO = is_first_order thy higher_order goal_cls - val included_cls = get_all_lemmas ctxt + val included_cls = get_all_lemmas respect_no_atp ctxt |> cnf_rules_pairs thy |> make_unique |> restrict_to_logic thy is_FO |> remove_unwanted_clauses in - relevance_filter ctxt relevance_threshold follow_defs max_new + relevance_filter ctxt relevance_threshold convergence follow_defs max_new add_theory_const relevance_override thy included_cls (map prop_of goal_cls) end; diff -r eb44a5d40b9e -r 8256d5a185bd src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Mar 28 18:39:27 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Mar 29 12:01:00 2010 +0200 @@ -40,9 +40,10 @@ val default_default_params = [("debug", "false"), ("verbose", "false"), + ("respect_no_atp", "true"), ("relevance_threshold", "50"), + ("convergence", "320"), ("higher_order", "smart"), - ("respect_no_atp", "true"), ("follow_defs", "false"), ("isar_proof", "false"), ("minimize_timeout", "5 s")] @@ -50,9 +51,9 @@ val negated_params = [("no_debug", "debug"), ("quiet", "verbose"), + ("ignore_no_atp", "respect_no_atp"), ("partial_types", "full_types"), ("first_order", "higher_order"), - ("ignore_no_atp", "respect_no_atp"), ("dont_follow_defs", "follow_defs"), ("metis_proof", "isar_proof")] @@ -119,19 +120,20 @@ val verbose = debug orelse lookup_bool "verbose" val atps = lookup_string "atps" |> space_explode " " val full_types = lookup_bool "full_types" + val respect_no_atp = lookup_bool "respect_no_atp" val relevance_threshold = 0.01 * Real.fromInt (lookup_int "relevance_threshold") + val convergence = 0.01 * Real.fromInt (lookup_int "convergence") val higher_order = lookup_bool_option "higher_order" - val respect_no_atp = lookup_bool "respect_no_atp" val follow_defs = lookup_bool "follow_defs" val isar_proof = lookup_bool "isar_proof" val timeout = lookup_time "timeout" val minimize_timeout = lookup_time "minimize_timeout" in {debug = debug, verbose = verbose, atps = atps, full_types = full_types, - relevance_threshold = relevance_threshold, higher_order = higher_order, - respect_no_atp = respect_no_atp, follow_defs = follow_defs, - isar_proof = isar_proof, timeout = timeout, + respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold, + convergence = convergence, higher_order = higher_order, + follow_defs = follow_defs, isar_proof = isar_proof, timeout = timeout, minimize_timeout = minimize_timeout} end