--- a/src/HOL/TPTP/mash_export.ML Thu Aug 22 12:12:51 2013 +0200
+++ b/src/HOL/TPTP/mash_export.ML Thu Aug 22 12:12:52 2013 +0200
@@ -174,11 +174,29 @@
smart_dependencies_of ctxt params_opt access_facts name_tabs th
(SOME isar_deps)
val parents = if linearize then prevs else parents
+ fun extra_features_of (((_, stature), th), weight) =
+ [prop_of th]
+ |> features_of ctxt prover (theory_of_thm th) (num_old_facts + j)
+ const_tab stature
+ |> map (apsnd (fn r => weight * extra_feature_weight_factor * r))
val query =
if do_query then
- "? " ^ string_of_int max_suggs ^ " # " ^
- encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
- encode_features feats ^ "\n"
+ let
+ val extra_featss =
+ new_facts
+ |> drop (j - num_extra_feature_facts)
+ |> take num_extra_feature_facts
+ |> rev
+ |> weight_facts_steeply
+ |> map extra_features_of
+ val extra_feats =
+ fold_rev (union (op = o pairself fst)) extra_featss []
+ val query_feats = union (op = o pairself fst) extra_feats feats
+ in
+ "? " ^ string_of_int max_suggs ^ " # " ^
+ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
+ encode_features query_feats ^ "\n"
+ end
else
""
val update =
@@ -254,10 +272,10 @@
let
val (name, mash_suggs) =
extract_suggestions mash_line
- ||> weight_mash_facts
+ ||> weight_facts_steeply
val (name', mepo_suggs) =
extract_suggestions mepo_line
- ||> weight_mepo_facts
+ ||> weight_facts_steeply
val _ = if name = name' then () else error "Input files out of sync."
val mess =
[(mepo_weight, (mepo_suggs, [])),
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Aug 22 12:12:51 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Aug 22 12:12:52 2013 +0200
@@ -73,8 +73,10 @@
-> bool * string list
val attach_parents_to_facts :
('a * thm) list -> ('a * thm) list -> (string list * ('a * thm)) list
- val weight_mepo_facts : 'a list -> ('a * real) list
- val weight_mash_facts : 'a list -> ('a * real) list
+ val num_extra_feature_facts : int
+ val extra_feature_weight_factor : real
+ val weight_facts_smoothly : 'a list -> ('a * real) list
+ val weight_facts_steeply : 'a list -> ('a * real) list
val find_mash_suggestions :
Proof.context -> int -> string list -> ('b * thm) list -> ('b * thm) list
-> ('b * thm) list -> ('b * thm) list * ('b * thm) list
@@ -903,23 +905,23 @@
fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm
-(* FUDGE *)
-fun weight_of_mepo_fact rank =
- Math.pow (0.62, log2 (Real.fromInt (rank + 1)))
-
-fun weight_mepo_facts facts =
- facts ~~ map weight_of_mepo_fact (0 upto length facts - 1)
-
-val weight_raw_mash_facts = weight_mepo_facts
-val weight_mash_facts = weight_raw_mash_facts
+val num_extra_feature_facts = 10 (* FUDGE *)
+val extra_feature_weight_factor = 0.1
(* FUDGE *)
fun weight_of_proximity_fact rank =
Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0
-fun weight_proximity_facts facts =
+fun weight_facts_smoothly facts =
facts ~~ map weight_of_proximity_fact (0 upto length facts - 1)
+(* FUDGE *)
+fun steep_weight_of_fact rank =
+ Math.pow (0.62, log2 (Real.fromInt (rank + 1)))
+
+fun weight_facts_steeply facts =
+ facts ~~ map steep_weight_of_fact (0 upto length facts - 1)
+
val max_proximity_facts = 100
fun find_mash_suggestions _ _ [] _ _ raw_unknown = ([], raw_unknown)
@@ -933,8 +935,8 @@
|> take max_proximity_facts
val mess =
[(0.90 (* FUDGE *), (map (rpair 1.0) unknown_chained, [])),
- (0.08 (* FUDGE *), (weight_raw_mash_facts raw_mash, raw_unknown)),
- (0.02 (* FUDGE *), (weight_proximity_facts proximity, []))]
+ (0.08 (* FUDGE *), (weight_facts_steeply raw_mash, raw_unknown)),
+ (0.02 (* FUDGE *), (weight_facts_smoothly proximity, []))]
val unknown =
raw_unknown
|> fold (subtract (Thm.eq_thm_prop o pairself snd))
@@ -1289,11 +1291,11 @@
fun mepo () =
mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t
facts
- |> weight_mepo_facts
+ |> weight_facts_steeply
fun mash () =
mash_suggested_facts ctxt params prover (generous_max_facts max_facts)
hyp_ts concl_t facts
- |>> weight_mash_facts
+ |>> weight_facts_steeply
val mess =
(* the order is important for the "case" expression below *)
[] |> (if effective_fact_filter <> mepoN then