src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
changeset 50608 5977de2993ac
parent 50383 4274b25ff4e7
child 50985 23bb011a5832
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Thu Dec 20 15:51:24 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Thu Dec 20 15:51:27 2012 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4    val const_names_in_fact :
     1.5      theory -> (string * typ -> term list -> bool * term list) -> term
     1.6      -> string list
     1.7 -  val weight_mepo_facts : ('a * thm) list -> (('a * thm) * real) list
     1.8 +  val weight_mepo_facts : 'a list -> ('a * real) list
     1.9    val mepo_suggested_facts :
    1.10      Proof.context -> params -> string -> int -> relevance_fudge option
    1.11      -> term list -> term -> fact list -> fact list
    1.12 @@ -28,6 +28,7 @@
    1.13  struct
    1.14  
    1.15  open ATP_Problem_Generate
    1.16 +open Sledgehammer_Util
    1.17  open Sledgehammer_Fact
    1.18  open Sledgehammer_Provers
    1.19  
    1.20 @@ -509,10 +510,9 @@
    1.21                        "Total relevant: " ^ string_of_int (length accepts)))
    1.22    end
    1.23  
    1.24 -(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
    1.25  (* FUDGE *)
    1.26  fun weight_of_mepo_fact rank =
    1.27 -  Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
    1.28 +  Math.pow (0.62, log2 (Real.fromInt (rank + 1)))
    1.29  
    1.30  fun weight_mepo_facts facts =
    1.31    facts ~~ map weight_of_mepo_fact (0 upto length facts - 1)