--- a/src/Doc/Sledgehammer/document/root.tex Thu Jun 12 17:02:02 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Jun 12 17:02:03 2014 +0200
@@ -110,9 +110,9 @@
\cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, and
Waldmeister \cite{waldmeister}. The ATPs are run either locally or remotely via
the System\-On\-TPTP web service \cite{sutcliffe-2000}. In addition to the ATPs,
-a selection of the SMT solvers CVC3 \cite{cvc3}, Yices \cite{yices}, and Z3
-\cite{z3} are run by default; these are run either locally or (for CVC3 and Z3)
-on a server at the TU M\"unchen.
+a selection of the SMT solvers CVC3 \cite{cvc3} and Z3 \cite{z3} are run by
+default; these are run either locally or (for CVC3 and Z3) on a server at the
+TU M\"unchen.
The problem passed to the automatic provers consists of your current goal
together with a heuristic selection of hundreds of facts (theorems) from the
@@ -157,8 +157,8 @@
be run locally; in addition, AgsyHOL, E, E-SInE, E-ToFoF, iProver, iProver-Eq,
LEO-II, Satallax, SNARK, Vampire, and Waldmeister are available remotely via
System\-On\-TPTP \cite{sutcliffe-2000}. If you want better performance, you
-should at least install E and SPASS locally. The SMT solvers CVC3, Yices, and Z3
-can be run locally.
+should at least install E and SPASS locally. The SMT solvers CVC3 and Z3 can be
+run locally.
There are three main ways to install automatic provers on your machine:
@@ -166,8 +166,8 @@
\begin{enum}
\item[\labelitemi] If you installed an official Isabelle package, it should
already include properly setup executables for CVC3, E, SPASS, and Z3, ready to use.%
-\footnote{Vampire's and Yices's licenses prevent us from doing the same for
-these otherwise remarkable tools.}
+\footnote{Vampire's license prevents us from doing the same for
+this otherwise remarkable tool.}
For Z3, you must additionally set the variable
\texttt{Z3\_NON\_COMMERCIAL} to \textit{yes} to confirm that you are a
noncommercial user---either in the environment in which Isabelle is
@@ -214,17 +214,13 @@
\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``3.0'').
Similarly, if you want to build CVC3, or found a
-Yices or Z3 executable somewhere (e.g.,
-\url{http://yices.csl.sri.com/download.shtml} or
-\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html}),
-set the environment variable \texttt{CVC3\_\allowbreak SOLVER},
-\texttt{YICES\_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,
-Yices 1.0.28 and 1.0.33, and Z3 4.3.2. Since the SMT solvers' output
-formats are somewhat unstable, other versions of the solvers might not work well
-with Sledgehammer. Ideally, also set \texttt{CVC3\_VERSION},
-\texttt{YICES\_VERSION}, or \texttt{Z3\_NEW\_VERSION} to the solver's version
+Z3 executable somewhere (e.g., \url{http://z3.codeplex.com/}),
+set the environment variable \texttt{CVC3\_\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 and Z3
+4.3.2. Since the SMT solvers' output formats are somewhat unstable, other
+versions of the solvers might not work well with Sledgehammer. Ideally, also set
+\texttt{CVC3\_VERSION} or \texttt{Z3\_NEW\_VERSION} to the solver's version
number (e.g., ``4.3.2'').
\end{enum}
\end{sloppy}
@@ -570,12 +566,11 @@
that can be guessed from the number of facts in the original proof and the time
it took to find or preplay it).
-In addition, some provers (e.g., Yices) do not provide proofs or sometimes
-produce incomplete proofs. The minimizer is then invoked to find out which facts
-are actually needed from the (large) set of facts that was initially given to
-the prover. Finally, if a prover returns a proof with lots of facts, the
-minimizer is invoked automatically since Metis would be unlikely to re-find the
-proof.
+In addition, some provers do not provide proofs or sometimes produce incomplete
+proofs. The minimizer is then invoked to find out which facts are actually needed
+from the (large) set of facts that was initially given to the prover. Finally,
+if a prover returns a proof with lots of facts, the minimizer is invoked
+automatically since Metis would be unlikely to re-find the proof.
%
Automatic minimization can be forced or disabled using the \textit{minimize}
option (\S\ref{mode-of-operation}).
@@ -899,11 +894,6 @@
``3.0''). Sledgehammer has been tested with versions 0.6 to 3.0.
Versions strictly above 1.8 support the TPTP typed first-order format (TFF0).
-\item[\labelitemi] \textbf{\textit{yices}:} Yices is an SMT solver developed at
-SRI \cite{yices}. To use Yices, set the environment variable
-\texttt{YICES\_SOLVER} to the complete path of the executable, including the
-file name. Sledgehammer has been tested with version 1.0.28.
-
\item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
Microsoft Research \cite{z3}. To use Z3, set the environment variable
\texttt{Z3\_NEW\_SOLVER} to the complete path of the executable, including the file
@@ -977,8 +967,8 @@
\end{enum}
By default, Sledgehammer runs a selection of CVC3, E, E-SInE, SPASS, Vampire,
-Yices, and Z3 in parallel---either locally or remotely, depending on the number
-of processor cores available.
+and Z3 in parallel---either locally or remotely, depending on the number of
+processor cores available.
It is generally a good idea to run several provers in parallel. Running E,
SPASS, and Vampire for 5~seconds yields a similar success rate to running the