tuned weights -- keep same relative values, but use 1.0 as the least weight
authorblanchet
Mon Dec 17 22:06:28 2012 +0100 (2012-12-17)
changeset 505844fff0898cc0e
parent 50583 681edd111e9b
child 50585 306c7b807e13
tuned weights -- keep same relative values, but use 1.0 as the least weight
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 17 22:06:28 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 17 22:06:28 2012 +0100
     1.3 @@ -464,15 +464,15 @@
     1.4              |> map snd |> take max_facts
     1.5      end
     1.6  
     1.7 -fun thy_feature_of s = ("y" ^ s, 0.5 (* FUDGE *))
     1.8 -fun const_feature_of s = ("c" ^ s, 4.0 (* FUDGE *))
     1.9 -fun free_feature_of s = ("f" ^ s, 5.0 (* FUDGE *))
    1.10 -fun type_feature_of s = ("t" ^ s, 0.5 (* FUDGE *))
    1.11 -fun class_feature_of s = ("s" ^ s, 0.25 (* FUDGE *))
    1.12 -fun status_feature_of status = (string_of_status status, 0.5 (* FUDGE *))
    1.13 -val local_feature = ("local", 2.0 (* FUDGE *))
    1.14 -val lams_feature = ("lams", 0.5 (* FUDGE *))
    1.15 -val skos_feature = ("skos", 0.5 (* FUDGE *))
    1.16 +fun thy_feature_of s = ("y" ^ s, 2.0 (* FUDGE *))
    1.17 +fun const_feature_of s = ("c" ^ s, 16.0 (* FUDGE *))
    1.18 +fun free_feature_of s = ("f" ^ s, 20.0 (* FUDGE *))
    1.19 +fun type_feature_of s = ("t" ^ s, 2.0 (* FUDGE *))
    1.20 +fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *))
    1.21 +fun status_feature_of status = (string_of_status status, 2.0 (* FUDGE *))
    1.22 +val local_feature = ("local", 8.0 (* FUDGE *))
    1.23 +val lams_feature = ("lams", 2.0 (* FUDGE *))
    1.24 +val skos_feature = ("skos", 2.0 (* FUDGE *))
    1.25  
    1.26  fun theory_ord p =
    1.27    if Theory.eq_thy p then