# HG changeset patch
# User blanchet
# Date 1406154240 -7200
# Node ID 3ab503b04bdbc0858e78af6247ccd9ecba9a1729
# Parent  97adb86619a48280c29bb45ae6d3b9b98ae791fa
stick to external proofs when invoking E, because they are more detailed and do not merge steps

diff -r 97adb86619a4 -r 3ab503b04bdb src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Thu Jul 24 00:24:00 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Thu Jul 24 00:24:00 2014 +0200
@@ -201,7 +201,7 @@
 for Alt-Ergo, set the
 environment variable \texttt{WHY3\_HOME} to the directory that contains the
 \texttt{why3} executable.
-Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.0 to 1.8,
+Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 1.8,
 LEO-II 1.3.4, Satallax 2.2 to 2.7, SPASS 3.8ds, and Vampire 0.6 to 3.0.%
 \footnote{Following the rewrite of Vampire, the counter for version numbers was
 reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, 2.6, and 3.0 are more
@@ -837,7 +837,7 @@
 variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof}
 executable and \texttt{E\_VERSION} to the version number (e.g., ``1.8''), or
 install the prebuilt E package from \download. Sledgehammer has been tested with
-versions 1.0 to 1.8.
+versions 1.6 to 1.8.
 
 \item[\labelitemi] \textbf{\textit{e\_males}:} E-MaLeS is a metaprover developed
 by Daniel K\"uhlwein that implements strategy scheduling on top of E. To use
diff -r 97adb86619a4 -r 3ab503b04bdb src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Jul 24 00:24:00 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Jul 24 00:24:00 2014 +0200
@@ -212,9 +212,8 @@
 
 (* E *)
 
-fun is_e_at_least_1_3 () = string_ord (getenv "E_VERSION", "1.3") <> LESS
-fun is_e_at_least_1_6 () = string_ord (getenv "E_VERSION", "1.6") <> LESS
 fun is_e_at_least_1_8 () = string_ord (getenv "E_VERSION", "1.8") <> LESS
+fun is_e_at_least_1_9 () = string_ord (getenv "E_VERSION", "1.9") <> LESS
 
 val e_smartN = "smart"
 val e_autoN = "auto"
@@ -286,29 +285,19 @@
        else "")
     end
 
-fun effective_e_selection_heuristic ctxt =
-  if is_e_at_least_1_3 () then Config.get ctxt e_selection_heuristic
-  else e_autoN
-
-fun e_kbo () = if is_e_at_least_1_3 () then "KBO6" else "KBO"
-
 val e_config : atp_config =
   {exec = (fn () => (["E_HOME"],
-     if is_e_at_least_1_8 () then ["eprover"] else ["eproof_ram", "eproof"])),
+     if is_e_at_least_1_9 () then ["eprover"] else ["eproof_ram", "eproof"])),
    arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout => fn file_name =>
      fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
        (if is_e_at_least_1_8 () then "--auto-schedule " else "") ^
        "--tstp-in --tstp-out --silent " ^
        e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
        e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
-       "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^
+       "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
        "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
-       (if is_e_at_least_1_8 () then
-          " --proof-object=1"
-        else
-          " --output-level=5" ^
-          (if is_e_at_least_1_6 () then " --pcl-shell-level=" ^ (if full_proof then "0" else "2")
-           else "")) ^
+       (if is_e_at_least_1_9 () then " --proof-object=3"
+        else " --output-level=5 --pcl-shell-level=" ^ (if full_proof then "0" else "2")) ^
        " " ^ file_name,
    proof_delims =
      [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
@@ -319,7 +308,7 @@
      known_szs_status_failures,
    prem_role = Conjecture,
    best_slices = fn ctxt =>
-     let val heuristic = effective_e_selection_heuristic ctxt in
+     let val heuristic = Config.get ctxt e_selection_heuristic in
        (* FUDGE *)
        if heuristic = e_smartN then
          [(0.15, (((128, meshN), FOF, "mono_tags??", combsN, false), e_fun_weightN)),