# HG changeset patch # User blanchet # Date 1282758078 -7200 # Node ID ad577fd62ee46858252eaf49faad1ce02293516e # Parent 2b6333f78a9eba8a1088a5a1dd88fbf2ee71fb10 reorganize options regarding to the relevance threshold and decay diff -r 2b6333f78a9e -r ad577fd62ee4 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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" diff -r 2b6333f78a9e -r ad577fd62ee4 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- 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 diff -r 2b6333f78a9e -r ad577fd62ee4 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML --- 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 diff -r 2b6333f78a9e -r ad577fd62ee4 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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