# HG changeset patch # User blanchet # Date 1271666708 -7200 # Node ID f3655a3ae1ab8673994aa3f6fed55980c07c42d0 # Parent 16670b4f0baaed109ed5d01a6dae1d447575d5df rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does diff -r 16670b4f0baa -r f3655a3ae1ab src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Apr 19 10:15:02 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Apr 19 10:45:08 2010 +0200 @@ -18,7 +18,7 @@ respect_no_atp: bool, relevance_threshold: real, convergence: real, - theory_const: bool option, + theory_relevant: bool option, higher_order: bool option, follow_defs: bool, isar_proof: bool, @@ -71,7 +71,7 @@ respect_no_atp: bool, relevance_threshold: real, convergence: real, - theory_const: bool option, + theory_relevant: bool option, higher_order: bool option, follow_defs: bool, isar_proof: bool, diff -r 16670b4f0baa -r f3655a3ae1ab src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Mon Apr 19 10:15:02 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Mon Apr 19 10:45:08 2010 +0200 @@ -48,7 +48,7 @@ arguments: Time.time -> string, failure_strs: string list, max_new_clauses: int, - prefers_theory_const: bool, + prefers_theory_relevant: bool, supports_isar_proofs: bool}; @@ -167,15 +167,15 @@ fun generic_tptp_prover (name, {command, arguments, failure_strs, max_new_clauses, - prefers_theory_const, supports_isar_proofs}) + prefers_theory_relevant, supports_isar_proofs}) (params as {overlord, respect_no_atp, relevance_threshold, convergence, - theory_const, higher_order, follow_defs, isar_proof, + theory_relevant, higher_order, follow_defs, isar_proof, modulus, sorts, ...}) timeout = generic_prover overlord (get_relevant_facts respect_no_atp relevance_threshold convergence higher_order follow_defs max_new_clauses - (the_default prefers_theory_const theory_const)) + (the_default prefers_theory_relevant theory_relevant)) (prepare_clauses higher_order false) write_tptp_file command (arguments timeout) failure_strs (if supports_isar_proofs andalso isar_proof then @@ -201,7 +201,7 @@ failure_strs = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"], max_new_clauses = 60, - prefers_theory_const = false, + prefers_theory_relevant = false, supports_isar_proofs = true} val vampire = tptp_prover "vampire" vampire_config @@ -218,7 +218,7 @@ "SZS status: ResourceOut", "SZS status ResourceOut", "# Cannot determine problem status"], max_new_clauses = 100, - prefers_theory_const = false, + prefers_theory_relevant = false, supports_isar_proofs = true} val e = tptp_prover "e" e_config @@ -227,14 +227,14 @@ fun generic_dfg_prover (name, ({command, arguments, failure_strs, max_new_clauses, - prefers_theory_const, ...} : prover_config)) + prefers_theory_relevant, ...} : prover_config)) (params as {overlord, respect_no_atp, relevance_threshold, convergence, - theory_const, higher_order, follow_defs, ...}) + theory_relevant, higher_order, follow_defs, ...}) timeout = generic_prover overlord (get_relevant_facts respect_no_atp relevance_threshold convergence higher_order follow_defs max_new_clauses - (the_default prefers_theory_const theory_const)) + (the_default prefers_theory_relevant theory_relevant)) (prepare_clauses higher_order true) write_dfg_file command (arguments timeout) failure_strs (metis_lemma_list true) name params; @@ -251,7 +251,7 @@ ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.", "SPASS beiseite: Maximal number of loops exceeded."], max_new_clauses = 40, - prefers_theory_const = true, + prefers_theory_relevant = true, supports_isar_proofs = false} val spass = dfg_prover ("spass", spass_config) @@ -285,7 +285,7 @@ val remote_failure_strs = ["Remote-script could not extract proof"]; fun remote_prover_config prover_prefix args - ({failure_strs, max_new_clauses, prefers_theory_const, ...} + ({failure_strs, max_new_clauses, prefers_theory_relevant, ...} : prover_config) : prover_config = {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP", arguments = (fn timeout => @@ -293,7 +293,7 @@ the_system prover_prefix), failure_strs = remote_failure_strs @ failure_strs, max_new_clauses = max_new_clauses, - prefers_theory_const = prefers_theory_const, + prefers_theory_relevant = prefers_theory_relevant, supports_isar_proofs = false} val remote_vampire = diff -r 16670b4f0baa -r f3655a3ae1ab src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Apr 19 10:15:02 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Apr 19 10:45:08 2010 +0200 @@ -127,8 +127,8 @@ (*Inserts a dummy "constant" referring to the theory name, so that relevance takes the given theory into account.*) -fun const_prop_of theory_const th = - if theory_const then +fun const_prop_of theory_relevant th = + if theory_relevant then let val name = Context.theory_name (theory_of_thm th) val t = Const (name ^ ". 1", HOLogic.boolT) in t $ prop_of th end @@ -157,7 +157,7 @@ structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord); -fun count_axiom_consts theory_const thy ((thm,_), tab) = +fun count_axiom_consts theory_relevant thy ((thm,_), tab) = let fun count_const (a, T, tab) = let val (c, cts) = const_with_typ thy (a,T) in (*Two-dimensional table update. Constant maps to types maps to count.*) @@ -170,7 +170,7 @@ count_term_consts (t, count_term_consts (u, tab)) | count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab) | count_term_consts (_, tab) = tab - in count_term_consts (const_prop_of theory_const thm, tab) end; + in count_term_consts (const_prop_of theory_relevant thm, tab) end; (**** Actual Filtering Code ****) @@ -201,8 +201,8 @@ let val tab = add_term_consts_typs_rm thy (t, null_const_tab) in Symtab.fold add_expand_pairs tab [] end; -fun pair_consts_typs_axiom theory_const thy (p as (thm, _)) = - (p, (consts_typs_of_term thy (const_prop_of theory_const thm))); +fun pair_consts_typs_axiom theory_relevant thy (p as (thm, _)) = + (p, (consts_typs_of_term thy (const_prop_of theory_relevant thm))); exception ConstFree; fun dest_ConstFree (Const aT) = aT @@ -294,10 +294,10 @@ in iter end fun relevance_filter ctxt relevance_threshold convergence follow_defs max_new - theory_const relevance_override thy axioms goals = + theory_relevant relevance_override thy axioms goals = if relevance_threshold > 0.0 then let - val const_tab = List.foldl (count_axiom_consts theory_const thy) + val const_tab = List.foldl (count_axiom_consts theory_relevant thy) Symtab.empty axioms val goal_const_tab = get_goal_consts_typs thy goals val _ = @@ -306,7 +306,8 @@ val relevant = relevant_clauses ctxt convergence follow_defs max_new relevance_override thy const_tab relevance_threshold goal_const_tab - (map (pair_consts_typs_axiom theory_const thy) axioms) + (map (pair_consts_typs_axiom theory_relevant thy) + axioms) in trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant)); relevant @@ -502,7 +503,7 @@ | SOME b => not b fun get_relevant_facts respect_no_atp relevance_threshold convergence - higher_order follow_defs max_new theory_const + higher_order follow_defs 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 @@ -517,7 +518,7 @@ |> remove_unwanted_clauses in relevance_filter ctxt relevance_threshold convergence follow_defs max_new - theory_const relevance_override thy included_cls + theory_relevant relevance_override thy included_cls (map prop_of goal_cls) end diff -r 16670b4f0baa -r f3655a3ae1ab src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Apr 19 10:15:02 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Apr 19 10:45:08 2010 +0200 @@ -44,7 +44,7 @@ ("respect_no_atp", "true"), ("relevance_threshold", "50"), ("convergence", "320"), - ("theory_const", "smart"), + ("theory_relevant", "smart"), ("higher_order", "smart"), ("follow_defs", "false"), ("isar_proof", "false"), @@ -60,7 +60,7 @@ ("no_overlord", "overlord"), ("ignore_no_atp", "respect_no_atp"), ("partial_types", "full_types"), - ("no_theory_const", "theory_const"), + ("theory_irrelevant", "theory_relevant"), ("first_order", "higher_order"), ("dont_follow_defs", "follow_defs"), ("metis_proof", "isar_proof"), @@ -150,7 +150,7 @@ val relevance_threshold = 0.01 * Real.fromInt (lookup_int "relevance_threshold") val convergence = 0.01 * Real.fromInt (lookup_int "convergence") - val theory_const = lookup_bool_option "theory_const" + val theory_relevant = lookup_bool_option "theory_relevant" val higher_order = lookup_bool_option "higher_order" val follow_defs = lookup_bool "follow_defs" val isar_proof = lookup_bool "isar_proof" @@ -162,7 +162,7 @@ {debug = debug, verbose = verbose, overlord = overlord, atps = atps, full_types = full_types, respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold, convergence = convergence, - theory_const = theory_const, higher_order = higher_order, + theory_relevant = theory_relevant, higher_order = higher_order, follow_defs = follow_defs, isar_proof = isar_proof, modulus = modulus, sorts = sorts, timeout = timeout, minimize_timeout = minimize_timeout} end