1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Jul 20 22:19:46 2012 +0200
1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Jul 20 22:19:46 2012 +0200
1.3 @@ -133,7 +133,7 @@
1.4 Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
1.5 hyp_ts concl_t
1.6 |> filter (is_appropriate_prop o prop_of o snd)
1.7 - |> Sledgehammer_MePo.iterative_relevant_facts ctxt params
1.8 + |> Sledgehammer_MePo.mepo_suggested_facts ctxt params
1.9 default_prover (the_default default_max_facts max_facts)
1.10 (SOME relevance_fudge) hyp_ts concl_t
1.11 |> map ((fn name => name ()) o fst o fst)
2.1 --- a/src/HOL/TPTP/atp_theory_export.ML Fri Jul 20 22:19:46 2012 +0200
2.2 +++ b/src/HOL/TPTP/atp_theory_export.ML Fri Jul 20 22:19:46 2012 +0200
2.3 @@ -115,7 +115,7 @@
2.4
2.5 fun all_non_tautological_facts_of thy css_table =
2.6 Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
2.7 - |> filter_out (Sledgehammer_MaSh.is_likely_tautology_or_too_meta o snd)
2.8 + |> filter_out (Sledgehammer_Fact.is_likely_tautology_or_too_meta o snd)
2.9
2.10 fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
2.11 let
3.1 --- a/src/HOL/TPTP/mash_eval.ML Fri Jul 20 22:19:46 2012 +0200
3.2 +++ b/src/HOL/TPTP/mash_eval.ML Fri Jul 20 22:19:46 2012 +0200
3.3 @@ -78,26 +78,28 @@
3.4 val isar_deps = isar_dependencies_of all_names th |> these
3.5 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
3.6 val mepo_facts =
3.7 - Sledgehammer_MePo.iterative_relevant_facts ctxt params prover
3.8 + Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
3.9 slack_max_facts NONE hyp_ts concl_t facts
3.10 - val mash_facts = facts |> suggested_facts suggs
3.11 + |> Sledgehammer_MePo.weight_mepo_facts
3.12 + val mash_facts = suggested_facts suggs facts
3.13 val mess = [(mepo_facts, []), (mash_facts, [])]
3.14 val mesh_facts = mesh_facts slack_max_facts mess
3.15 - val isar_facts = suggested_facts isar_deps facts
3.16 - fun prove ok heading facts =
3.17 + val isar_facts = suggested_facts (map (rpair 1.0) isar_deps) facts
3.18 + fun prove ok heading get facts =
3.19 let
3.20 val facts =
3.21 - facts
3.22 - |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
3.23 - |> take (the max_facts)
3.24 + facts |> map get
3.25 + |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts
3.26 + concl_t
3.27 + |> take (the max_facts)
3.28 val res as {outcome, ...} =
3.29 run_prover_for_mash ctxt params prover facts goal
3.30 val _ = if is_none outcome then ok := !ok + 1 else ()
3.31 in str_of_res heading facts res end
3.32 - val mepo_s = prove mepo_ok MePoN mepo_facts
3.33 - val mash_s = prove mash_ok MaShN mash_facts
3.34 - val mesh_s = prove mesh_ok MeshN mesh_facts
3.35 - val isar_s = prove isar_ok IsarN isar_facts
3.36 + val mepo_s = prove mepo_ok MePoN fst mepo_facts
3.37 + val mash_s = prove mash_ok MaShN fst mash_facts
3.38 + val mesh_s = prove mesh_ok MeshN I mesh_facts
3.39 + val isar_s = prove isar_ok IsarN fst isar_facts
3.40 in
3.41 ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
3.42 isar_s]
4.1 --- a/src/HOL/TPTP/mash_export.ML Fri Jul 20 22:19:46 2012 +0200
4.2 +++ b/src/HOL/TPTP/mash_export.ML Fri Jul 20 22:19:46 2012 +0200
4.3 @@ -179,7 +179,7 @@
4.4 let
4.5 val suggs =
4.6 old_facts
4.7 - |> Sledgehammer_MePo.iterative_relevant_facts ctxt params prover
4.8 + |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
4.9 max_relevant NONE hyp_ts concl_t
4.10 |> map (fn ((name, _), _) => name ())
4.11 val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n"
5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 20 22:19:46 2012 +0200
5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 20 22:19:46 2012 +0200
5.3 @@ -23,6 +23,7 @@
5.4 val fact_from_ref :
5.5 Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
5.6 -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
5.7 + val is_likely_tautology_or_too_meta : thm -> bool
5.8 val backquote_thm : thm -> string
5.9 val clasimpset_rule_table_of : Proof.context -> status Termtab.table
5.10 val maybe_instantiate_inducts :
5.11 @@ -210,6 +211,24 @@
5.12 is_that_fact thm
5.13 end
5.14
5.15 +fun is_likely_tautology_or_too_meta th =
5.16 + let
5.17 + val is_boring_const = member (op =) atp_widely_irrelevant_consts
5.18 + fun is_boring_bool t =
5.19 + not (exists_Const (not o is_boring_const o fst) t) orelse
5.20 + exists_type (exists_subtype (curry (op =) @{typ prop})) t
5.21 + fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t
5.22 + | is_boring_prop (@{const "==>"} $ t $ u) =
5.23 + is_boring_prop t andalso is_boring_prop u
5.24 + | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) =
5.25 + is_boring_prop t andalso is_boring_prop u
5.26 + | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) =
5.27 + is_boring_bool t andalso is_boring_bool u
5.28 + | is_boring_prop _ = true
5.29 + in
5.30 + is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th))
5.31 + end
5.32 +
5.33 fun hackish_string_for_term thy t =
5.34 Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
5.35 (print_mode_value ())) (Syntax.string_of_term_global thy) t
5.36 @@ -439,6 +458,7 @@
5.37 else
5.38 let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
5.39 all_facts ctxt ho_atp reserved add chained css
5.40 + |> filter_out (is_likely_tautology_or_too_meta o snd)
5.41 |> filter_out (member Thm.eq_thm_prop del o snd)
5.42 |> maybe_filter_no_atps ctxt
5.43 |> uniquify
6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:46 2012 +0200
6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:46 2012 +0200
6.3 @@ -218,7 +218,7 @@
6.4 val max_local_and_remote =
6.5 max_local_and_remote
6.6 |> (if String.isPrefix remote_prefix prover then apsnd else apfst)
6.7 - (Integer.add ~1)
6.8 + (Integer.add ~1)
6.9 in prover :: avoid_too_many_threads ctxt max_local_and_remote provers end
6.10
6.11 val max_default_remote_threads = 4
7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200
7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200
7.3 @@ -28,12 +28,12 @@
7.4 val escape_metas : string list -> string
7.5 val unescape_meta : string -> string
7.6 val unescape_metas : string -> string list
7.7 - val extract_query : string -> string * string list
7.8 + val extract_query : string -> string * (string * real) list
7.9 val nickname_of : thm -> string
7.10 - val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list
7.11 + val suggested_facts :
7.12 + (string * 'a) list -> ('b * thm) list -> (('b * thm) * 'a) list
7.13 val mesh_facts :
7.14 - int -> (('a * thm) list * ('a * thm) list) list -> ('a * thm) list
7.15 - val is_likely_tautology_or_too_meta : thm -> bool
7.16 + int -> ((('a * thm) * real) list * ('a * thm) list) list -> ('a * thm) list
7.17 val theory_ord : theory * theory -> order
7.18 val thm_ord : thm * thm -> order
7.19 val goal_of_thm : theory -> thm -> thm
7.20 @@ -52,13 +52,14 @@
7.21 val mash_REPROVE :
7.22 Proof.context -> bool -> (string * string list) list -> unit
7.23 val mash_QUERY :
7.24 - Proof.context -> bool -> int -> string list * string list -> string list
7.25 + Proof.context -> bool -> int -> string list * string list
7.26 + -> (string * real) list
7.27 val mash_unlearn : Proof.context -> unit
7.28 val mash_could_suggest_facts : unit -> bool
7.29 val mash_can_suggest_facts : Proof.context -> bool
7.30 - val mash_suggest_facts :
7.31 + val mash_suggested_facts :
7.32 Proof.context -> params -> string -> int -> term list -> term
7.33 - -> ('a * thm) list -> ('a * thm) list * ('a * thm) list
7.34 + -> ('a * thm) list -> (('a * thm) * real) list * ('a * thm) list
7.35 val mash_learn_proof :
7.36 Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
7.37 -> unit
7.38 @@ -132,9 +133,22 @@
7.39 val unescape_metas =
7.40 space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta
7.41
7.42 +fun extract_node line =
7.43 + case space_explode ":" line of
7.44 + [name, parents] => (unescape_meta name, unescape_metas parents)
7.45 + | _ => ("", [])
7.46 +
7.47 +fun extract_suggestion sugg =
7.48 + case space_explode "=" sugg of
7.49 + [name, weight] =>
7.50 + SOME (unescape_meta name, Real.fromString weight |> the_default 0.0)
7.51 + | _ => NONE
7.52 +
7.53 fun extract_query line =
7.54 case space_explode ":" line of
7.55 - [goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs)
7.56 + [goal, suggs] =>
7.57 + (unescape_meta goal,
7.58 + map_filter extract_suggestion (space_explode " " suggs))
7.59 | _ => ("", [])
7.60
7.61 fun parent_of_local_thm th =
7.62 @@ -165,31 +179,35 @@
7.63 let
7.64 fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact)
7.65 val tab = Symtab.empty |> fold add_fact facts
7.66 - in map_filter (Symtab.lookup tab) suggs end
7.67 + fun find_sugg (name, weight) =
7.68 + Symtab.lookup tab name |> Option.map (rpair weight)
7.69 + in map_filter find_sugg suggs end
7.70
7.71 -(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
7.72 -fun score x = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt x) + 15.0
7.73 +fun sum_avg [] = 0
7.74 + | sum_avg xs = Real.ceil (100000.0 * fold (curry (op +)) xs 0.0) div length xs
7.75
7.76 -fun sum_sq_avg [] = 0
7.77 - | sum_sq_avg xs =
7.78 - Real.ceil (100000.0 * fold (curry (op +) o score) xs 0.0) div length xs
7.79 +fun normalize_scores [] = []
7.80 + | normalize_scores ((fact, score) :: tail) =
7.81 + (fact, 1.0) :: map (apsnd (curry Real.* (1.0 / score))) tail
7.82
7.83 -fun mesh_facts max_facts [(selected, unknown)] =
7.84 - take max_facts selected @ take (max_facts - length selected) unknown
7.85 +fun mesh_facts max_facts [(sels, unks)] =
7.86 + map fst (take max_facts sels) @ take (max_facts - length sels) unks
7.87 | mesh_facts max_facts mess =
7.88 let
7.89 - val mess = mess |> map (apfst (`length))
7.90 + val mess = mess |> map (apfst (normalize_scores #> `length))
7.91 val fact_eq = Thm.eq_thm o pairself snd
7.92 + fun score_at sels = try (nth sels) #> Option.map snd
7.93 fun score_in fact ((sel_len, sels), unks) =
7.94 - case find_index (curry fact_eq fact) sels of
7.95 + case find_index (curry fact_eq fact o fst) sels of
7.96 ~1 => (case find_index (curry fact_eq fact) unks of
7.97 - ~1 => SOME sel_len
7.98 + ~1 => score_at sels sel_len
7.99 | _ => NONE)
7.100 - | j => SOME j
7.101 - fun score_of fact = mess |> map_filter (score_in fact) |> sum_sq_avg
7.102 - val facts = fold (union fact_eq o take max_facts o snd o fst) mess []
7.103 + | rank => score_at sels rank
7.104 + fun weight_of fact = mess |> map_filter (score_in fact) |> sum_avg
7.105 + val facts =
7.106 + fold (union fact_eq o map fst o take max_facts o snd o fst) mess []
7.107 in
7.108 - facts |> map (`score_of) |> sort (int_ord o swap o pairself fst)
7.109 + facts |> map (`weight_of) |> sort (int_ord o swap o pairself fst)
7.110 |> map snd |> take max_facts
7.111 end
7.112
7.113 @@ -198,24 +216,6 @@
7.114 val type_name_of = prefix "t"
7.115 val class_name_of = prefix "s"
7.116
7.117 -fun is_likely_tautology_or_too_meta th =
7.118 - let
7.119 - val is_boring_const = member (op =) atp_widely_irrelevant_consts
7.120 - fun is_boring_bool t =
7.121 - not (exists_Const (not o is_boring_const o fst) t) orelse
7.122 - exists_type (exists_subtype (curry (op =) @{typ prop})) t
7.123 - fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t
7.124 - | is_boring_prop (@{const "==>"} $ t $ u) =
7.125 - is_boring_prop t andalso is_boring_prop u
7.126 - | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) =
7.127 - is_boring_prop t andalso is_boring_prop u
7.128 - | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) =
7.129 - is_boring_bool t andalso is_boring_bool u
7.130 - | is_boring_prop _ = true
7.131 - in
7.132 - is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th))
7.133 - end
7.134 -
7.135 fun theory_ord p =
7.136 if Theory.eq_thy p then
7.137 EQUAL
7.138 @@ -280,10 +280,11 @@
7.139 if is_bad_const x args then ""
7.140 else mk_app (const_name_of s) (map (patternify (depth - 1)) args)
7.141 | _ => ""
7.142 + fun add_pattern depth t =
7.143 + case patternify depth t of "" => I | s => insert (op =) s
7.144 fun add_term_patterns ~1 _ = I
7.145 | add_term_patterns depth t =
7.146 - insert (op =) (patternify depth t)
7.147 - #> add_term_patterns (depth - 1) t
7.148 + add_pattern depth t #> add_term_patterns (depth - 1) t
7.149 val add_term = add_term_patterns term_max_depth
7.150 fun add_patterns t =
7.151 let val (head, args) = strip_comb t in
7.152 @@ -327,8 +328,8 @@
7.153 fun trim_dependencies deps =
7.154 if length deps <= max_dependencies then SOME deps else NONE
7.155
7.156 -fun isar_dependencies_of all_facts =
7.157 - thms_in_proof (SOME all_facts) #> trim_dependencies
7.158 +fun isar_dependencies_of all_names =
7.159 + thms_in_proof (SOME all_names) #> trim_dependencies
7.160
7.161 fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover
7.162 auto_level facts all_names th =
7.163 @@ -349,7 +350,7 @@
7.164 SOME ((name, status), th) => accum @ [((name, status), th)]
7.165 | NONE => accum (* shouldn't happen *)
7.166 val facts =
7.167 - facts |> iterative_relevant_facts ctxt params prover
7.168 + facts |> mepo_suggested_facts ctxt params prover
7.169 (max_facts |> the_default atp_dependency_default_max_fact)
7.170 NONE hyp_ts concl_t
7.171 |> fold (add_isar_dep facts) (these isar_deps)
7.172 @@ -432,7 +433,7 @@
7.173 "p " ^ escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
7.174
7.175 fun str_of_query (parents, feats) =
7.176 - "? " ^ escape_metas parents ^ "; " ^ escape_metas feats
7.177 + "? " ^ escape_metas parents ^ "; " ^ escape_metas feats ^ "\n"
7.178
7.179 fun mash_CLEAR ctxt =
7.180 let val path = mash_model_dir () |> Path.explode in
7.181 @@ -487,6 +488,13 @@
7.182 "Internal error when " ^ when ^ ":\n" ^
7.183 ML_Compiler.exn_message exn); def)
7.184
7.185 +fun graph_info G =
7.186 + string_of_int (length (Graph.keys G)) ^ " node(s), " ^
7.187 + string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^
7.188 + " edge(s), " ^
7.189 + string_of_int (length (Graph.minimals G)) ^ " minimal, " ^
7.190 + string_of_int (length (Graph.maximals G)) ^ " maximal"
7.191 +
7.192 type mash_state = {fact_G : unit Graph.T}
7.193
7.194 val empty_state = {fact_G = Graph.empty}
7.195 @@ -500,26 +508,27 @@
7.196 let val path = mash_state_path () in
7.197 (true,
7.198 case try File.read_lines path of
7.199 - SOME (version' :: fact_lines) =>
7.200 + SOME (version' :: node_lines) =>
7.201 let
7.202 fun add_edge_to name parent =
7.203 - Graph.default_node (parent, ())
7.204 - #> Graph.add_edge (parent, name)
7.205 - fun add_fact_line line =
7.206 - case extract_query line of
7.207 + Graph.default_node (parent, ()) #> Graph.add_edge (parent, name)
7.208 + fun add_node line =
7.209 + case extract_node line of
7.210 ("", _) => I (* shouldn't happen *)
7.211 | (name, parents) =>
7.212 - Graph.default_node (name, ())
7.213 - #> fold (add_edge_to name) parents
7.214 + Graph.default_node (name, ()) #> fold (add_edge_to name) parents
7.215 val fact_G =
7.216 try_graph ctxt "loading state" Graph.empty (fn () =>
7.217 - Graph.empty |> version' = version
7.218 - ? fold add_fact_line fact_lines)
7.219 - in {fact_G = fact_G} end
7.220 + Graph.empty |> version' = version ? fold add_node node_lines)
7.221 + in
7.222 + trace_msg ctxt (fn () =>
7.223 + "Loaded fact graph (" ^ graph_info fact_G ^ ")");
7.224 + {fact_G = fact_G}
7.225 + end
7.226 | _ => empty_state)
7.227 end
7.228
7.229 -fun save {fact_G} =
7.230 +fun save ctxt {fact_G} =
7.231 let
7.232 val path = mash_state_path ()
7.233 fun fact_line_for name parents =
7.234 @@ -529,7 +538,8 @@
7.235 append_fact name (Graph.Keys.dest parents)
7.236 in
7.237 File.write path (version ^ "\n");
7.238 - Graph.fold append_entry fact_G ()
7.239 + Graph.fold append_entry fact_G ();
7.240 + trace_msg ctxt (fn () => "Saved fact graph (" ^ graph_info fact_G ^ ")")
7.241 end
7.242
7.243 val global_state =
7.244 @@ -538,7 +548,7 @@
7.245 in
7.246
7.247 fun mash_map ctxt f =
7.248 - Synchronized.change global_state (load ctxt ##> (f #> tap save))
7.249 + Synchronized.change global_state (load ctxt ##> (f #> tap (save ctxt)))
7.250
7.251 fun mash_get ctxt =
7.252 Synchronized.change_result global_state (load ctxt #> `snd)
7.253 @@ -567,9 +577,11 @@
7.254 if Symtab.defined tab name then
7.255 let
7.256 val new = (Graph.all_preds fact_G [name], name)
7.257 - fun not_ancestor (_, x) (yp, _) = not (member (op =) yp x)
7.258 - val maxs = maxs |> filter (fn max => not_ancestor max new)
7.259 - val maxs = maxs |> forall (not_ancestor new) maxs ? cons new
7.260 + fun is_ancestor (_, x) (yp, _) = member (op =) yp x
7.261 + val maxs = maxs |> filter (fn max => not (is_ancestor max new))
7.262 + val maxs =
7.263 + if exists (is_ancestor new) maxs then maxs
7.264 + else new :: filter_out (fn max => is_ancestor max new) maxs
7.265 in find_maxes (name :: seen) maxs names end
7.266 else
7.267 find_maxes (name :: seen) maxs
7.268 @@ -585,8 +597,8 @@
7.269 fun is_fact_in_graph fact_G (_, th) =
7.270 can (Graph.get_node fact_G) (nickname_of th)
7.271
7.272 -fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
7.273 - concl_t facts =
7.274 +fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
7.275 + concl_t facts =
7.276 let
7.277 val thy = Proof_Context.theory_of ctxt
7.278 val fact_G = #fact_G (mash_get ctxt)
7.279 @@ -756,13 +768,13 @@
7.280 n
7.281 else
7.282 let
7.283 - fun score_of (_, th) =
7.284 + fun priority_of (_, th) =
7.285 random_range 0 (1000 * max_dependencies)
7.286 - 500 * (th |> isar_dependencies_of all_names
7.287 |> Option.map length
7.288 |> the_default max_dependencies)
7.289 val old_facts =
7.290 - old_facts |> map (`score_of)
7.291 + old_facts |> map (`priority_of)
7.292 |> sort (int_ord o pairself fst)
7.293 |> map snd
7.294 val (reps, (n, _, _)) =
7.295 @@ -850,13 +862,14 @@
7.296 ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
7.297 (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
7.298 |> take max_facts
7.299 - fun iter () =
7.300 - iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts
7.301 - concl_t facts
7.302 + fun mepo () =
7.303 + facts |> mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts
7.304 + concl_t
7.305 + |> weight_mepo_facts
7.306 fun mash () =
7.307 - mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts
7.308 + mash_suggested_facts ctxt params prover max_facts hyp_ts concl_t facts
7.309 val mess =
7.310 - [] |> (if fact_filter <> mashN then cons (iter (), []) else I)
7.311 + [] |> (if fact_filter <> mashN then cons (mepo (), []) else I)
7.312 |> (if fact_filter <> mepoN then cons (mash ()) else I)
7.313 in
7.314 mesh_facts max_facts mess
8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Fri Jul 20 22:19:46 2012 +0200
8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Fri Jul 20 22:19:46 2012 +0200
8.3 @@ -18,9 +18,10 @@
8.4 val const_names_in_fact :
8.5 theory -> (string * typ -> term list -> bool * term list) -> term
8.6 -> string list
8.7 - val iterative_relevant_facts :
8.8 + val mepo_suggested_facts :
8.9 Proof.context -> params -> string -> int -> relevance_fudge option
8.10 -> term list -> term -> fact list -> fact list
8.11 + val weight_mepo_facts : fact list -> (fact * real) list
8.12 end;
8.13
8.14 structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =
8.15 @@ -508,7 +509,7 @@
8.16 "Total relevant: " ^ string_of_int (length accepts)))
8.17 end
8.18
8.19 -fun iterative_relevant_facts ctxt
8.20 +fun mepo_suggested_facts ctxt
8.21 ({fact_thresholds = (thres0, thres1), ...} : params) prover
8.22 max_facts fudge hyp_ts concl_t facts =
8.23 let
8.24 @@ -534,4 +535,11 @@
8.25 (concl_t |> theory_constify fudge (Context.theory_name thy)))
8.26 end
8.27
8.28 +(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
8.29 +fun weight_of_fact rank =
8.30 + Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
8.31 +
8.32 +fun weight_mepo_facts facts =
8.33 + facts ~~ map weight_of_fact (0 upto length facts - 1)
8.34 +
8.35 end;