# HG changeset patch
# User blanchet
# Date 1308559262 -7200
# Node ID 423cd1ecf71410460615722d0051549af2ad58cb
# Parent  fb2713b803e69682c943347da66d30eb3ec80c58
optimized E's time slicing, based on latest exhaustive Judgment Day results

diff -r fb2713b803e6 -r 423cd1ecf714 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 20 10:41:02 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 20 10:41:02 2011 +0200
@@ -211,15 +211,14 @@
    prem_kind = Conjecture,
    formats = [FOF],
    best_slices = fn ctxt =>
-     (* FUDGE *)
      let val method = effective_e_weight_method ctxt in
+       (* FUDGE *)
        if method = e_smartN then
-         [(0.333, (true, (100, ["mangled_preds_heavy"], e_sym_offset_weightN))),
-          (0.333, (true, (800, ["poly_preds?"], e_autoN))),
-          (0.334, (true,
-             (200, ["mangled_tags!", "mangled_tags?"], e_fun_weightN)))]
+         [(0.333, (true, (200, ["mangled_preds"], e_sym_offset_weightN))),
+          (0.333, (true, (1000, ["mangled_preds?"], e_fun_weightN))),
+          (0.334, (true, (50, ["mangled_tags?"], e_sym_offset_weightN)))]
        else
-         [(1.0, (true, (200, ["mangled_tags!", "mangled_tags?"], method)))]
+         [(1.0, (true, (300, ["mangled_tags?"], method)))]
      end}
 
 val e = (eN, e_config)