updated docs
authorblanchet
Thu Jun 12 17:02:03 2014 +0200 (2014-06-12)
changeset 572417fca4159117f
parent 57240 9a5729600ba9
child 57242 25aff3b8d550
updated docs
NEWS
src/Doc/Nitpick/document/root.tex
src/Doc/Sledgehammer/document/root.tex
src/Doc/manual.bib
     1.1 --- a/NEWS	Thu Jun 12 17:02:03 2014 +0200
     1.2 +++ b/NEWS	Thu Jun 12 17:02:03 2014 +0200
     1.3 @@ -382,9 +382,9 @@
     1.4  * SMT module:
     1.5    * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2
     1.6      and supports recent versions of Z3 (e.g., 4.3). The new proof method is
     1.7 -    called "smt2". CVC3 is also supported as an oracle. Yices is no longer
     1.8 -    supported, because no version of the solver can handle both SMT-LIB 2 and
     1.9 -    quantifiers.
    1.10 +    called "smt2". CVC3 and CVC4 are also supported as oracles. Yices is no
    1.11 +    longer supported, because no version of the solver can handle both
    1.12 +    SMT-LIB 2 and quantifiers.
    1.13  
    1.14  * Sledgehammer:
    1.15    - New prover "z3_new" with support for Isar proofs
     2.1 --- a/src/Doc/Nitpick/document/root.tex	Thu Jun 12 17:02:03 2014 +0200
     2.2 +++ b/src/Doc/Nitpick/document/root.tex	Thu Jun 12 17:02:03 2014 +0200
     2.3 @@ -1745,8 +1745,8 @@
     2.4  The options are categorized as follows:\ mode of operation
     2.5  (\S\ref{mode-of-operation}), scope of search (\S\ref{scope-of-search}), output
     2.6  format (\S\ref{output-format}), automatic counterexample checks
     2.7 -(\S\ref{authentication}), optimizations
     2.8 -(\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
     2.9 +(\S\ref{authentication}), regression testing (\S\ref{regression-testing}),
    2.10 +optimizations (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
    2.11  
    2.12  If you use Isabelle/jEdit, Nitpick also provides an automatic mode that can
    2.13  be enabled via the ``Auto Nitpick'' option under ``Plugins > Plugin Options
    2.14 @@ -2186,6 +2186,9 @@
    2.15  \nopagebreak
    2.16  {\small See also \textit{max\_genuine} (\S\ref{output-format}).}
    2.17  
    2.18 +\subsection{Regression Testing}
    2.19 +\label{regression-testing}
    2.20 +
    2.21  \opnodefault{expect}{string}
    2.22  Specifies the expected outcome, which must be one of the following:
    2.23  
     3.1 --- a/src/Doc/Sledgehammer/document/root.tex	Thu Jun 12 17:02:03 2014 +0200
     3.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Thu Jun 12 17:02:03 2014 +0200
     3.3 @@ -109,13 +109,12 @@
     3.4  \cite{leo2}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS
     3.5  \cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, and
     3.6  Waldmeister \cite{waldmeister}. The ATPs are run either locally or remotely via
     3.7 -the System\-On\-TPTP web service \cite{sutcliffe-2000}. In addition to the ATPs,
     3.8 -a selection of the SMT solvers CVC3 \cite{cvc3} and Z3 \cite{z3} are run by
     3.9 -default; these are run either locally or (for CVC3 and Z3) on a server at the
    3.10 -TU M\"unchen.
    3.11 +the System\-On\-TPTP web service \cite{sutcliffe-2000}. The supported SMT
    3.12 +solvers are CVC3 \cite{cvc3}, CVC4 \cite{cvc4}, and Z3 \cite{z3}. These are
    3.13 +always run locally.
    3.14  
    3.15 -The problem passed to the automatic provers consists of your current goal
    3.16 -together with a heuristic selection of hundreds of facts (theorems) from the
    3.17 +The problem passed to the external provers (or solvers) consists of your current
    3.18 +goal together with a heuristic selection of hundreds of facts (theorems) from the
    3.19  current theory context, filtered by relevance.
    3.20  
    3.21  The result of a successful proof search is some source text that usually (but
    3.22 @@ -157,8 +156,8 @@
    3.23  be run locally; in addition, AgsyHOL, E, E-SInE, E-ToFoF, iProver, iProver-Eq,
    3.24  LEO-II, Satallax, SNARK, Vampire, and Waldmeister are available remotely via
    3.25  System\-On\-TPTP \cite{sutcliffe-2000}. If you want better performance, you
    3.26 -should at least install E and SPASS locally. The SMT solvers CVC3 and Z3 can be
    3.27 -run locally.
    3.28 +should at least install E and SPASS locally. The SMT solvers CVC3, CVC4, and Z3
    3.29 +can be run locally.
    3.30  
    3.31  There are three main ways to install automatic provers on your machine:
    3.32  
    3.33 @@ -213,15 +212,16 @@
    3.34  \texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or
    3.35  \texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``3.0'').
    3.36  
    3.37 -Similarly, if you want to build CVC3, or found a
    3.38 +Similarly, if you want to build CVC3 or CVC4, or found a
    3.39  Z3 executable somewhere (e.g., \url{http://z3.codeplex.com/}),
    3.40 -set the environment variable \texttt{CVC3\_\allowbreak SOLVER}
    3.41 -or \texttt{Z3\_SOLVER} to the complete path of the executable, \emph{including
    3.42 -the file name}. Sledgehammer has been tested with CVC3 2.2 and 2.4.1 and Z3
    3.43 -4.3.2. Since the SMT solvers' output formats are somewhat unstable, other
    3.44 -versions of the solvers might not work well with Sledgehammer. Ideally, also set
    3.45 -\texttt{CVC3\_VERSION} or \texttt{Z3\_NEW\_VERSION} to the solver's version
    3.46 -number (e.g., ``4.3.2'').
    3.47 +set the environment variable \texttt{CVC3\_\allowbreak SOLVER},
    3.48 +\texttt{CVC4\_\allowbreak SOLVER}, or \texttt{Z3\_SOLVER} to the complete path
    3.49 +of the executable, \emph{including the file name}. Sledgehammer has been tested
    3.50 +with CVC3 2.2 and 2.4.1, CVC4 1.2, and Z3 4.3.2. Since Z3's output format is
    3.51 +somewhat unstable, other versions of the solver might not work well with
    3.52 +Sledgehammer. Ideally, also set
    3.53 +\texttt{CVC3\_VERSION}, \texttt{CVC4\_VERSION}, or \texttt{Z3\_NEW\_VERSION} to
    3.54 +the solver's version number (e.g., ``4.3.2'').
    3.55  \end{enum}
    3.56  \end{sloppy}
    3.57  
    3.58 @@ -770,8 +770,8 @@
    3.59  Sledgehammer's options are categorized as follows:\ mode of operation
    3.60  (\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}),
    3.61  relevance filter (\S\ref{relevance-filter}), output format
    3.62 -(\S\ref{output-format}), authentication (\S\ref{authentication}), and timeouts
    3.63 -(\S\ref{timeouts}).
    3.64 +(\S\ref{output-format}), regression testing (\S\ref{regression-testing}),
    3.65 +and timeouts (\S\ref{timeouts}).
    3.66  
    3.67  The descriptions below refer to the following syntactic quantities:
    3.68  
    3.69 @@ -824,7 +824,13 @@
    3.70  Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
    3.71  set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
    3.72  executable, including the file name, or install the prebuilt CVC3 package from
    3.73 -\download. Sledgehammer has been tested with version 2.2 and 2.4.1.
    3.74 +\download. Sledgehammer has been tested with versions 2.2 and 2.4.1.
    3.75 +
    3.76 +\item[\labelitemi] \textbf{\textit{cvc4}:} CVC4 \cite{cvc4} is the successor to
    3.77 +CVC3. To use CVC4, set the environment variable \texttt{CVC4\_SOLVER} to the
    3.78 +complete path of the executable, including the file name, or install the
    3.79 +prebuilt CVC4 package from \download. Sledgehammer has been tested with version
    3.80 +1.2.
    3.81  
    3.82  \item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover
    3.83  developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment
    3.84 @@ -1338,8 +1344,8 @@
    3.85  proofs.
    3.86  \end{enum}
    3.87  
    3.88 -\subsection{Authentication}
    3.89 -\label{authentication}
    3.90 +\subsection{Regression Testing}
    3.91 +\label{regression-testing}
    3.92  
    3.93  \begin{enum}
    3.94  \opnodefault{expect}{string}
     4.1 --- a/src/Doc/manual.bib	Thu Jun 12 17:02:03 2014 +0200
     4.2 +++ b/src/Doc/manual.bib	Thu Jun 12 17:02:03 2014 +0200
     4.3 @@ -193,6 +193,27 @@
     4.4    year      = {2007}
     4.5  }
     4.6  
     4.7 +@inproceedings{cvc4,
     4.8 +  author    = {Clark Barrett and
     4.9 +               Christopher L. Conway and
    4.10 +               Morgan Deters and
    4.11 +               Liana Hadarean and
    4.12 +               Dejan Jovanovic and
    4.13 +               Tim King and
    4.14 +               Andrew Reynolds and
    4.15 +               Cesare Tinelli},
    4.16 +  title     = {{CVC4}},
    4.17 +  booktitle = {CAV 2011},
    4.18 +  year      = {2011},
    4.19 +  pages     = {171--177},
    4.20 +  editor    = {Ganesh Gopalakrishnan and
    4.21 +               Shaz Qadeer},
    4.22 +  publisher = {Springer},
    4.23 +  series    = LNCS,
    4.24 +  volume    = {6806},
    4.25 +  year      = {2011}
    4.26 +}
    4.27 +
    4.28  @incollection{basin91,
    4.29    author	= {David Basin and Matt Kaufmann},
    4.30    title		= {The {Boyer-Moore} Prover and {Nuprl}: An Experimental