# HG changeset patch
# User blanchet
# Date 1626100215 -7200
# Node ID 34c8cf767fa3fdc881afcdfa86ed9c55fc0ab2c5
# Parent  ca2a35c0fe6e9e2c5c5a359e1bdbb3ca83b7fc73
adjusted E setup to avoid generating FOOL with 2.5 (where 'ite' is missing)

diff -r ca2a35c0fe6e -r 34c8cf767fa3 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Mon Jul 12 11:41:02 2021 +0000
+++ b/src/Doc/Sledgehammer/document/root.tex	Mon Jul 12 16:30:15 2021 +0200
@@ -189,22 +189,15 @@
 \texttt{eprover} (and/or \texttt{eproof} or \texttt{eproof\_ram}),
 \texttt{leo}, \texttt{leo3}, or \texttt{satallax} executable;
 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.6 to 2.0, LEO-II 1.3.4, Leo-III
-1.1, and Satallax 2.7. Since the ATPs' output formats are neither documented
-nor stable, other versions might not work well with Sledgehammer. Ideally, you
+directory that contains the \texttt{why3} executable. Ideally, you
 should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
 \texttt{LEO3\_VERSION}, or \texttt{SATALLAX\_VERSION} to the prover's version
-number (e.g., ``2.7''); this might help Sledgehammer invoke the prover
-optimally.
+number (e.g., ``3.6'').
 
 Similarly, if you want to install CVC3, CVC4, veriT, or Z3, set the environment
 variable \texttt{CVC3\_\allowbreak SOLVER}, \texttt{CVC4\_\allowbreak SOLVER},
 \texttt{VERIT\_\allowbreak SOLVER}, or \texttt{Z3\_SOLVER} to the complete path
-of the executable, \emph{including the file name}. Sledgehammer has been tested
-with CVC3 2.2 and 2.4.1, CVC4 1.5-prerelease, veriT 2020.10-rmx, and Z3 4.3.2.
-Since Z3's output format is somewhat unstable, other versions of the solver
-might not work well with Sledgehammer. Ideally, also set
+of the executable, \emph{including the file name}. Ideally, also set
 \texttt{CVC3\_VERSION}, \texttt{CVC4\_VERSION}, \texttt{VERIT\_VERSION}, or
 \texttt{Z3\_VERSION} to the solver's version number (e.g., ``4.4.0'').
 \end{enum}
diff -r ca2a35c0fe6e -r 34c8cf767fa3 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Jul 12 11:41:02 2021 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Jul 12 16:30:15 2021 +0200
@@ -289,12 +289,11 @@
    best_slices = fn ctxt =>
      let
        val heuristic = Config.get ctxt e_selection_heuristic
-       val modern = string_ord (getenv "E_VERSION", "2.3") <> LESS
        val (format, enc) =
-         if modern then
-           (THF (With_FOOL, Monomorphic, THF_Lambda_Free), "mono_native_higher_fool")
+         if string_ord (getenv "E_VERSION", "2.6") <> LESS then
+           (THF (With_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher_fool")
          else
-           (TFF (Without_FOOL, Monomorphic), "mono_native")
+           (THF (With_FOOL, Monomorphic, THF_Lambda_Free), "mono_native_higher")
      in
        (* FUDGE *)
        if heuristic = e_smartN then