# HG changeset patch
# User blanchet
# Date 1282816266 -7200
# Node ID 21a6f261595e3f43b96a5f9c1ad06d0a8c73be36
# Parent  3913f58d0fcc39c84694162b071c44e660ef4470
lower penalty for Skolem constants

diff -r 3913f58d0fcc -r 21a6f261595e src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 10:42:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 11:51:06 2010 +0200
@@ -105,7 +105,7 @@
   | string_for_super_pseudoconst (s, Tss) =
     s ^ "{" ^ commas (map string_for_pseudotypes Tss) ^ "}"
 
-val abs_prefix = "Sledgehammer.abs"
+val abs_name = "Sledgehammer.abs"
 val skolem_prefix = "Sledgehammer.sko"
 
 (* Add a pseudoconstant to the table, but a [] entry means a standard
@@ -135,7 +135,7 @@
       | Free (s, _) => add_pseudoconst_to_table also_skolems (s, [])
       | t1 $ t2 => fold do_term [t1, t2]
       | Abs (_, _, t') =>
-        do_term t' #> add_pseudoconst_to_table true (abs_prefix, [])
+        do_term t' #> add_pseudoconst_to_table true (abs_name, [])
       | _ => I
     fun do_quantifier will_surely_be_skolemized body_t =
       do_formula pos body_t
@@ -250,18 +250,15 @@
 fun irrel_log n = Math.ln (Real.fromInt n + 19.0) / 6.4
 
 (* FUDGE *)
-val skolem_weight = 1.0
 val abs_weight = 2.0
+val skolem_weight = 0.5
 
 (* Computes a constant's weight, as determined by its frequency. *)
 val rel_weight = rel_log oo pseudoconst_freq match_pseudotypes
 fun irrel_weight const_tab (c as (s, _)) =
-  if String.isPrefix skolem_prefix s then skolem_weight
-  else if String.isPrefix abs_prefix s then abs_weight
+  if s = abs_name then abs_weight
+  else if String.isPrefix skolem_prefix s then skolem_weight
   else irrel_log (pseudoconst_freq (match_pseudotypes o swap) const_tab c)
-(* TODO: experiment
-fun irrel_weight _ _ = 1.0
-*)
 
 (* FUDGE *)
 fun locality_multiplier General = 1.0