--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 24 22:57:22 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Aug 25 09:02:07 2010 +0200
@@ -452,10 +452,10 @@
relevance filter. The option ranges from 0 to 100, where 0 means that all
theorems are relevant.
-\opdefault{relevance\_convergence}{int}{31}
-Specifies the convergence factor, expressed as a percentage, used by the
-relevance filter. This factor is used by the relevance filter to scale down the
-relevance of facts at each iteration of the filter.
+\opdefault{relevance\_decay}{int}{31}
+Specifies the decay factor, expressed as a percentage, used by the relevance
+filter. This factor is used by the relevance filter to scale down the relevance
+of new facts at each iteration of the filter.
\opdefault{max\_relevant\_per\_iter}{int\_or\_smart}{\textit{smart}}
Specifies the maximum number of facts that may be added during one iteration of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 24 22:57:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 25 09:02:07 2010 +0200
@@ -19,7 +19,7 @@
full_types: bool,
explicit_apply: bool,
relevance_threshold: real,
- relevance_convergence: real,
+ relevance_decay: real,
max_relevant_per_iter: int option,
theory_relevant: bool option,
defs_relevant: bool,
@@ -88,7 +88,7 @@
full_types: bool,
explicit_apply: bool,
relevance_threshold: real,
- relevance_convergence: real,
+ relevance_decay: real,
max_relevant_per_iter: int option,
theory_relevant: bool option,
defs_relevant: bool,
@@ -215,7 +215,7 @@
known_failures, default_max_relevant_per_iter, default_theory_relevant,
explicit_forall, use_conjecture_for_hypotheses}
({debug, verbose, overlord, full_types, explicit_apply,
- relevance_threshold, relevance_convergence,
+ relevance_threshold, relevance_decay,
max_relevant_per_iter, theory_relevant,
defs_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
minimize_command
@@ -233,7 +233,7 @@
case axioms of
SOME axioms => axioms
| NONE =>
- (relevant_facts full_types relevance_threshold relevance_convergence
+ (relevant_facts full_types relevance_threshold relevance_decay
defs_relevant
(the_default default_max_relevant_per_iter
max_relevant_per_iter)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Aug 24 22:57:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 25 09:02:07 2010 +0200
@@ -285,114 +285,108 @@
fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
(* Limit the number of new facts, to prevent runaway acceptance. *)
-fun take_best max_new (new_pairs : (annotated_thm * real) list) =
+fun take_best max_relevant_per_iter (new_pairs : (annotated_thm * real) list) =
let val nnew = length new_pairs in
- if nnew <= max_new then
+ if nnew <= max_relevant_per_iter then
(map #1 new_pairs, [])
else
let
val new_pairs = sort compare_pairs new_pairs
- val accepted = List.take (new_pairs, max_new)
+ val accepted = List.take (new_pairs, max_relevant_per_iter)
in
trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
- ", exceeds the limit of " ^ Int.toString max_new));
+ ", exceeds the limit of " ^ Int.toString max_relevant_per_iter));
trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
trace_msg (fn () => "Actually passed: " ^
space_implode ", " (map (fst o (fn f => f ()) o fst o fst o fst) accepted));
- (map #1 accepted, List.drop (new_pairs, max_new))
+ (map #1 accepted, List.drop (new_pairs, max_relevant_per_iter))
end
end;
val threshold_divisor = 2.0
val ridiculous_threshold = 0.1
-fun relevance_filter ctxt relevance_threshold relevance_convergence
- defs_relevant max_new theory_relevant
+fun relevance_filter ctxt relevance_threshold relevance_decay defs_relevant
+ max_relevant_per_iter theory_relevant
({add, del, ...} : relevance_override) axioms goal_ts =
- if relevance_threshold > 1.0 then
- []
- else if relevance_threshold < 0.0 then
- axioms
- else
- let
- val thy = ProofContext.theory_of ctxt
- val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
- Symtab.empty
- val goal_const_tab = get_consts thy (SOME false) goal_ts
- val _ =
- trace_msg (fn () => "Initial constants: " ^
- commas (goal_const_tab
- |> Symtab.dest
- |> filter (curry (op <>) [] o snd)
- |> map fst))
- val add_thms = maps (ProofContext.get_fact ctxt) add
- val del_thms = maps (ProofContext.get_fact ctxt) del
- fun iter j threshold rel_const_tab =
- let
- fun relevant ([], rejects) [] =
- (* Nothing was added this iteration. *)
- if j = 0 andalso threshold >= ridiculous_threshold then
- (* First iteration? Try again. *)
- iter 0 (threshold / threshold_divisor) rel_const_tab
- (map (apsnd SOME) rejects)
+ let
+ val thy = ProofContext.theory_of ctxt
+ val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
+ Symtab.empty
+ val goal_const_tab = get_consts thy (SOME false) goal_ts
+ val _ =
+ trace_msg (fn () => "Initial constants: " ^
+ commas (goal_const_tab |> Symtab.dest
+ |> filter (curry (op <>) [] o snd)
+ |> map fst))
+ val add_thms = maps (ProofContext.get_fact ctxt) add
+ val del_thms = maps (ProofContext.get_fact ctxt) del
+ fun iter j threshold rel_const_tab =
+ let
+ fun relevant ([], rejects) [] =
+ (* Nothing was added this iteration. *)
+ if j = 0 andalso threshold >= ridiculous_threshold then
+ (* First iteration? Try again. *)
+ iter 0 (threshold / threshold_divisor) rel_const_tab
+ (map (apsnd SOME) rejects)
+ else
+ (* Add "add:" facts. *)
+ if null add_thms then
+ []
else
- (* Add "add:" facts. *)
- if null add_thms then
- []
- else
- map_filter (fn ((p as (_, th), _), _) =>
- if member Thm.eq_thm add_thms th then SOME p
- else NONE) rejects
- | relevant (new_pairs, rejects) [] =
- let
- val (new_rels, more_rejects) = take_best max_new new_pairs
- val rel_const_tab' =
- rel_const_tab |> fold add_const_to_table (maps snd new_rels)
- fun is_dirty c =
- const_mem rel_const_tab' c andalso
- not (const_mem rel_const_tab c)
- val rejects =
- more_rejects @ rejects
- |> map (fn (ax as (_, consts), old_weight) =>
- (ax, if exists is_dirty consts then NONE
- else SOME old_weight))
- val threshold =
- threshold + (1.0 - threshold) * relevance_convergence
- in
- trace_msg (fn () => "relevant this iteration: " ^
- Int.toString (length new_rels));
- map #1 new_rels @ iter (j + 1) threshold rel_const_tab' rejects
- end
- | relevant (new_rels, rejects)
- (((ax as ((name, th), axiom_consts)), cached_weight)
- :: rest) =
- let
- val weight =
- case cached_weight of
- 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
- (trace_msg (fn () =>
- fst (name ()) ^ " passes: " ^ Real.toString weight
- ^ " consts: " ^ commas (map fst axiom_consts));
- relevant ((ax, weight) :: new_rels, rejects) rest)
- else
- relevant (new_rels, (ax, weight) :: rejects) rest
- end
- in
- trace_msg (fn () => "relevant_facts, current threshold: " ^
- Real.toString threshold);
- relevant ([], [])
- end
- in
- axioms |> filter_out (member Thm.eq_thm del_thms o snd)
- |> map (rpair NONE o pair_consts_axiom theory_relevant thy)
- |> iter 0 relevance_threshold goal_const_tab
- |> tap (fn res => trace_msg (fn () =>
+ map_filter (fn ((p as (_, th), _), _) =>
+ if member Thm.eq_thm add_thms th then SOME p
+ else NONE) rejects
+ | relevant (new_pairs, rejects) [] =
+ let
+ val (new_rels, more_rejects) =
+ take_best max_relevant_per_iter new_pairs
+ val rel_const_tab' =
+ rel_const_tab |> fold add_const_to_table (maps snd new_rels)
+ fun is_dirty c =
+ const_mem rel_const_tab' c andalso
+ not (const_mem rel_const_tab c)
+ val rejects =
+ more_rejects @ rejects
+ |> map (fn (ax as (_, consts), old_weight) =>
+ (ax, if exists is_dirty consts then NONE
+ else SOME old_weight))
+ val threshold = threshold + (1.0 - threshold) * relevance_decay
+ in
+ trace_msg (fn () => "relevant this iteration: " ^
+ Int.toString (length new_rels));
+ map #1 new_rels @ iter (j + 1) threshold rel_const_tab' rejects
+ end
+ | relevant (new_rels, rejects)
+ (((ax as ((name, th), axiom_consts)), cached_weight)
+ :: rest) =
+ let
+ val weight =
+ case cached_weight of
+ 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
+ (trace_msg (fn () =>
+ fst (name ()) ^ " passes: " ^ Real.toString weight
+ ^ " consts: " ^ commas (map fst axiom_consts));
+ relevant ((ax, weight) :: new_rels, rejects) rest)
+ else
+ relevant (new_rels, (ax, weight) :: rejects) rest
+ end
+ in
+ trace_msg (fn () => "relevant_facts, current threshold: " ^
+ Real.toString threshold);
+ relevant ([], [])
+ end
+ in
+ axioms |> filter_out (member Thm.eq_thm del_thms o snd)
+ |> map (rpair NONE o pair_consts_axiom theory_relevant thy)
+ |> iter 0 relevance_threshold goal_const_tab
+ |> tap (fn res => trace_msg (fn () =>
"Total relevant: " ^ Int.toString (length res)))
- end
+ end
(***************************************************************)
(* Retrieving and filtering lemmas *)
@@ -614,8 +608,8 @@
(* ATP invocation methods setup *)
(***************************************************************)
-fun relevant_facts full_types relevance_threshold relevance_convergence
- defs_relevant max_new theory_relevant
+fun relevant_facts full_types relevance_threshold relevance_decay defs_relevant
+ max_relevant_per_iter theory_relevant
(relevance_override as {add, del, only})
(ctxt, (chained_ths, _)) hyp_ts concl_t =
let
@@ -632,9 +626,14 @@
in
trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^
" theorems");
- relevance_filter ctxt relevance_threshold relevance_convergence
- defs_relevant max_new theory_relevant relevance_override
- axioms (concl_t :: hyp_ts)
+ (if relevance_threshold > 1.0 then
+ []
+ else if relevance_threshold < 0.0 then
+ axioms
+ else
+ relevance_filter ctxt relevance_threshold relevance_decay defs_relevant
+ max_relevant_per_iter theory_relevant relevance_override
+ axioms (concl_t :: hyp_ts))
|> map (apfst (fn f => f ()))
|> sort_wrt (fst o fst)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 24 22:57:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 25 09:02:07 2010 +0200
@@ -41,9 +41,8 @@
end
fun test_theorems ({debug, verbose, overlord, atps, full_types,
- relevance_threshold, relevance_convergence,
- defs_relevant, isar_proof, isar_shrink_factor, ...}
- : params)
+ relevance_threshold, relevance_decay, defs_relevant,
+ isar_proof, isar_shrink_factor, ...} : params)
(prover : prover) explicit_apply timeout subgoal state
name_thms_pairs =
let
@@ -53,10 +52,10 @@
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
full_types = full_types, explicit_apply = explicit_apply,
relevance_threshold = relevance_threshold,
- relevance_convergence = relevance_convergence,
- max_relevant_per_iter = NONE, theory_relevant = NONE,
- defs_relevant = defs_relevant, isar_proof = isar_proof,
- isar_shrink_factor = isar_shrink_factor, timeout = timeout}
+ 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}
val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
val {context = ctxt, facts, goal} = Proof.goal state
val problem =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 24 22:57:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 25 09:02:07 2010 +0200
@@ -68,7 +68,7 @@
("overlord", "false"),
("explicit_apply", "false"),
("relevance_threshold", "40"),
- ("relevance_convergence", "31"),
+ ("relevance_decay", "31"),
("max_relevant_per_iter", "smart"),
("theory_relevant", "smart"),
("defs_relevant", "false"),
@@ -170,8 +170,8 @@
val explicit_apply = lookup_bool "explicit_apply"
val relevance_threshold =
0.01 * Real.fromInt (lookup_int "relevance_threshold")
- val relevance_convergence =
- 0.01 * Real.fromInt (lookup_int "relevance_convergence")
+ val relevance_decay =
+ 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"
@@ -182,7 +182,7 @@
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
full_types = full_types, explicit_apply = explicit_apply,
relevance_threshold = relevance_threshold,
- relevance_convergence = relevance_convergence,
+ 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,