# HG changeset patch # User blanchet # Date 1282721563 -7200 # Node ID 7635bf8918a10d28230a3821911a8b040423b927 # Parent e2d58749194b960af89bc9674c0f910672143168 get rid of "defs_relevant" feature; nobody uses it and it works poorly diff -r e2d58749194b -r 7635bf8918a1 doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Wed Aug 25 09:05:22 2010 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Aug 25 09:32:43 2010 +0200 @@ -469,10 +469,10 @@ it is taken to be \textit{true} for SPASS and \textit{false} for E and Vampire, because empirical results suggest that these are the best settings. -\opfalse{defs\_relevant}{defs\_irrelevant} -Specifies whether the definition of constants occurring in the formula to prove -should be considered particularly relevant. Enabling this option tends to lead -to larger problems and typically slows down the ATPs. +%\opfalse{defs\_relevant}{defs\_irrelevant} +%Specifies whether the definition of constants occurring in the formula to prove +%should be considered particularly relevant. Enabling this option tends to lead +%to larger problems and typically slows down the ATPs. \end{enum} diff -r e2d58749194b -r 7635bf8918a1 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 25 09:05:22 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 25 09:32:43 2010 +0200 @@ -22,7 +22,6 @@ relevance_decay: real, max_relevant_per_iter: int option, theory_relevant: bool option, - defs_relevant: bool, isar_proof: bool, isar_shrink_factor: int, timeout: Time.time} @@ -91,7 +90,6 @@ relevance_decay: real, max_relevant_per_iter: int option, theory_relevant: bool option, - defs_relevant: bool, isar_proof: bool, isar_shrink_factor: int, timeout: Time.time} @@ -216,8 +214,8 @@ explicit_forall, use_conjecture_for_hypotheses} ({debug, verbose, overlord, full_types, explicit_apply, relevance_threshold, relevance_decay, - max_relevant_per_iter, theory_relevant, - defs_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params) + max_relevant_per_iter, theory_relevant, isar_proof, + isar_shrink_factor, timeout, ...} : params) minimize_command ({subgoal, goal, relevance_override, axioms} : problem) = let @@ -234,7 +232,6 @@ SOME axioms => axioms | NONE => (relevant_facts full_types relevance_threshold relevance_decay - defs_relevant (the_default default_max_relevant_per_iter max_relevant_per_iter) (the_default default_theory_relevant theory_relevant) diff -r e2d58749194b -r 7635bf8918a1 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 25 09:05:22 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 25 09:32:43 2010 +0200 @@ -15,7 +15,7 @@ Proof.context -> unit Symtab.table -> thm list -> Facts.ref -> (unit -> string * bool) * thm list val relevant_facts : - bool -> real -> real -> bool -> int -> bool -> relevance_override + bool -> real -> real -> int -> bool -> relevance_override -> Proof.context * (thm list * 'a) -> term list -> term -> ((string * bool) * thm) list end; @@ -244,9 +244,9 @@ in if Real.isFinite res then res else 0.0 end *) -(*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*) +(* Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list + -> ('a * 'b) list. *) fun add_expand_pairs (x, ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys - fun consts_of_term thy t = Symtab.fold add_expand_pairs (get_consts thy (SOME true) [t]) [] @@ -254,30 +254,6 @@ (axiom, axiom |> snd |> theory_const_prop_of theory_relevant |> consts_of_term thy) -exception CONST_OR_FREE of unit - -fun dest_Const_or_Free (Const x) = x - | dest_Const_or_Free (Free x) = x - | dest_Const_or_Free _ = raise CONST_OR_FREE () - -(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*) -fun defines thy thm gctypes = - let val tm = prop_of thm - fun defs lhs rhs = - let val (rator,args) = strip_comb lhs - val ct = const_with_typ thy (dest_Const_or_Free rator) - in - forall is_Var args andalso const_mem gctypes ct andalso - subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) - end - handle CONST_OR_FREE () => false - in - case tm of - @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) => - defs lhs rhs - | _ => false - end; - type annotated_thm = ((unit -> string * bool) * thm) * (string * const_typ list) list @@ -306,7 +282,7 @@ val threshold_divisor = 2.0 val ridiculous_threshold = 0.1 -fun relevance_filter ctxt relevance_threshold relevance_decay defs_relevant +fun relevance_filter ctxt relevance_threshold relevance_decay max_relevant_per_iter theory_relevant ({add, del, ...} : relevance_override) axioms goal_ts = let @@ -366,8 +342,7 @@ SOME w => w | NONE => axiom_weight const_tab rel_const_tab axiom_consts in - if weight >= threshold orelse - (defs_relevant andalso defines thy th rel_const_tab) then + if weight >= threshold then (trace_msg (fn () => fst (name ()) ^ " passes: " ^ Real.toString weight ^ " consts: " ^ commas (map fst axiom_consts)); @@ -608,7 +583,7 @@ (* ATP invocation methods setup *) (***************************************************************) -fun relevant_facts full_types relevance_threshold relevance_decay defs_relevant +fun relevant_facts full_types relevance_threshold relevance_decay max_relevant_per_iter theory_relevant (relevance_override as {add, del, only}) (ctxt, (chained_ths, _)) hyp_ts concl_t = @@ -631,7 +606,7 @@ else if relevance_threshold < 0.0 then axioms else - relevance_filter ctxt relevance_threshold relevance_decay defs_relevant + relevance_filter ctxt relevance_threshold relevance_decay max_relevant_per_iter theory_relevant relevance_override axioms (concl_t :: hyp_ts)) |> map (apfst (fn f => f ())) diff -r e2d58749194b -r 7635bf8918a1 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 25 09:05:22 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 25 09:32:43 2010 +0200 @@ -41,8 +41,8 @@ end fun test_theorems ({debug, verbose, overlord, atps, full_types, - relevance_threshold, relevance_decay, defs_relevant, - isar_proof, isar_shrink_factor, ...} : params) + relevance_threshold, relevance_decay, isar_proof, + isar_shrink_factor, ...} : params) (prover : prover) explicit_apply timeout subgoal state name_thms_pairs = let @@ -53,9 +53,8 @@ full_types = full_types, explicit_apply = explicit_apply, relevance_threshold = relevance_threshold, relevance_decay = relevance_decay, max_relevant_per_iter = NONE, - theory_relevant = NONE, defs_relevant = defs_relevant, - isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, - timeout = timeout} + theory_relevant = NONE, isar_proof = isar_proof, + isar_shrink_factor = isar_shrink_factor, timeout = timeout} val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs val {context = ctxt, facts, goal} = Proof.goal state val problem = diff -r e2d58749194b -r 7635bf8918a1 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 25 09:05:22 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 25 09:32:43 2010 +0200 @@ -71,7 +71,6 @@ ("relevance_decay", "31"), ("max_relevant_per_iter", "smart"), ("theory_relevant", "smart"), - ("defs_relevant", "false"), ("isar_proof", "false"), ("isar_shrink_factor", "1")] @@ -84,7 +83,6 @@ ("partial_types", "full_types"), ("implicit_apply", "explicit_apply"), ("theory_irrelevant", "theory_relevant"), - ("defs_irrelevant", "defs_relevant"), ("no_isar_proof", "isar_proof")] val params_for_minimize = @@ -174,7 +172,6 @@ 0.01 * Real.fromInt (lookup_int "relevance_decay") val max_relevant_per_iter = lookup_int_option "max_relevant_per_iter" val theory_relevant = lookup_bool_option "theory_relevant" - val defs_relevant = lookup_bool "defs_relevant" val isar_proof = lookup_bool "isar_proof" val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") val timeout = lookup_time "timeout" @@ -184,9 +181,8 @@ relevance_threshold = relevance_threshold, relevance_decay = relevance_decay, max_relevant_per_iter = max_relevant_per_iter, - theory_relevant = theory_relevant, defs_relevant = defs_relevant, - isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, - timeout = timeout} + theory_relevant = theory_relevant, isar_proof = isar_proof, + isar_shrink_factor = isar_shrink_factor, timeout = timeout} end fun get_params thy = extract_params (default_raw_params thy)