# HG changeset patch
# User blanchet
# Date 1377267266 -7200
# Node ID 4b9df3461edae5b8927a235a85a5bfc06430085c
# Parent  c8369b691d04a27c6d1559906c0ea6b5fcfe301c
thread information about when a constant became relevant through MePo -- the information is not used yet but could help fight starvation in the (ITP) world

diff -r c8369b691d04 -r 4b9df3461eda src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Aug 23 16:02:32 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Aug 23 16:14:26 2013 +0200
@@ -311,10 +311,10 @@
   s = pseudo_abs_name orelse String.isPrefix pseudo_skolem_prefix s orelse
   String.isSuffix theory_const_suffix s
 
-fun fact_weight fudge stature const_tab relevant_consts chained_consts
-                fact_consts =
-  case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts)
-                   ||> filter_out (pconst_hyper_mem swap relevant_consts) of
+fun fact_weight fudge stature const_tab rel_const_tab rel_const_iter_tab
+                chained_const_tab fact_consts =
+  case fact_consts |> List.partition (pconst_hyper_mem I rel_const_tab)
+                   ||> filter_out (pconst_hyper_mem swap rel_const_tab) of
     ([], _) => 0.0
   | (rel, irrel) =>
     if forall (forall (is_odd_const_name o fst)) [rel, irrel] then
@@ -327,7 +327,8 @@
         val irrel_weight =
           ~ (stature_bonus fudge stature)
           |> fold (curry (op +)
-                   o irrel_pconst_weight fudge const_tab chained_consts) irrel
+                   o irrel_pconst_weight fudge const_tab chained_const_tab)
+                  irrel
         val res = rel_weight / (rel_weight + irrel_weight)
       in if Real.isFinite res then res else 0.0 end
 
@@ -400,30 +401,36 @@
                             | _ => NONE)
     val chained_const_tab = Symtab.empty |> fold (add_pconsts true) chained_ts
     val goal_const_tab =
-      Symtab.empty |> fold (add_pconsts true) hyp_ts
-                   |> add_pconsts false concl_t
+      Symtab.empty
+      |> fold (add_pconsts true) hyp_ts
+      |> add_pconsts false concl_t
       |> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab)
       |> fold (if_empty_replace_with_scope thy is_built_in_const facts)
               [Chained, Assum, Local]
-    fun iter j remaining_max thres rel_const_tab hopeless hopeful =
+    val goal_const_iter_tab = goal_const_tab |> Symtab.map (K (K ~1))
+    fun iter j remaining_max thres rel_const_tab rel_const_iter_tab hopeless
+             hopeful =
       let
         fun relevant [] _ [] =
             (* Nothing has been added this iteration. *)
             if j = 0 andalso thres >= ridiculous_threshold then
               (* First iteration? Try again. *)
               iter 0 max_facts (thres / threshold_divisor) rel_const_tab
-                   hopeless hopeful
+                   rel_const_iter_tab hopeless hopeful
             else
               []
           | relevant candidates rejects [] =
             let
               val (accepts, more_rejects) =
                 take_most_relevant ctxt max_facts remaining_max fudge candidates
+              val sps = maps (snd o fst) accepts;
               val rel_const_tab' =
-                rel_const_tab
-                |> 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
+                rel_const_tab |> fold (add_pconst_to_table false) sps
+              val rel_const_iter_tab' =
+                rel_const_iter_tab
+                |> fold (fn (s, _) => Symtab.default (s, j)) sps
+              fun is_dirty (s, _) =
+                Symtab.lookup rel_const_tab' s <> Symtab.lookup rel_const_tab s
               val (hopeful_rejects, hopeless_rejects) =
                  (rejects @ hopeless, ([], []))
                  |-> fold (fn (ax as (_, consts), old_weight) =>
@@ -441,7 +448,8 @@
               val remaining_max = remaining_max - length accepts
             in
               trace_msg ctxt (fn () => "New or updated constants: " ^
-                  commas (rel_const_tab' |> Symtab.dest
+                  commas (rel_const_tab'
+                          |> Symtab.dest
                           |> subtract (op =) (rel_const_tab |> Symtab.dest)
                           |> map string_of_hyper_pconst));
               map (fst o fst) accepts @
@@ -449,7 +457,7 @@
                  []
                else
                  iter (j + 1) remaining_max thres rel_const_tab'
-                      hopeless_rejects hopeful_rejects)
+                      rel_const_iter_tab' hopeless_rejects hopeful_rejects)
             end
           | relevant candidates rejects
                      (((ax as (((_, stature), _), fact_consts)), cached_weight)
@@ -458,8 +466,9 @@
               val weight =
                 case cached_weight of
                   SOME w => w
-                | NONE => fact_weight fudge stature const_tab rel_const_tab
-                                      chained_const_tab fact_consts
+                | NONE =>
+                  fact_weight fudge stature const_tab rel_const_tab
+                              rel_const_iter_tab chained_const_tab fact_consts
             in
               if weight >= thres then
                 relevant ((ax, weight) :: candidates) rejects hopeful
@@ -470,7 +479,8 @@
           trace_msg ctxt (fn () =>
               "ITERATION " ^ string_of_int j ^ ": current threshold: " ^
               Real.toString thres ^ ", constants: " ^
-              commas (rel_const_tab |> Symtab.dest
+              commas (rel_const_tab
+                      |> Symtab.dest
                       |> filter (curry (op <>) [] o snd)
                       |> map string_of_hyper_pconst));
           relevant [] [] hopeful
@@ -499,7 +509,7 @@
          |> insert_into_facts accepts
   in
     facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
-          |> iter 0 max_facts thres0 goal_const_tab []
+          |> iter 0 max_facts thres0 goal_const_tab goal_const_iter_tab []
           |> insert_special_facts
           |> tap (fn accepts => trace_msg ctxt (fn () =>
                       "Total relevant: " ^ string_of_int (length accepts)))