--- a/doc-src/Sledgehammer/sledgehammer.tex Fri Dec 03 18:29:14 2010 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Fri Dec 03 18:29:49 2010 +0100
@@ -78,13 +78,13 @@
\label{introduction}
Sledgehammer is a tool that applies first-order automatic theorem provers (ATPs)
-and satisfiability-modulo-theory (SMT) solvers on the current goal. The
+and satisfiability-modulo-theories (SMT) solvers on the current goal. The
supported ATPs are E \cite{schulz-2002}, SPASS \cite{weidenbach-et-al-2009},
Vampire \cite{riazanov-voronkov-2002}, SInE-E \cite{sine}, and SNARK
\cite{snark}. The ATPs are run either locally or remotely via the
System\-On\-TPTP web service \cite{sutcliffe-2000}. In addition to the ATPs, the
-\textit{smt} proof method (which typically relies on the Z3 SMT solver
-\cite{z3}) is tried as well.
+SMT solvers Z3 \cite{z3} is used, and you can tell Sledgehammer to try Yices
+\cite{yices} and CVC3 \cite{cvc3} as well.
The problem passed to the automatic provers consists of your current goal
together with a heuristic selection of hundreds of facts (theorems) from the
@@ -226,12 +226,17 @@
Try this command: \textbf{by} (\textit{metis hd.simps}) \\
To minimize the number of lemmas, try this: \\
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}).
+%
+Sledgehammer: ``\textit{remote\_z3}'' for subgoal 1: \\
+$([a] = [b]) = (a = b)$ \\
+Try this command: \textbf{by} (\textit{metis hd.simps}) \\
+To minimize the number of lemmas, try this: \\
+\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}).
\postw
-Sledgehammer ran E, SPASS, Vampire, SInE-E, and the \textit{smt} proof method in
-parallel. Depending on which provers are installed and how many processor cores
-are available, some of the provers might be missing or present with a
-\textit{remote\_} prefix.
+Sledgehammer ran E, SPASS, Vampire, SInE-E, and Z3 in parallel. Depending on
+which provers are installed and how many processor cores are available, some of
+the provers might be missing or present with a \textit{remote\_} prefix.
For each successful prover, Sledgehammer gives a one-liner proof that uses the
\textit{metis} or \textit{smt} method. You can click the proof to insert it into
@@ -416,10 +421,24 @@
\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by
Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use
Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory
-that contains the \texttt{vampire} executable.
+that contains the \texttt{vampire} executable. Sledgehammer has been tested with
+versions 11, 0.6, and 1.0.
+
+\item[$\bullet$] \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. Sledgehammer has been tested with 2.7 to 2.15.
-\item[$\bullet$] \textbf{\textit{smt}:} The \textit{smt} proof method invokes an
-external SMT prover (usually Z3 \cite{z3}).
+\item[$\bullet$] \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.
+
+\item[$\bullet$] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
+Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
+set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
+executable, including the file name. Sledgehammer has been tested with version
+2.2.
\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
@@ -435,13 +454,17 @@
developed by Stickel et al.\ \cite{snark}. The remote version of
SNARK runs on Geoff Sutcliffe's Miami servers.
-\item[$\bullet$] \textbf{\textit{remote\_smt}:} The remote version of the
-\textit{smt} proof method runs the SMT solver on servers at the TU M\"unchen (or
-wherever \texttt{REMOTE\_SMT\_URL} is set to point).
+\item[$\bullet$] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
+servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
+point).
+\item[$\bullet$] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
+on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
+point).
\end{enum}
-By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and \textit{smt} in
+By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and Z3 (or whatever
+the SMT module's \emph{smt\_solver} configuration option is set to) in
parallel---either locally or remotely, depending on the number of processor
cores available. For historical reasons, the default value of this option can be
overridden using the option ``Sledgehammer: Provers'' from the ``Isabelle'' menu
--- a/doc-src/manual.bib Fri Dec 03 18:29:14 2010 +0100
+++ b/doc-src/manual.bib Fri Dec 03 18:29:49 2010 +0100
@@ -159,6 +159,18 @@
editor = {A. Robinson and A. Voronkov}
}
+@inproceedings{cvc3,
+ author = {Clark Barrett and Cesare Tinelli},
+ title = {{CVC3}},
+ booktitle = {CAV},
+ editor = {Werner Damm and Holger Hermanns},
+ volume = {4590},
+ series = LNCS,
+ pages = {298--302},
+ publisher = {Springer},
+ year = {2007}
+}
+
@incollection{basin91,
author = {David Basin and Matt Kaufmann},
title = {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
@@ -392,6 +404,12 @@
year = 1977,
publisher = {Oxford University Press}}
+@misc{yices,
+ author = {Bruno Dutertre and Leonardo de Moura},
+ title = {The {Yices} {SMT} Solver},
+ publisher = "\url{http://yices.csl.sri.com/tool-paper.pdf}",
+ year = 2006}
+
@incollection{dybjer91,
author = {Peter Dybjer},
title = {Inductive Sets and Families in {Martin-L{\"o}f's} Type