# HG changeset patch # User blanchet # Date 1273846510 -7200 # Node ID 12f87df9c1a5f660e98ca57a402902b436355bfd # Parent e65f8d253fd15dd9ca4522d9312d48760436dbf1 renamed two Sledgehammer options diff -r e65f8d253fd1 -r 12f87df9c1a5 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri May 14 15:27:07 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri May 14 16:15:10 2010 +0200 @@ -20,9 +20,9 @@ explicit_apply: bool, respect_no_atp: bool, relevance_threshold: real, - convergence: real, + relevance_convergence: real, theory_relevant: bool option, - follow_defs: bool, + defs_relevant: bool, isar_proof: bool, shrink_factor: int, timeout: Time.time, @@ -79,9 +79,9 @@ explicit_apply: bool, respect_no_atp: bool, relevance_threshold: real, - convergence: real, + relevance_convergence: real, theory_relevant: bool option, - follow_defs: bool, + defs_relevant: bool, isar_proof: bool, shrink_factor: int, timeout: Time.time, diff -r e65f8d253fd1 -r 12f87df9c1a5 src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri May 14 15:27:07 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri May 14 16:15:10 2010 +0200 @@ -237,11 +237,12 @@ (name, {home_var, executable, arguments, proof_delims, known_failures, max_axiom_clauses, prefers_theory_relevant}) (params as {debug, overlord, respect_no_atp, relevance_threshold, - convergence, theory_relevant, follow_defs, isar_proof, ...}) + relevance_convergence, theory_relevant, defs_relevant, + isar_proof, ...}) minimize_command timeout = generic_prover overlord - (get_relevant_facts respect_no_atp relevance_threshold convergence - follow_defs max_axiom_clauses + (get_relevant_facts respect_no_atp relevance_threshold + relevance_convergence defs_relevant max_axiom_clauses (the_default prefers_theory_relevant theory_relevant)) (prepare_clauses false) (write_tptp_file (debug andalso overlord)) home_var @@ -309,12 +310,12 @@ fun generic_dfg_prover (name, {home_var, executable, arguments, proof_delims, known_failures, max_axiom_clauses, prefers_theory_relevant}) - (params as {overlord, respect_no_atp, relevance_threshold, convergence, - theory_relevant, follow_defs, ...}) + (params as {overlord, respect_no_atp, relevance_threshold, + relevance_convergence, theory_relevant, defs_relevant, ...}) minimize_command timeout = generic_prover overlord - (get_relevant_facts respect_no_atp relevance_threshold convergence - follow_defs max_axiom_clauses + (get_relevant_facts respect_no_atp relevance_threshold + relevance_convergence defs_relevant max_axiom_clauses (the_default prefers_theory_relevant theory_relevant)) (prepare_clauses true) write_dfg_file home_var executable (arguments timeout) proof_delims known_failures name params diff -r e65f8d253fd1 -r 12f87df9c1a5 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri May 14 15:27:07 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri May 14 16:15:10 2010 +0200 @@ -253,7 +253,7 @@ end end; -fun relevant_clauses ctxt convergence follow_defs max_new +fun relevant_clauses ctxt relevance_convergence defs_relevant max_new (relevance_override as {add, del, only}) thy ctab = let val thms_for_facts = @@ -268,7 +268,7 @@ val (newrels, more_rejects) = take_best max_new newpairs val new_consts = maps #2 newrels val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts - val newp = p + (1.0-p) / convergence + val newp = p + (1.0 - p) / relevance_convergence in trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels)); @@ -283,7 +283,7 @@ else clause_weight ctab rel_consts consts_typs in if p <= weight orelse - (follow_defs andalso defines thy (#1 clsthm) rel_consts) then + (defs_relevant andalso defines thy (#1 clsthm) rel_consts) then (trace_msg (fn () => name ^ " clause " ^ Int.toString n ^ " passes: " ^ Real.toString weight); relevant ((ax, weight) :: newrels, rejects) axs) @@ -297,8 +297,9 @@ end in iter end -fun relevance_filter ctxt relevance_threshold convergence follow_defs max_new - theory_relevant relevance_override thy axioms goals = +fun relevance_filter ctxt relevance_threshold relevance_convergence + defs_relevant max_new theory_relevant relevance_override + thy axioms goals = if relevance_threshold > 0.0 then let val const_tab = List.foldl (count_axiom_consts theory_relevant thy) @@ -308,8 +309,9 @@ trace_msg (fn () => "Initial constants: " ^ commas (Symtab.keys goal_const_tab)) val relevant = - relevant_clauses ctxt convergence follow_defs max_new relevance_override - thy const_tab relevance_threshold goal_const_tab + relevant_clauses ctxt relevance_convergence defs_relevant max_new + relevance_override thy const_tab relevance_threshold + goal_const_tab (map (pair_consts_typs_axiom theory_relevant thy) axioms) in @@ -504,8 +506,8 @@ fun is_first_order thy = forall (Meson.is_fol_term thy) o map prop_of -fun get_relevant_facts respect_no_atp relevance_threshold convergence - follow_defs max_new theory_relevant +fun get_relevant_facts respect_no_atp relevance_threshold relevance_convergence + defs_relevant max_new theory_relevant (relevance_override as {add, only, ...}) (ctxt, (chain_ths, th)) goal_cls = if (only andalso null add) orelse relevance_threshold > 1.0 then @@ -519,9 +521,9 @@ |> restrict_to_logic thy is_FO |> remove_unwanted_clauses in - relevance_filter ctxt relevance_threshold convergence follow_defs max_new - theory_relevant relevance_override thy included_cls - (map prop_of goal_cls) + relevance_filter ctxt relevance_threshold relevance_convergence + defs_relevant max_new theory_relevant relevance_override + thy included_cls (map prop_of goal_cls) end (* prepare for passing to writer, diff -r e65f8d253fd1 -r 12f87df9c1a5 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri May 14 15:27:07 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri May 14 16:15:10 2010 +0200 @@ -52,14 +52,6 @@ open Sledgehammer_FOL_Clause open Sledgehammer_Fact_Preprocessor -(* Parameter "full_types" below indicates that full type information is to be - exported. - - If "explicit_apply" is false, each function will be directly applied to as - many arguments as possible, avoiding use of the "apply" operator. Use of - "hBOOL" is also minimized. -*) - fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c); (*True if the constant ever appears outside of the top-level position in literals. diff -r e65f8d253fd1 -r 12f87df9c1a5 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 14 15:27:07 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 14 16:15:10 2010 +0200 @@ -94,9 +94,9 @@ ("explicit_apply", "false"), ("respect_no_atp", "true"), ("relevance_threshold", "50"), - ("convergence", "320"), + ("relevance_convergence", "320"), ("theory_relevant", "smart"), - ("follow_defs", "false"), + ("defs_relevant", "false"), ("isar_proof", "false"), ("shrink_factor", "1"), ("minimize_timeout", "5 s")] @@ -111,7 +111,7 @@ ("implicit_apply", "explicit_apply"), ("ignore_no_atp", "respect_no_atp"), ("theory_irrelevant", "theory_relevant"), - ("dont_follow_defs", "follow_defs"), + ("defs_irrelevant", "defs_relevant"), ("no_isar_proof", "isar_proof")] val params_for_minimize = @@ -194,9 +194,10 @@ 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 relevance_convergence = + 0.01 * Real.fromInt (lookup_int "relevance_convergence") val theory_relevant = lookup_bool_option "theory_relevant" - val follow_defs = lookup_bool "follow_defs" + val defs_relevant = lookup_bool "defs_relevant" val isar_proof = lookup_bool "isar_proof" val shrink_factor = Int.max (1, lookup_int "shrink_factor") val timeout = lookup_time "timeout" @@ -205,9 +206,9 @@ {debug = debug, verbose = verbose, overlord = overlord, atps = atps, full_types = full_types, explicit_apply = explicit_apply, respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold, - convergence = convergence, theory_relevant = theory_relevant, - follow_defs = follow_defs, isar_proof = isar_proof, - shrink_factor = shrink_factor, timeout = timeout, + relevance_convergence = relevance_convergence, + theory_relevant = theory_relevant, defs_relevant = defs_relevant, + isar_proof = isar_proof, shrink_factor = shrink_factor, timeout = timeout, minimize_timeout = minimize_timeout} end