# 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)