# HG changeset patch
# User blanchet
# Date 1283174715 -7200
# Node ID ee36b983ca22a03bc1e8cb1cc135b9400ae9cb4c
# Parent  853a061af37dbc2b6d98cd198e59a2c5a3bb9202
fiddle with fact filter based on Mirabelle experiments

diff -r 853a061af37d -r ee36b983ca22 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 30 12:44:00 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 30 15:25:15 2010 +0200
@@ -155,7 +155,7 @@
         (Const x, ts) => do_const true x ts
       | (Free x, ts) => do_const false x ts
       | (Abs (_, _, t'), ts) =>
-        null ts ? add_pconst_to_table true (abs_name, [])
+        (null ts ? add_pconst_to_table true (abs_name, []))
         #> fold do_term (t' :: ts)
       | (_, ts) => fold do_term ts
     fun do_quantifier will_surely_be_skolemized body_t =
@@ -273,14 +273,16 @@
   else if String.isPrefix skolem_prefix s then skolem_weight
   else logx (pconst_freq (match_patterns o f) const_tab c)
 
-val rel_weight = generic_weight (!abs_rel_weight) 0.0 rel_log I
-val irrel_weight = generic_weight (!abs_irrel_weight) (!skolem_irrel_weight)
-                                  irrel_log swap
+fun rel_weight const_tab =
+  generic_weight (!abs_rel_weight) 0.0 rel_log I const_tab
+fun irrel_weight const_tab =
+  generic_weight (!abs_irrel_weight) (!skolem_irrel_weight) irrel_log swap
+                 const_tab
 
 (* FUDGE *)
-val theory_bonus = Unsynchronized.ref 0.5
-val local_bonus = Unsynchronized.ref 1.0
-val chained_bonus = Unsynchronized.ref 2.0
+val theory_bonus = Unsynchronized.ref 0.1
+val local_bonus = Unsynchronized.ref 0.2
+val chained_bonus = Unsynchronized.ref 1.5
 
 fun locality_bonus General = 0.0
   | locality_bonus Theory = !theory_bonus
@@ -348,7 +350,7 @@
 (* FUDGE *)
 val threshold_divisor = Unsynchronized.ref 2.0
 val ridiculous_threshold = Unsynchronized.ref 0.1
-val max_max_imperfect_fudge_factor = Unsynchronized.ref 0.5
+val max_max_imperfect_fudge_factor = Unsynchronized.ref 1.66
 
 fun relevance_filter ctxt threshold0 decay max_relevant theory_relevant
                      ({add, del, ...} : relevance_override) axioms goal_ts =
@@ -389,8 +391,7 @@
                                    candidates
               val rel_const_tab' =
                 rel_const_tab
-                |> fold (add_pconst_to_table false)
-                        (maps (snd o fst) accepts)
+                |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
               fun is_dirty (c, _) =
                 Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
               val (hopeful_rejects, hopeless_rejects) =
@@ -430,8 +431,8 @@
                 | NONE => axiom_weight loc const_tab rel_const_tab axiom_consts
 (* TODO: experiment
 val name = fst (fst (fst ax)) ()
-val _ = if String.isPrefix "lift.simps(3" name then
-tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight const_tab rel_const_tab axiom_consts))
+val _ = if name = "foo" then
+tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight loc const_tab rel_const_tab axiom_consts))
 else
 ()
 *)