# HG changeset patch
# User blanchet
# Date 1323871522 -3600
# Node ID a8b9191609a8717f30335ae9ea004db4ba75f2e6
# Parent  36ff12b5663bf4de03d622c3c3a211a1c5d53699
updated Sledgehammer/SMT docs

diff -r 36ff12b5663b -r a8b9191609a8 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Wed Dec 14 10:18:28 2011 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed Dec 14 15:05:22 2011 +0100
@@ -178,8 +178,8 @@
 
 in it.
 
-\item[\labelitemi] If you prefer to build E or SPASS yourself, or obtained a
-Vampire executable from somewhere (e.g., \url{http://www.vprover.org/}),
+\item[\labelitemi] If you prefer to build E or SPASS yourself, or found a
+Vampire executable somewhere (e.g., \url{http://www.vprover.org/}),
 set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
 \texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested
@@ -188,7 +188,7 @@
 reset to 0; hence the (new) Vampire versions 0.6, 1.0, and 1.8 are more recent
 than, say, Vampire 9.0 or 11.5.}%
 . Since the ATPs' output formats are neither documented nor stable, other
-versions of the ATPs might or might not work well with Sledgehammer. Ideally,
+versions of the ATPs might not work well with Sledgehammer. Ideally,
 also set \texttt{E\_VERSION}, \texttt{SPASS\_VERSION}, or
 \texttt{VAMPIRE\_VERSION} to the ATP's version number (e.g., ``1.4'').
 \end{enum}
@@ -220,20 +220,36 @@
 
 There are two main ways of installing SMT solvers locally.
 
+\sloppy
+
 \begin{enum}
 \item[\labelitemi] If you installed an official Isabelle package with everything
 inside, it should already include properly setup executables for CVC3 and Z3,
 ready to use.%
 \footnote{Yices's license prevents us from doing the same for this otherwise
 wonderful tool.}
-For Z3, you additionally need to set the environment variable
-\texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a noncommercial
-user.
+For Z3, you must also set the variable
+\texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
+noncommercial user, either in the environment in which Isabelle is
+launched or in your
+\texttt{\char`\~/\$ISABELLE\_HOME\_USER/etc/settings} file.
 
-\item[\labelitemi] Otherwise, follow the instructions documented in the \emph{SMT}
-theory (\texttt{\$ISABELLE\_HOME/src/HOL/SMT.thy}).
+\item[\labelitemi] If you prefer to build CVC3 yourself, 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, including the file name. Sledgehammer has been tested
+with CVC3 2.2, Yices 1.0.28, and Z3 3.0 to 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\_VERSION} to the solver's version number (e.g., ``3.2'').
 \end{enum}
 
+\fussy
+
 \section{First Steps}
 \label{first-steps}
 
@@ -779,18 +795,20 @@
 \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.
+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\_SOLVER} to the complete path of the executable, including the file
 name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
-noncommercial user. Sledgehammer has been tested with versions 2.7 to 2.18.
+noncommercial user. Sledgehammer has been tested with versions 3.0 to 3.2.
 
 \item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
 an ATP, exploiting Z3's support for the TPTP untyped and typed first-order
-formats (FOF and TFF0). It is included for experimental purposes. It requires
-version 3.0 or above.
+formats (FOF and TFF0). It is included for experimental purposes. It
+requires version 3.0 or above. To use it, set the environment variable
+\texttt{Z3\_HOME} to the directory that contains the \texttt{z3}
+executable.
 \end{enum}
 
 In addition, the following remote provers are supported: