tuning
authorblanchet
Wed Dec 05 13:25:06 2012 +0100 (2012-12-05 ago)
changeset 50382cb564ff43c28
parent 50361 3ae4376cb739
child 50383 4274b25ff4e7
tuning
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Dec 05 11:05:34 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Dec 05 13:25:06 2012 +0100
     1.3 @@ -57,9 +57,10 @@
     1.4    val atp_dependencies_of :
     1.5      Proof.context -> params -> string -> int -> fact list -> unit 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 mash_suggested_facts :
     1.9      Proof.context -> params -> string -> int -> term list -> term
    1.10 -    -> fact list -> (fact * real) list * fact list
    1.11 +    -> fact list -> fact list * fact list
    1.12    val mash_learn_proof :
    1.13      Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
    1.14      -> unit
    1.15 @@ -473,11 +474,11 @@
    1.16      EQUAL => string_ord (pairself Context.theory_name p)
    1.17    | order => order
    1.18  
    1.19 -fun thm_ord thp =
    1.20 -  case theory_ord (pairself theory_of_thm thp) of
    1.21 +fun thm_ord p =
    1.22 +  case theory_ord (pairself theory_of_thm p) of
    1.23      EQUAL =>
    1.24      (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
    1.25 -    string_ord (pairself nickname_of (swap thp))
    1.26 +    string_ord (pairself nickname_of (swap p))
    1.27    | ord => ord
    1.28  
    1.29  val freezeT = Type.legacy_freeze_type
    1.30 @@ -708,6 +709,8 @@
    1.31  (* factor that controls whether unknown global facts should be included *)
    1.32  val include_unk_global_factor = 15
    1.33  
    1.34 +val weight_mash_facts = weight_mepo_facts (* use MePo weights for now *)
    1.35 +
    1.36  fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
    1.37                           concl_t facts =
    1.38    let
    1.39 @@ -740,8 +743,7 @@
    1.40        ([], unk_global)
    1.41        |> include_unk_global_factor * length unk_global <= max_facts ? swap
    1.42    in
    1.43 -    (interleave max_facts (chained @ unk_local @ small_unk_global) sels
    1.44 -     |> weight_mepo_facts (* use MePo weights for now *),
    1.45 +    (interleave max_facts (chained @ unk_local @ small_unk_global) sels,
    1.46       big_unk_global)
    1.47    end
    1.48  
    1.49 @@ -1034,11 +1036,12 @@
    1.50           (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
    1.51          |> take max_facts
    1.52        fun mepo () =
    1.53 -        facts |> mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts
    1.54 -                                      concl_t
    1.55 -              |> weight_mepo_facts
    1.56 +        mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t
    1.57 +                             facts
    1.58 +        |> weight_mepo_facts
    1.59        fun mash () =
    1.60          mash_suggested_facts ctxt params prover max_facts hyp_ts concl_t facts
    1.61 +        |>> weight_mash_facts
    1.62        val mess =
    1.63          [] |> (if fact_filter <> mashN then cons (mepo (), []) else I)
    1.64             |> (if fact_filter <> mepoN then cons (mash ()) else I)
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Dec 05 11:05:34 2012 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Dec 05 13:25:06 2012 +0100
     2.3 @@ -18,10 +18,10 @@
     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 mepo_suggested_facts :
     2.9      Proof.context -> params -> string -> int -> relevance_fudge option
    2.10      -> term list -> term -> fact list -> fact list
    2.11 -  val weight_mepo_facts : ('a * thm) list -> (('a * thm) * real) list
    2.12  end;
    2.13  
    2.14  structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =
    2.15 @@ -509,6 +509,12 @@
    2.16                        "Total relevant: " ^ string_of_int (length accepts)))
    2.17    end
    2.18  
    2.19 +(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
    2.20 +fun weight_of_fact rank = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
    2.21 +
    2.22 +fun weight_mepo_facts facts =
    2.23 +  facts ~~ map weight_of_fact (0 upto length facts - 1)
    2.24 +
    2.25  fun mepo_suggested_facts ctxt
    2.26          ({fact_thresholds = (thres0, thres1), ...} : params) prover
    2.27          max_facts fudge hyp_ts concl_t facts =
    2.28 @@ -535,10 +541,4 @@
    2.29             (concl_t |> theory_constify fudge (Context.theory_name thy)))
    2.30    end
    2.31  
    2.32 -(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
    2.33 -fun weight_of_fact rank = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
    2.34 -
    2.35 -fun weight_mepo_facts facts =
    2.36 -  facts ~~ map weight_of_fact (0 upto length facts - 1)
    2.37 -
    2.38  end;