# HG changeset patch # User blanchet # Date 1356015087 -3600 # Node ID 5977de2993ac43e0496ed028348edb01443c7c88 # Parent e928f86473023b3556367acc895bcd9a96955a3e better weight functions for MePo/MaSh etc. diff -r e928f8647302 -r 5977de2993ac src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Dec 20 15:51:24 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Dec 20 15:51:27 2012 +0100 @@ -58,7 +58,7 @@ val prover_dependencies_of : Proof.context -> params -> string -> int -> fact list -> string Symtab.table -> thm -> bool * string list option - val weight_mash_facts : ('a * thm) list -> (('a * thm) * real) list + val weight_mash_facts : 'a list -> ('a * real) list val find_mash_suggestions : int -> (Symtab.key * 'a) list -> ('b * thm) list -> ('b * thm) list -> ('b * thm) list -> ('b * thm) list * ('b * thm) list @@ -727,7 +727,6 @@ fun is_fact_in_graph fact_G (_, th) = can (Graph.get_node fact_G) (nickname_of th) -(* use MePo weights for now *) val weight_raw_mash_facts = weight_mepo_facts val weight_mash_facts = weight_raw_mash_facts diff -r e928f8647302 -r 5977de2993ac src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Thu Dec 20 15:51:24 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Thu Dec 20 15:51:27 2012 +0100 @@ -18,7 +18,7 @@ val const_names_in_fact : theory -> (string * typ -> term list -> bool * term list) -> term -> string list - val weight_mepo_facts : ('a * thm) list -> (('a * thm) * real) list + val weight_mepo_facts : 'a list -> ('a * real) list val mepo_suggested_facts : Proof.context -> params -> string -> int -> relevance_fudge option -> term list -> term -> fact list -> fact list @@ -28,6 +28,7 @@ struct open ATP_Problem_Generate +open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_Provers @@ -509,10 +510,9 @@ "Total relevant: " ^ string_of_int (length accepts))) end -(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *) (* FUDGE *) fun weight_of_mepo_fact rank = - Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0 + 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) diff -r e928f8647302 -r 5977de2993ac src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Dec 20 15:51:24 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Dec 20 15:51:27 2012 +0100 @@ -7,6 +7,7 @@ signature SLEDGEHAMMER_UTIL = sig val sledgehammerN : string + val log2 : real -> real val plural_s : int -> string val serial_commas : string -> string list -> string list val simplify_spaces : string -> string @@ -32,6 +33,10 @@ val sledgehammerN = "sledgehammer" +val log10_2 = Math.log10 2.0 + +fun log2 n = Math.log10 n / log10_2 + fun plural_s n = if n = 1 then "" else "s" val serial_commas = Try.serial_commas