# HG changeset patch # User blanchet # Date 1291397389 -3600 # Node ID e08fa125c268cb4626ed6bb7cfd90f3cb59c90ff # Parent a3e6f8634a116dcf63ba914bc8e9f0cc1a045ad6 update documentation diff -r a3e6f8634a11 -r e08fa125c268 doc-src/Sledgehammer/sledgehammer.tex --- 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 diff -r a3e6f8634a11 -r e08fa125c268 doc-src/manual.bib --- 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