better weight functions for MePo/MaSh etc.
authorblanchet
Thu Dec 20 15:51:27 2012 +0100 (2012-12-20)
changeset 506085977de2993ac
parent 50607 e928f8647302
child 50609 1d8dae3257f0
better weight functions for MePo/MaSh etc.
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 20 15:51:24 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 20 15:51:27 2012 +0100
     1.3 @@ -58,7 +58,7 @@
     1.4    val prover_dependencies_of :
     1.5      Proof.context -> params -> string -> int -> fact list -> string Symtab.table
     1.6      -> thm -> bool * string list option
     1.7 -  val weight_mash_facts : ('a * thm) list -> (('a * thm) * real) list
     1.8 +  val weight_mash_facts : 'a list -> ('a * real) list
     1.9    val find_mash_suggestions :
    1.10      int -> (Symtab.key * 'a) list -> ('b * thm) list -> ('b * thm) list
    1.11      -> ('b * thm) list -> ('b * thm) list * ('b * thm) list
    1.12 @@ -727,7 +727,6 @@
    1.13  fun is_fact_in_graph fact_G (_, th) =
    1.14    can (Graph.get_node fact_G) (nickname_of th)
    1.15  
    1.16 -(* use MePo weights for now *)
    1.17  val weight_raw_mash_facts = weight_mepo_facts
    1.18  val weight_mash_facts = weight_raw_mash_facts
    1.19  
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Thu Dec 20 15:51:24 2012 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Thu Dec 20 15:51:27 2012 +0100
     2.3 @@ -18,7 +18,7 @@
     2.4    val const_names_in_fact :
     2.5      theory -> (string * typ -> term list -> bool * term list) -> term
     2.6      -> string list
     2.7 -  val weight_mepo_facts : ('a * thm) list -> (('a * thm) * real) list
     2.8 +  val weight_mepo_facts : 'a list -> ('a * real) list
     2.9    val mepo_suggested_facts :
    2.10      Proof.context -> params -> string -> int -> relevance_fudge option
    2.11      -> term list -> term -> fact list -> fact list
    2.12 @@ -28,6 +28,7 @@
    2.13  struct
    2.14  
    2.15  open ATP_Problem_Generate
    2.16 +open Sledgehammer_Util
    2.17  open Sledgehammer_Fact
    2.18  open Sledgehammer_Provers
    2.19  
    2.20 @@ -509,10 +510,9 @@
    2.21                        "Total relevant: " ^ string_of_int (length accepts)))
    2.22    end
    2.23  
    2.24 -(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
    2.25  (* FUDGE *)
    2.26  fun weight_of_mepo_fact rank =
    2.27 -  Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
    2.28 +  Math.pow (0.62, log2 (Real.fromInt (rank + 1)))
    2.29  
    2.30  fun weight_mepo_facts facts =
    2.31    facts ~~ map weight_of_mepo_fact (0 upto length facts - 1)
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Dec 20 15:51:24 2012 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Dec 20 15:51:27 2012 +0100
     3.3 @@ -7,6 +7,7 @@
     3.4  signature SLEDGEHAMMER_UTIL =
     3.5  sig
     3.6    val sledgehammerN : string
     3.7 +  val log2 : real -> real
     3.8    val plural_s : int -> string
     3.9    val serial_commas : string -> string list -> string list
    3.10    val simplify_spaces : string -> string
    3.11 @@ -32,6 +33,10 @@
    3.12  
    3.13  val sledgehammerN = "sledgehammer"
    3.14  
    3.15 +val log10_2 = Math.log10 2.0
    3.16 +
    3.17 +fun log2 n = Math.log10 n / log10_2
    3.18 +
    3.19  fun plural_s n = if n = 1 then "" else "s"
    3.20  
    3.21  val serial_commas = Try.serial_commas