--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 25 17:49:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 25 19:41:18 2010 +0200
@@ -18,8 +18,7 @@
atps: string list,
full_types: bool,
explicit_apply: bool,
- relevance_threshold: real,
- relevance_decay: real option,
+ relevance_thresholds: real * real,
max_relevant: int option,
theory_relevant: bool option,
isar_proof: bool,
@@ -86,8 +85,7 @@
atps: string list,
full_types: bool,
explicit_apply: bool,
- relevance_threshold: real,
- relevance_decay: real option,
+ relevance_thresholds: real * real,
max_relevant: int option,
theory_relevant: bool option,
isar_proof: bool,
@@ -213,8 +211,8 @@
known_failures, default_max_relevant, default_theory_relevant,
explicit_forall, use_conjecture_for_hypotheses}
({debug, verbose, overlord, full_types, explicit_apply,
- relevance_threshold, relevance_decay, max_relevant, theory_relevant,
- isar_proof, isar_shrink_factor, timeout, ...} : params)
+ relevance_thresholds, max_relevant, theory_relevant, isar_proof,
+ isar_shrink_factor, timeout, ...} : params)
minimize_command
({subgoal, goal, relevance_override, axioms} : problem) =
let
@@ -230,13 +228,13 @@
case axioms of
SOME axioms => axioms
| NONE =>
- (relevant_facts full_types relevance_threshold relevance_decay
+ (relevant_facts full_types relevance_thresholds
(the_default default_max_relevant max_relevant)
(the_default default_theory_relevant theory_relevant)
relevance_override goal hyp_ts concl_t
|> tap ((fn n => print_v (fn () =>
- "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
- " for " ^ quote atp_name ^ ".")) o length))
+ "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
+ " for " ^ quote atp_name ^ ".")) o length))
(* path to unique problem file *)
val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 25 17:49:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 25 19:41:18 2010 +0200
@@ -15,7 +15,7 @@
Proof.context -> unit Symtab.table -> thm list -> Facts.ref
-> ((unit -> string * bool) * (bool * thm)) list
val relevant_facts :
- bool -> real -> real option -> int -> bool -> relevance_override
+ bool -> real * real -> int -> bool -> relevance_override
-> Proof.context * (thm list * 'a) -> term list -> term
-> ((string * bool) * thm) list
end;
@@ -265,47 +265,45 @@
type annotated_thm =
((unit -> string * bool) * thm) * (string * pseudotype list) list
-fun rev_compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
-
-fun take_best max (new_pairs : (annotated_thm * real) list) =
+fun take_best max (candidates : (annotated_thm * real) list) =
let
val ((perfect, more_perfect), imperfect) =
- new_pairs |> List.partition (fn (_, w) => w > 0.99999)
- |>> chop (max - 1) ||> sort rev_compare_pairs
- val (accepted, rejected) =
+ candidates |> List.partition (fn (_, w) => w > 0.99999) |>> chop (max - 1)
+ ||> sort (Real.compare o swap o pairself snd)
+ val (accepts, rejects) =
case more_perfect @ imperfect of
[] => (perfect, [])
| (q :: qs) => (q :: perfect, qs)
in
trace_msg (fn () => "Number of candidates: " ^
- string_of_int (length new_pairs));
+ string_of_int (length candidates));
trace_msg (fn () => "Effective threshold: " ^
- Real.toString (#2 (hd accepted)));
+ Real.toString (#2 (hd accepts)));
trace_msg (fn () => "Actually passed: " ^
- (accepted |> map (fn (((name, _), _), weight) =>
- fst (name ()) ^ " [" ^ Real.toString weight ^ "]")
- |> commas));
- (map #1 accepted, rejected)
+ (accepts |> map (fn (((name, _), _), weight) =>
+ fst (name ()) ^ " [" ^ Real.toString weight ^ "]")
+ |> commas));
+ (accepts, rejects)
end
val threshold_divisor = 2.0
val ridiculous_threshold = 0.1
-fun relevance_filter ctxt relevance_threshold relevance_decay max_relevant
- theory_relevant ({add, del, ...} : relevance_override)
- axioms goal_ts =
+fun relevance_filter ctxt threshold0 decay max_relevant theory_relevant
+ ({add, del, ...} : relevance_override) axioms goal_ts =
let
val thy = ProofContext.theory_of ctxt
val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
Symtab.empty
val add_thms = maps (ProofContext.get_fact ctxt) add
val del_thms = maps (ProofContext.get_fact ctxt) del
- fun iter j max threshold rel_const_tab rest =
+ fun iter j max threshold rel_const_tab hopeless hopeful =
let
fun game_over rejects =
if j = 0 andalso threshold >= ridiculous_threshold then
(* First iteration? Try again. *)
- iter 0 max (threshold / threshold_divisor) rel_const_tab rejects
+ iter 0 max (threshold / threshold_divisor) rel_const_tab hopeless
+ hopeful
else
(* Add "add:" facts. *)
if null add_thms then
@@ -314,35 +312,45 @@
map_filter (fn ((p as (_, th), _), _) =>
if member Thm.eq_thm add_thms th then SOME p
else NONE) rejects
- fun relevant ([], rejects) [] =
+ fun relevant [] rejects [] hopeless =
(* Nothing has been added this iteration. *)
- game_over (map (apsnd SOME) rejects)
- | relevant (new_pairs, rejects) [] =
+ game_over (map (apsnd SOME) (rejects @ hopeless))
+ | relevant candidates rejects [] hopeless =
let
- val (new_rels, more_rejects) = take_best max new_pairs
+ val (accepts, more_rejects) = take_best max candidates
val rel_const_tab' =
- rel_const_tab |> fold add_const_to_table (maps snd new_rels)
+ rel_const_tab
+ |> fold add_const_to_table (maps (snd o fst) accepts)
fun is_dirty (c, _) =
Symtab.lookup rel_const_tab' c <> Symtab.lookup 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
- val max = max - length new_rels
+ val (hopeful_rejects, hopeless_rejects) =
+ (rejects @ hopeless, ([], []))
+ |-> fold (fn (ax as (_, consts), old_weight) =>
+ if exists is_dirty consts then
+ apfst (cons (ax, NONE))
+ else
+ apsnd (cons (ax, old_weight)))
+ |>> append (more_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) * decay
+ val max = max - length accepts
in
trace_msg (fn () => "New or updated constants: " ^
commas (rel_const_tab' |> Symtab.dest
|> subtract (op =) (Symtab.dest rel_const_tab)
|> map string_for_super_pseudoconst));
- map #1 new_rels @
- (if max = 0 then game_over rejects
- else iter (j + 1) max threshold rel_const_tab' rejects)
+ map (fst o fst) accepts @
+ (if max = 0 then
+ game_over (hopeful_rejects @ map (apsnd SOME) hopeless_rejects)
+ else
+ iter (j + 1) max threshold rel_const_tab' hopeless_rejects
+ hopeful_rejects)
end
- | relevant (new_rels, rejects)
+ | relevant candidates rejects
(((ax as ((name, th), axiom_consts)), cached_weight)
- :: rest) =
+ :: hopeful) hopeless =
let
val weight =
case cached_weight of
@@ -350,9 +358,9 @@
| NONE => axiom_weight const_tab rel_const_tab axiom_consts
in
if weight >= threshold then
- relevant ((ax, weight) :: new_rels, rejects) rest
+ relevant ((ax, weight) :: candidates) rejects hopeful hopeless
else
- relevant (new_rels, (ax, weight) :: rejects) rest
+ relevant candidates ((ax, weight) :: rejects) hopeful hopeless
end
in
trace_msg (fn () =>
@@ -361,13 +369,13 @@
commas (rel_const_tab |> Symtab.dest
|> filter (curry (op <>) [] o snd)
|> map string_for_super_pseudoconst));
- relevant ([], []) rest
+ relevant [] [] hopeful hopeless
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 max_relevant relevance_threshold
- (get_consts thy (SOME false) goal_ts)
+ |> iter 0 max_relevant threshold0
+ (get_consts thy (SOME false) goal_ts) []
|> tap (fn res => trace_msg (fn () =>
"Total relevant: " ^ Int.toString (length res)))
end
@@ -585,14 +593,12 @@
(* ATP invocation methods setup *)
(***************************************************************)
-fun relevant_facts full_types relevance_threshold relevance_decay max_relevant
+fun relevant_facts full_types (threshold0, threshold1) max_relevant
theory_relevant (relevance_override as {add, del, only})
(ctxt, (chained_ths, _)) hyp_ts concl_t =
let
- val relevance_decay =
- case relevance_decay of
- SOME x => x
- | NONE => 0.35 / Math.ln (Real.fromInt (max_relevant + 1))
+ val decay = 1.0 - Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
+ 1.0 / Real.fromInt (max_relevant + 1))
val add_thms = maps (ProofContext.get_fact ctxt) add
val reserved = reserved_isar_keyword_table ()
val axioms =
@@ -605,14 +611,13 @@
in
trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^
" theorems");
- (if relevance_threshold > 1.0 then
+ (if threshold0 > 1.0 orelse threshold0 > threshold1 then
[]
- else if relevance_threshold < 0.0 then
+ else if threshold0 < 0.0 then
axioms
else
- relevance_filter ctxt relevance_threshold relevance_decay max_relevant
- theory_relevant relevance_override axioms
- (concl_t :: hyp_ts))
+ relevance_filter ctxt threshold0 decay max_relevant 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 Wed Aug 25 17:49:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 25 19:41:18 2010 +0200
@@ -50,7 +50,7 @@
val params =
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
full_types = full_types, explicit_apply = explicit_apply,
- relevance_threshold = 1.1, relevance_decay = NONE, max_relevant = NONE,
+ relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
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) axioms
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 25 17:49:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 25 19:41:18 2010 +0200
@@ -67,8 +67,7 @@
("verbose", "false"),
("overlord", "false"),
("explicit_apply", "false"),
- ("relevance_threshold", "40"),
- ("relevance_decay", "smart"),
+ ("relevance_thresholds", "45 95"),
("max_relevant", "smart"),
("theory_relevant", "smart"),
("isar_proof", "false"),
@@ -156,6 +155,14 @@
SOME n => n
| NONE => error ("Parameter " ^ quote name ^
" must be assigned an integer value.")
+ fun lookup_int_pair name =
+ case lookup name of
+ NONE => (0, 0)
+ | SOME s => case s |> space_explode " " |> map Int.fromString of
+ [SOME n1, SOME n2] => (n1, n2)
+ | _ => error ("Parameter " ^ quote name ^
+ "must be assigned a pair of integer values \
+ \(e.g., \"60 95\")")
fun lookup_int_option name =
case lookup name of
SOME "smart" => NONE
@@ -166,11 +173,9 @@
val atps = lookup_string "atps" |> space_explode " "
val full_types = lookup_bool "full_types"
val explicit_apply = lookup_bool "explicit_apply"
- val relevance_threshold =
- 0.01 * Real.fromInt (lookup_int "relevance_threshold")
- val relevance_decay =
- lookup_int_option "relevance_decay"
- |> Option.map (fn n => 0.01 * Real.fromInt n)
+ val relevance_thresholds =
+ lookup_int_pair "relevance_thresholds"
+ |> pairself (fn n => 0.01 * Real.fromInt n)
val max_relevant = lookup_int_option "max_relevant"
val theory_relevant = lookup_bool_option "theory_relevant"
val isar_proof = lookup_bool "isar_proof"
@@ -179,8 +184,7 @@
in
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
full_types = full_types, explicit_apply = explicit_apply,
- relevance_threshold = relevance_threshold,
- relevance_decay = relevance_decay, max_relevant = max_relevant,
+ relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
theory_relevant = theory_relevant, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, timeout = timeout}
end