1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 25 17:49:52 2010 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 25 19:41:18 2010 +0200
1.3 @@ -18,8 +18,7 @@
1.4 atps: string list,
1.5 full_types: bool,
1.6 explicit_apply: bool,
1.7 - relevance_threshold: real,
1.8 - relevance_decay: real option,
1.9 + relevance_thresholds: real * real,
1.10 max_relevant: int option,
1.11 theory_relevant: bool option,
1.12 isar_proof: bool,
1.13 @@ -86,8 +85,7 @@
1.14 atps: string list,
1.15 full_types: bool,
1.16 explicit_apply: bool,
1.17 - relevance_threshold: real,
1.18 - relevance_decay: real option,
1.19 + relevance_thresholds: real * real,
1.20 max_relevant: int option,
1.21 theory_relevant: bool option,
1.22 isar_proof: bool,
1.23 @@ -213,8 +211,8 @@
1.24 known_failures, default_max_relevant, default_theory_relevant,
1.25 explicit_forall, use_conjecture_for_hypotheses}
1.26 ({debug, verbose, overlord, full_types, explicit_apply,
1.27 - relevance_threshold, relevance_decay, max_relevant, theory_relevant,
1.28 - isar_proof, isar_shrink_factor, timeout, ...} : params)
1.29 + relevance_thresholds, max_relevant, theory_relevant, isar_proof,
1.30 + isar_shrink_factor, timeout, ...} : params)
1.31 minimize_command
1.32 ({subgoal, goal, relevance_override, axioms} : problem) =
1.33 let
1.34 @@ -230,13 +228,13 @@
1.35 case axioms of
1.36 SOME axioms => axioms
1.37 | NONE =>
1.38 - (relevant_facts full_types relevance_threshold relevance_decay
1.39 + (relevant_facts full_types relevance_thresholds
1.40 (the_default default_max_relevant max_relevant)
1.41 (the_default default_theory_relevant theory_relevant)
1.42 relevance_override goal hyp_ts concl_t
1.43 |> tap ((fn n => print_v (fn () =>
1.44 - "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
1.45 - " for " ^ quote atp_name ^ ".")) o length))
1.46 + "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
1.47 + " for " ^ quote atp_name ^ ".")) o length))
1.48
1.49 (* path to unique problem file *)
1.50 val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 25 17:49:52 2010 +0200
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 25 19:41:18 2010 +0200
2.3 @@ -15,7 +15,7 @@
2.4 Proof.context -> unit Symtab.table -> thm list -> Facts.ref
2.5 -> ((unit -> string * bool) * (bool * thm)) list
2.6 val relevant_facts :
2.7 - bool -> real -> real option -> int -> bool -> relevance_override
2.8 + bool -> real * real -> int -> bool -> relevance_override
2.9 -> Proof.context * (thm list * 'a) -> term list -> term
2.10 -> ((string * bool) * thm) list
2.11 end;
2.12 @@ -265,47 +265,45 @@
2.13 type annotated_thm =
2.14 ((unit -> string * bool) * thm) * (string * pseudotype list) list
2.15
2.16 -fun rev_compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
2.17 -
2.18 -fun take_best max (new_pairs : (annotated_thm * real) list) =
2.19 +fun take_best max (candidates : (annotated_thm * real) list) =
2.20 let
2.21 val ((perfect, more_perfect), imperfect) =
2.22 - new_pairs |> List.partition (fn (_, w) => w > 0.99999)
2.23 - |>> chop (max - 1) ||> sort rev_compare_pairs
2.24 - val (accepted, rejected) =
2.25 + candidates |> List.partition (fn (_, w) => w > 0.99999) |>> chop (max - 1)
2.26 + ||> sort (Real.compare o swap o pairself snd)
2.27 + val (accepts, rejects) =
2.28 case more_perfect @ imperfect of
2.29 [] => (perfect, [])
2.30 | (q :: qs) => (q :: perfect, qs)
2.31 in
2.32 trace_msg (fn () => "Number of candidates: " ^
2.33 - string_of_int (length new_pairs));
2.34 + string_of_int (length candidates));
2.35 trace_msg (fn () => "Effective threshold: " ^
2.36 - Real.toString (#2 (hd accepted)));
2.37 + Real.toString (#2 (hd accepts)));
2.38 trace_msg (fn () => "Actually passed: " ^
2.39 - (accepted |> map (fn (((name, _), _), weight) =>
2.40 - fst (name ()) ^ " [" ^ Real.toString weight ^ "]")
2.41 - |> commas));
2.42 - (map #1 accepted, rejected)
2.43 + (accepts |> map (fn (((name, _), _), weight) =>
2.44 + fst (name ()) ^ " [" ^ Real.toString weight ^ "]")
2.45 + |> commas));
2.46 + (accepts, rejects)
2.47 end
2.48
2.49 val threshold_divisor = 2.0
2.50 val ridiculous_threshold = 0.1
2.51
2.52 -fun relevance_filter ctxt relevance_threshold relevance_decay max_relevant
2.53 - theory_relevant ({add, del, ...} : relevance_override)
2.54 - axioms goal_ts =
2.55 +fun relevance_filter ctxt threshold0 decay max_relevant theory_relevant
2.56 + ({add, del, ...} : relevance_override) axioms goal_ts =
2.57 let
2.58 val thy = ProofContext.theory_of ctxt
2.59 val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
2.60 Symtab.empty
2.61 val add_thms = maps (ProofContext.get_fact ctxt) add
2.62 val del_thms = maps (ProofContext.get_fact ctxt) del
2.63 - fun iter j max threshold rel_const_tab rest =
2.64 + fun iter j max threshold rel_const_tab hopeless hopeful =
2.65 let
2.66 fun game_over rejects =
2.67 if j = 0 andalso threshold >= ridiculous_threshold then
2.68 (* First iteration? Try again. *)
2.69 - iter 0 max (threshold / threshold_divisor) rel_const_tab rejects
2.70 + iter 0 max (threshold / threshold_divisor) rel_const_tab hopeless
2.71 + hopeful
2.72 else
2.73 (* Add "add:" facts. *)
2.74 if null add_thms then
2.75 @@ -314,35 +312,45 @@
2.76 map_filter (fn ((p as (_, th), _), _) =>
2.77 if member Thm.eq_thm add_thms th then SOME p
2.78 else NONE) rejects
2.79 - fun relevant ([], rejects) [] =
2.80 + fun relevant [] rejects [] hopeless =
2.81 (* Nothing has been added this iteration. *)
2.82 - game_over (map (apsnd SOME) rejects)
2.83 - | relevant (new_pairs, rejects) [] =
2.84 + game_over (map (apsnd SOME) (rejects @ hopeless))
2.85 + | relevant candidates rejects [] hopeless =
2.86 let
2.87 - val (new_rels, more_rejects) = take_best max new_pairs
2.88 + val (accepts, more_rejects) = take_best max candidates
2.89 val rel_const_tab' =
2.90 - rel_const_tab |> fold add_const_to_table (maps snd new_rels)
2.91 + rel_const_tab
2.92 + |> fold add_const_to_table (maps (snd o fst) accepts)
2.93 fun is_dirty (c, _) =
2.94 Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
2.95 - val rejects =
2.96 - more_rejects @ rejects
2.97 - |> map (fn (ax as (_, consts), old_weight) =>
2.98 - (ax, if exists is_dirty consts then NONE
2.99 - else SOME old_weight))
2.100 - val threshold = threshold + (1.0 - threshold) * relevance_decay
2.101 - val max = max - length new_rels
2.102 + val (hopeful_rejects, hopeless_rejects) =
2.103 + (rejects @ hopeless, ([], []))
2.104 + |-> fold (fn (ax as (_, consts), old_weight) =>
2.105 + if exists is_dirty consts then
2.106 + apfst (cons (ax, NONE))
2.107 + else
2.108 + apsnd (cons (ax, old_weight)))
2.109 + |>> append (more_rejects
2.110 + |> map (fn (ax as (_, consts), old_weight) =>
2.111 + (ax, if exists is_dirty consts then NONE
2.112 + else SOME old_weight)))
2.113 + val threshold = threshold + (1.0 - threshold) * decay
2.114 + val max = max - length accepts
2.115 in
2.116 trace_msg (fn () => "New or updated constants: " ^
2.117 commas (rel_const_tab' |> Symtab.dest
2.118 |> subtract (op =) (Symtab.dest rel_const_tab)
2.119 |> map string_for_super_pseudoconst));
2.120 - map #1 new_rels @
2.121 - (if max = 0 then game_over rejects
2.122 - else iter (j + 1) max threshold rel_const_tab' rejects)
2.123 + map (fst o fst) accepts @
2.124 + (if max = 0 then
2.125 + game_over (hopeful_rejects @ map (apsnd SOME) hopeless_rejects)
2.126 + else
2.127 + iter (j + 1) max threshold rel_const_tab' hopeless_rejects
2.128 + hopeful_rejects)
2.129 end
2.130 - | relevant (new_rels, rejects)
2.131 + | relevant candidates rejects
2.132 (((ax as ((name, th), axiom_consts)), cached_weight)
2.133 - :: rest) =
2.134 + :: hopeful) hopeless =
2.135 let
2.136 val weight =
2.137 case cached_weight of
2.138 @@ -350,9 +358,9 @@
2.139 | NONE => axiom_weight const_tab rel_const_tab axiom_consts
2.140 in
2.141 if weight >= threshold then
2.142 - relevant ((ax, weight) :: new_rels, rejects) rest
2.143 + relevant ((ax, weight) :: candidates) rejects hopeful hopeless
2.144 else
2.145 - relevant (new_rels, (ax, weight) :: rejects) rest
2.146 + relevant candidates ((ax, weight) :: rejects) hopeful hopeless
2.147 end
2.148 in
2.149 trace_msg (fn () =>
2.150 @@ -361,13 +369,13 @@
2.151 commas (rel_const_tab |> Symtab.dest
2.152 |> filter (curry (op <>) [] o snd)
2.153 |> map string_for_super_pseudoconst));
2.154 - relevant ([], []) rest
2.155 + relevant [] [] hopeful hopeless
2.156 end
2.157 in
2.158 axioms |> filter_out (member Thm.eq_thm del_thms o snd)
2.159 |> map (rpair NONE o pair_consts_axiom theory_relevant thy)
2.160 - |> iter 0 max_relevant relevance_threshold
2.161 - (get_consts thy (SOME false) goal_ts)
2.162 + |> iter 0 max_relevant threshold0
2.163 + (get_consts thy (SOME false) goal_ts) []
2.164 |> tap (fn res => trace_msg (fn () =>
2.165 "Total relevant: " ^ Int.toString (length res)))
2.166 end
2.167 @@ -585,14 +593,12 @@
2.168 (* ATP invocation methods setup *)
2.169 (***************************************************************)
2.170
2.171 -fun relevant_facts full_types relevance_threshold relevance_decay max_relevant
2.172 +fun relevant_facts full_types (threshold0, threshold1) max_relevant
2.173 theory_relevant (relevance_override as {add, del, only})
2.174 (ctxt, (chained_ths, _)) hyp_ts concl_t =
2.175 let
2.176 - val relevance_decay =
2.177 - case relevance_decay of
2.178 - SOME x => x
2.179 - | NONE => 0.35 / Math.ln (Real.fromInt (max_relevant + 1))
2.180 + val decay = 1.0 - Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
2.181 + 1.0 / Real.fromInt (max_relevant + 1))
2.182 val add_thms = maps (ProofContext.get_fact ctxt) add
2.183 val reserved = reserved_isar_keyword_table ()
2.184 val axioms =
2.185 @@ -605,14 +611,13 @@
2.186 in
2.187 trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^
2.188 " theorems");
2.189 - (if relevance_threshold > 1.0 then
2.190 + (if threshold0 > 1.0 orelse threshold0 > threshold1 then
2.191 []
2.192 - else if relevance_threshold < 0.0 then
2.193 + else if threshold0 < 0.0 then
2.194 axioms
2.195 else
2.196 - relevance_filter ctxt relevance_threshold relevance_decay max_relevant
2.197 - theory_relevant relevance_override axioms
2.198 - (concl_t :: hyp_ts))
2.199 + relevance_filter ctxt threshold0 decay max_relevant theory_relevant
2.200 + relevance_override axioms (concl_t :: hyp_ts))
2.201 |> map (apfst (fn f => f ())) |> sort_wrt (fst o fst)
2.202 end
2.203
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 25 17:49:52 2010 +0200
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 25 19:41:18 2010 +0200
3.3 @@ -50,7 +50,7 @@
3.4 val params =
3.5 {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
3.6 full_types = full_types, explicit_apply = explicit_apply,
3.7 - relevance_threshold = 1.1, relevance_decay = NONE, max_relevant = NONE,
3.8 + relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
3.9 theory_relevant = NONE, isar_proof = isar_proof,
3.10 isar_shrink_factor = isar_shrink_factor, timeout = timeout}
3.11 val axioms = maps (fn (n, ths) => map (pair n) ths) axioms
4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 25 17:49:52 2010 +0200
4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 25 19:41:18 2010 +0200
4.3 @@ -67,8 +67,7 @@
4.4 ("verbose", "false"),
4.5 ("overlord", "false"),
4.6 ("explicit_apply", "false"),
4.7 - ("relevance_threshold", "40"),
4.8 - ("relevance_decay", "smart"),
4.9 + ("relevance_thresholds", "45 95"),
4.10 ("max_relevant", "smart"),
4.11 ("theory_relevant", "smart"),
4.12 ("isar_proof", "false"),
4.13 @@ -156,6 +155,14 @@
4.14 SOME n => n
4.15 | NONE => error ("Parameter " ^ quote name ^
4.16 " must be assigned an integer value.")
4.17 + fun lookup_int_pair name =
4.18 + case lookup name of
4.19 + NONE => (0, 0)
4.20 + | SOME s => case s |> space_explode " " |> map Int.fromString of
4.21 + [SOME n1, SOME n2] => (n1, n2)
4.22 + | _ => error ("Parameter " ^ quote name ^
4.23 + "must be assigned a pair of integer values \
4.24 + \(e.g., \"60 95\")")
4.25 fun lookup_int_option name =
4.26 case lookup name of
4.27 SOME "smart" => NONE
4.28 @@ -166,11 +173,9 @@
4.29 val atps = lookup_string "atps" |> space_explode " "
4.30 val full_types = lookup_bool "full_types"
4.31 val explicit_apply = lookup_bool "explicit_apply"
4.32 - val relevance_threshold =
4.33 - 0.01 * Real.fromInt (lookup_int "relevance_threshold")
4.34 - val relevance_decay =
4.35 - lookup_int_option "relevance_decay"
4.36 - |> Option.map (fn n => 0.01 * Real.fromInt n)
4.37 + val relevance_thresholds =
4.38 + lookup_int_pair "relevance_thresholds"
4.39 + |> pairself (fn n => 0.01 * Real.fromInt n)
4.40 val max_relevant = lookup_int_option "max_relevant"
4.41 val theory_relevant = lookup_bool_option "theory_relevant"
4.42 val isar_proof = lookup_bool "isar_proof"
4.43 @@ -179,8 +184,7 @@
4.44 in
4.45 {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
4.46 full_types = full_types, explicit_apply = explicit_apply,
4.47 - relevance_threshold = relevance_threshold,
4.48 - relevance_decay = relevance_decay, max_relevant = max_relevant,
4.49 + relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
4.50 theory_relevant = theory_relevant, isar_proof = isar_proof,
4.51 isar_shrink_factor = isar_shrink_factor, timeout = timeout}
4.52 end