# HG changeset patch # User blanchet # Date 1402585323 -7200 # Node ID 7fca4159117f4ca5155352de89c2518a18778eb8 # Parent 9a5729600ba94abbb67e5edfb50c6d1890cc21ca updated docs diff -r 9a5729600ba9 -r 7fca4159117f NEWS --- a/NEWS Thu Jun 12 17:02:03 2014 +0200 +++ b/NEWS Thu Jun 12 17:02:03 2014 +0200 @@ -382,9 +382,9 @@ * SMT module: * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2 and supports recent versions of Z3 (e.g., 4.3). The new proof method is - called "smt2". CVC3 is also supported as an oracle. Yices is no longer - supported, because no version of the solver can handle both SMT-LIB 2 and - quantifiers. + called "smt2". CVC3 and CVC4 are also supported as oracles. Yices is no + longer supported, because no version of the solver can handle both + SMT-LIB 2 and quantifiers. * Sledgehammer: - New prover "z3_new" with support for Isar proofs diff -r 9a5729600ba9 -r 7fca4159117f src/Doc/Nitpick/document/root.tex --- a/src/Doc/Nitpick/document/root.tex Thu Jun 12 17:02:03 2014 +0200 +++ b/src/Doc/Nitpick/document/root.tex Thu Jun 12 17:02:03 2014 +0200 @@ -1745,8 +1745,8 @@ The options are categorized as follows:\ mode of operation (\S\ref{mode-of-operation}), scope of search (\S\ref{scope-of-search}), output format (\S\ref{output-format}), automatic counterexample checks -(\S\ref{authentication}), optimizations -(\S\ref{optimizations}), and timeouts (\S\ref{timeouts}). +(\S\ref{authentication}), regression testing (\S\ref{regression-testing}), +optimizations (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}). If you use Isabelle/jEdit, Nitpick also provides an automatic mode that can be enabled via the ``Auto Nitpick'' option under ``Plugins > Plugin Options @@ -2186,6 +2186,9 @@ \nopagebreak {\small See also \textit{max\_genuine} (\S\ref{output-format}).} +\subsection{Regression Testing} +\label{regression-testing} + \opnodefault{expect}{string} Specifies the expected outcome, which must be one of the following: diff -r 9a5729600ba9 -r 7fca4159117f src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Thu Jun 12 17:02:03 2014 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Thu Jun 12 17:02:03 2014 +0200 @@ -109,13 +109,12 @@ \cite{leo2}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS \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} 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 System\-On\-TPTP web service \cite{sutcliffe-2000}. The supported SMT +solvers are CVC3 \cite{cvc3}, CVC4 \cite{cvc4}, and Z3 \cite{z3}. These are +always run locally. -The problem passed to the automatic provers consists of your current goal -together with a heuristic selection of hundreds of facts (theorems) from the +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 current theory context, filtered by relevance. The result of a successful proof search is some source text that usually (but @@ -157,8 +156,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 and Z3 can be -run locally. +should at least install E and SPASS locally. The SMT solvers CVC3, CVC4, and Z3 +can be run locally. There are three main ways to install automatic provers on your machine: @@ -213,15 +212,16 @@ \texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or \texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``3.0''). -Similarly, if you want to build CVC3, or found a +Similarly, if you want to build CVC3 or CVC4, or found a 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''). +set the environment variable \texttt{CVC3\_\allowbreak SOLVER}, +\texttt{CVC4\_\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, CVC4 1.2, and Z3 4.3.2. Since Z3's output format is +somewhat unstable, other versions of the solver might not work well with +Sledgehammer. Ideally, also set +\texttt{CVC3\_VERSION}, \texttt{CVC4\_VERSION}, or \texttt{Z3\_NEW\_VERSION} to +the solver's version number (e.g., ``4.3.2''). \end{enum} \end{sloppy} @@ -770,8 +770,8 @@ Sledgehammer's options are categorized as follows:\ mode of operation (\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}), relevance filter (\S\ref{relevance-filter}), output format -(\S\ref{output-format}), authentication (\S\ref{authentication}), and timeouts -(\S\ref{timeouts}). +(\S\ref{output-format}), regression testing (\S\ref{regression-testing}), +and timeouts (\S\ref{timeouts}). The descriptions below refer to the following syntactic quantities: @@ -824,7 +824,13 @@ 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, or install the prebuilt CVC3 package from -\download. Sledgehammer has been tested with version 2.2 and 2.4.1. +\download. Sledgehammer has been tested with versions 2.2 and 2.4.1. + +\item[\labelitemi] \textbf{\textit{cvc4}:} CVC4 \cite{cvc4} is the successor to +CVC3. 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. Sledgehammer has been tested with version +1.2. \item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment @@ -1338,8 +1344,8 @@ proofs. \end{enum} -\subsection{Authentication} -\label{authentication} +\subsection{Regression Testing} +\label{regression-testing} \begin{enum} \opnodefault{expect}{string} diff -r 9a5729600ba9 -r 7fca4159117f src/Doc/manual.bib --- a/src/Doc/manual.bib Thu Jun 12 17:02:03 2014 +0200 +++ b/src/Doc/manual.bib Thu Jun 12 17:02:03 2014 +0200 @@ -193,6 +193,27 @@ year = {2007} } +@inproceedings{cvc4, + author = {Clark Barrett and + Christopher L. Conway and + Morgan Deters and + Liana Hadarean and + Dejan Jovanovic and + Tim King and + Andrew Reynolds and + Cesare Tinelli}, + title = {{CVC4}}, + booktitle = {CAV 2011}, + year = {2011}, + pages = {171--177}, + editor = {Ganesh Gopalakrishnan and + Shaz Qadeer}, + publisher = {Springer}, + series = LNCS, + volume = {6806}, + year = {2011} +} + @incollection{basin91, author = {David Basin and Matt Kaufmann}, title = {The {Boyer-Moore} Prover and {Nuprl}: An Experimental