# HG changeset patch
# User blanchet
# Date 1298280708 -3600
# Node ID 56dcd46ddf7a167fffd2f114b21ba85b12d0cb10
# Parent  7c7b68b06c1a037d704b58b42318962f936b4e39
give more weight to Frees than to Consts in relevance filter

diff -r 7c7b68b06c1a -r 56dcd46ddf7a src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon Feb 21 10:29:13 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon Feb 21 10:31:48 2011 +0100
@@ -11,12 +11,15 @@
   | NONE => default_value
 
 fun extract_relevance_fudge args
-      {allow_ext, worse_irrel_freq, higher_order_irrel_weight, abs_rel_weight,
-       abs_irrel_weight, skolem_irrel_weight, theory_const_rel_weight,
-       theory_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus,
-       local_bonus, assum_bonus, chained_bonus, max_imperfect,
-       max_imperfect_exp, threshold_divisor, ridiculous_threshold} =
+      {allow_ext, local_const_multiplier, worse_irrel_freq,
+       higher_order_irrel_weight, abs_rel_weight, abs_irrel_weight,
+       skolem_irrel_weight, theory_const_rel_weight, theory_const_irrel_weight,
+       intro_bonus, elim_bonus, simp_bonus, local_bonus, assum_bonus,
+       chained_bonus, max_imperfect, max_imperfect_exp, threshold_divisor,
+       ridiculous_threshold} =
   {allow_ext = allow_ext,
+   local_const_multiplier =
+       get args "local_const_multiplier" local_const_multiplier,
    worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq,
    higher_order_irrel_weight =
        get args "higher_order_irrel_weight" higher_order_irrel_weight,
diff -r 7c7b68b06c1a -r 56dcd46ddf7a src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Feb 21 10:29:13 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Feb 21 10:31:48 2011 +0100
@@ -11,6 +11,7 @@
 
   type relevance_fudge =
     {allow_ext : bool,
+     local_const_multiplier : real,
      worse_irrel_freq : real,
      higher_order_irrel_weight : real,
      abs_rel_weight : real,
@@ -67,6 +68,7 @@
 
 type relevance_fudge =
   {allow_ext : bool,
+   local_const_multiplier : real,
    worse_irrel_freq : real,
    higher_order_irrel_weight : real,
    abs_rel_weight : real,
@@ -413,23 +415,34 @@
     * pow_int higher_order_irrel_weight (order - 1)
   end
 
-(* Computes a constant's weight, as determined by its frequency. *)
-fun generic_pconst_weight abs_weight skolem_weight theory_const_weight
-                          weight_for f const_tab (c as (s, PType (m, _))) =
-  if s = abs_name then abs_weight
-  else if String.isPrefix skolem_prefix s then skolem_weight
-  else if String.isSuffix theory_const_suffix s then theory_const_weight
-  else weight_for m (pconst_freq (match_ptype o f) const_tab c)
+fun multiplier_for_const_name local_const_multiplier s =
+  if String.isSubstring "." s then 1.0 else local_const_multiplier
 
-fun rel_pconst_weight ({abs_rel_weight, theory_const_rel_weight, ...}
-                       : relevance_fudge) const_tab =
-  generic_pconst_weight abs_rel_weight 0.0 theory_const_rel_weight
-                        rel_weight_for I const_tab
-fun irrel_pconst_weight (fudge as {abs_irrel_weight, skolem_irrel_weight,
+(* Computes a constant's weight, as determined by its frequency. *)
+fun generic_pconst_weight local_const_multiplier abs_weight skolem_weight
+                          theory_const_weight weight_for f const_tab
+                          (c as (s, PType (m, _))) =
+  if s = abs_name then
+    abs_weight
+  else if String.isPrefix skolem_prefix s then
+    skolem_weight
+  else if String.isSuffix theory_const_suffix s then
+    theory_const_weight
+  else
+    multiplier_for_const_name local_const_multiplier s
+    * weight_for m (pconst_freq (match_ptype o f) const_tab c)
+
+fun rel_pconst_weight ({local_const_multiplier, abs_rel_weight,
+                        theory_const_rel_weight, ...} : relevance_fudge)
+                      const_tab =
+  generic_pconst_weight local_const_multiplier abs_rel_weight 0.0
+                        theory_const_rel_weight rel_weight_for I const_tab
+fun irrel_pconst_weight (fudge as {local_const_multiplier, abs_irrel_weight,
+                                   skolem_irrel_weight,
                                    theory_const_irrel_weight, ...}) const_tab =
-  generic_pconst_weight abs_irrel_weight skolem_irrel_weight
-                        theory_const_irrel_weight (irrel_weight_for fudge) swap
-                        const_tab
+  generic_pconst_weight local_const_multiplier abs_irrel_weight
+                        skolem_irrel_weight theory_const_irrel_weight
+                        (irrel_weight_for fudge) swap const_tab
 
 fun locality_bonus (_ : relevance_fudge) General = 0.0
   | locality_bonus {intro_bonus, ...} Intro = intro_bonus
diff -r 7c7b68b06c1a -r 56dcd46ddf7a src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Feb 21 10:29:13 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Feb 21 10:31:48 2011 +0100
@@ -161,6 +161,7 @@
 (* FUDGE *)
 val atp_relevance_fudge =
   {allow_ext = true,
+   local_const_multiplier = 1.5,
    worse_irrel_freq = 100.0,
    higher_order_irrel_weight = 1.05,
    abs_rel_weight = 0.5,
@@ -182,6 +183,7 @@
 (* FUDGE (FIXME) *)
 val smt_relevance_fudge =
   {allow_ext = false,
+   local_const_multiplier = #local_const_multiplier atp_relevance_fudge,
    worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge,
    higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge,
    abs_rel_weight = #abs_rel_weight atp_relevance_fudge,