# HG changeset patch # User blanchet # Date 1354924130 -3600 # Node ID e8f2d7a3ef5302297c95f9e92d4cc8044a94d529 # Parent 960a3429615c21e640573f75ee5209c0cc11c2fb tweak MaSh fudge factors diff -r 960a3429615c -r e8f2d7a3ef53 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Dec 08 00:48:50 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Dec 08 00:48:50 2012 +0100 @@ -465,8 +465,8 @@ end fun thy_feature_of s = ("y" ^ s, 0.5 (* FUDGE *)) -fun const_feature_of s = ("c" ^ s, 1.0 (* FUDGE *)) -fun free_feature_of s = ("f" ^ s, 2.0 (* FUDGE *)) +fun const_feature_of s = ("c" ^ s, 4.0 (* FUDGE *)) +fun free_feature_of s = ("f" ^ s, 5.0 (* FUDGE *)) fun type_feature_of s = ("t" ^ s, 0.5 (* FUDGE *)) fun class_feature_of s = ("s" ^ s, 0.25 (* FUDGE *)) fun status_feature_of status = (string_of_status status, 0.5 (* FUDGE *)) @@ -722,9 +722,6 @@ fun is_fact_in_graph fact_G (_, th) = can (Graph.get_node fact_G) (nickname_of th) -(* factor that controls whether unknown global facts should be included *) -val include_unk_global_factor = 15 - (* use MePo weights for now *) val weight_raw_mash_facts = weight_mepo_facts val weight_mash_facts = weight_raw_mash_facts @@ -745,9 +742,9 @@ |> map fst val proximity = facts |> sort (thm_ord o pairself snd o swap) val mess = - [(0.8000 (* FUDGE *), (map (rpair 1.0) chained, [])), - (0.1333 (* FUDGE *), (weight_raw_mash_facts raw_mash, unknown)), - (0.0667 (* FUDGE *), (weight_proximity_facts proximity, []))] + [(0.80 (* FUDGE *), (map (rpair 1.0) chained, [])), + (0.16 (* FUDGE *), (weight_raw_mash_facts raw_mash, unknown)), + (0.04 (* FUDGE *), (weight_proximity_facts proximity, []))] in mesh_facts max_facts mess end fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts