# HG changeset patch
# User blanchet
# Date 1378917503 -7200
# Node ID a2d2fa096e31392bbbe3aff26e1b31fafc710228
# Parent  f7e987ef730405404199d4ba286d4b9c3dec9e61
kick out totally hopeless facts after 5 iterations to speed things up

diff -r f7e987ef7304 -r a2d2fa096e31 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Sep 11 18:37:47 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Sep 11 18:38:23 2013 +0200
@@ -387,7 +387,9 @@
 (* High enough so that it isn't wrongly considered as very relevant (e.g., for E
    weights), but low enough so that it is unlikely to be truncated away if few
    facts are included. *)
-val special_fact_index = 45
+val special_fact_index = 45 (* FUDGE *)
+
+val really_hopeless_get_kicked_out_iter = 5 (* FUDGE *)
 
 fun relevance_filter ctxt thres0 decay max_facts is_built_in_const
         (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts
@@ -409,6 +411,9 @@
               [Chained, Assum, Local]
     fun iter j remaining_max thres rel_const_tab hopeless hopeful =
       let
+        val hopeless =
+          hopeless |> j = really_hopeless_get_kicked_out_iter
+                      ? filter_out (fn (_, w) => w < 0.001)
         fun relevant [] _ [] =
             (* Nothing has been added this iteration. *)
             if j = 0 andalso thres >= ridiculous_threshold then
@@ -421,7 +426,7 @@
             let
               val (accepts, more_rejects) =
                 take_most_relevant ctxt max_facts remaining_max fudge candidates
-              val sps = maps (snd o fst) accepts;
+              val sps = maps (snd o fst) accepts
               val rel_const_tab' =
                 rel_const_tab |> fold (add_pconst_to_table false) sps
               fun is_dirty (s, _) =