lower penalty for Skolem constants
authorblanchet
Thu Aug 26 11:51:06 2010 +0200 (2010-08-26)
changeset 3881621a6f261595e
parent 38753 3913f58d0fcc
child 38817 bf27c24ba224
lower penalty for Skolem constants
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 10:42:22 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 11:51:06 2010 +0200
     1.3 @@ -105,7 +105,7 @@
     1.4    | string_for_super_pseudoconst (s, Tss) =
     1.5      s ^ "{" ^ commas (map string_for_pseudotypes Tss) ^ "}"
     1.6  
     1.7 -val abs_prefix = "Sledgehammer.abs"
     1.8 +val abs_name = "Sledgehammer.abs"
     1.9  val skolem_prefix = "Sledgehammer.sko"
    1.10  
    1.11  (* Add a pseudoconstant to the table, but a [] entry means a standard
    1.12 @@ -135,7 +135,7 @@
    1.13        | Free (s, _) => add_pseudoconst_to_table also_skolems (s, [])
    1.14        | t1 $ t2 => fold do_term [t1, t2]
    1.15        | Abs (_, _, t') =>
    1.16 -        do_term t' #> add_pseudoconst_to_table true (abs_prefix, [])
    1.17 +        do_term t' #> add_pseudoconst_to_table true (abs_name, [])
    1.18        | _ => I
    1.19      fun do_quantifier will_surely_be_skolemized body_t =
    1.20        do_formula pos body_t
    1.21 @@ -250,18 +250,15 @@
    1.22  fun irrel_log n = Math.ln (Real.fromInt n + 19.0) / 6.4
    1.23  
    1.24  (* FUDGE *)
    1.25 -val skolem_weight = 1.0
    1.26  val abs_weight = 2.0
    1.27 +val skolem_weight = 0.5
    1.28  
    1.29  (* Computes a constant's weight, as determined by its frequency. *)
    1.30  val rel_weight = rel_log oo pseudoconst_freq match_pseudotypes
    1.31  fun irrel_weight const_tab (c as (s, _)) =
    1.32 -  if String.isPrefix skolem_prefix s then skolem_weight
    1.33 -  else if String.isPrefix abs_prefix s then abs_weight
    1.34 +  if s = abs_name then abs_weight
    1.35 +  else if String.isPrefix skolem_prefix s then skolem_weight
    1.36    else irrel_log (pseudoconst_freq (match_pseudotypes o swap) const_tab c)
    1.37 -(* TODO: experiment
    1.38 -fun irrel_weight _ _ = 1.0
    1.39 -*)
    1.40  
    1.41  (* FUDGE *)
    1.42  fun locality_multiplier General = 1.0