--- a/src/Doc/Sledgehammer/document/root.tex Thu Aug 11 13:23:00 2022 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Aug 12 15:35:07 2022 +0200
@@ -109,8 +109,9 @@
Vampire \cite{riazanov-voronkov-2002}, Waldmeister \cite{waldmeister}, and
Zipperposition \cite{cruanes-2014}. The ATPs are run either locally or remotely
via the System\-On\-TPTP web service \cite{sutcliffe-2000}. The supported SMT
-solvers are CVC4 \cite{cvc4}, veriT \cite{bouton-et-al-2009}, and Z3
-\cite{de-moura-2008}. These are always run locally.
+solvers are CVC4 \cite{cvc4}, cvc5 \cite{barbosa-et-al-cvc5}, veriT
+\cite{bouton-et-al-2009}, and Z3 \cite{de-moura-2008}. These are always run
+locally.
The problem passed to the external provers (or solvers) consists of your current
goal together with a heuristic selection of hundreds of facts (theorems) from the
@@ -151,15 +152,15 @@
and Zipperposition can be run locally; in addition, agsyHOL, Alt-Ergo, E,
iProver, LEO-II, Leo-III, Satallax, Vampire, Waldmeister, and Zipperposition are
available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers
-CVC4, veriT, and Z3 can be run locally.
+CVC4, cvc5, veriT, and Z3 can be run locally.
There are three main ways to install automatic provers on your machine:
\begin{sloppy}
\begin{enum}
\item[\labelitemi] If you installed an official Isabelle package, it should
-already include properly set up executables for CVC4, E, SPASS, Vampire, veriT,
-Z3, and Zipperposition ready to use.
+already include properly set up executables for CVC4, cvc5, E, SPASS, Vampire,
+veriT, Z3, and Zipperposition ready to use.
\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC4, E,
SPASS, Vampire, veriT, Z3, and Zipperposition binary packages from \download.
@@ -191,10 +192,11 @@
\texttt{LEO3\_VERSION}, \texttt{SATALLAX\_VERSION}, or
\texttt{ZIPPERPOSITION\_VERSION} to the prover's version number (e.g., ``3.6'').
-Similarly, if you want to install CVC4, veriT, or Z3, set the environment
-variable \texttt{CVC4\_\allowbreak SOLVER}, \texttt{ISABELLE\_\allowbreak VERIT},
+Similarly, if you want to install CVC4, cvc5, veriT, or Z3, set the environment
+variable \texttt{CVC4\_\allowbreak SOLVER}, \texttt{CVC5\_\allowbreak SOLVER},
+\texttt{ISABELLE\_\allowbreak VERIT},
or \texttt{Z3\_SOLVER} to the complete path of the executable, \emph{including
-the file name}. Ideally, also set \texttt{CVC4\_VERSION},
+the file name}. Ideally, also set \texttt{CVC4\_VERSION}, \texttt{CVC5\_VERSION},
\texttt{VERIT\_VERSION}, or \texttt{Z3\_VERSION} to the solver's version number
(e.g., ``4.4.0'').
\end{enum}
@@ -673,11 +675,16 @@
requires Alt-Ergo 0.95.2 and Why3 0.83.
\item[\labelitemi] \textbf{\textit{cvc4}:} CVC4 is an SMT solver developed by
-Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc4}. To use CVC4,
+Barrett et al.\ \cite{cvc4}. To use CVC4,
set the environment variable \texttt{CVC4\_SOLVER} to the complete path of the
executable, including the file name, or install the prebuilt CVC4 package from
\download.
+\item[\labelitemi] \textbf{\textit{cvc5}:} cvc5 is an SMT solver developed by
+Barbosa et al.\ \cite{barbosa-et-al-cvc5}. To use cvc5,
+set the environment variable \texttt{CVC5\_SOLVER} to the complete path of the
+executable, including the file name.
+
\item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover
developed by Stephan Schulz \cite{schulz-2019}. To use E, set the environment
variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof}
@@ -776,10 +783,10 @@
version of Zipperposition runs on Geoff Sutcliffe's Miami servers.
\end{enum}
-By default, Sledgehammer runs a subset of CVC4, E, SPASS, Vampire, veriT, and
-Z3 in parallel, either locally or remotely---depending on the number of
-processor cores available and on which provers are actually installed. It is
-generally desirable to run several provers in parallel.
+By default, Sledgehammer runs a subset of CVC4, E, SPASS, Vampire, veriT, Z3,
+and Zipperposition in parallel, either locally or remotely---depending on the
+number of processor cores available and on which provers are actually installed.
+It is generally beneficial to run several provers in parallel.
\opnodefault{prover}{string}
Alias for \textit{provers}.