--- a/doc-src/Sledgehammer/sledgehammer.tex Fri May 27 10:30:08 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Fri May 27 10:30:08 2011 +0200
@@ -250,33 +250,33 @@
Sledgehammer: ``\textit{e}'' on goal: \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
Try this command: \textbf{by} (\textit{metis last\_ConsL}). \\
-To minimize: \textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{e}] (\textit{last\_ConsL}). \\[3\smallskipamount]
+To minimize: \textbf{sledgehammer} \textit{min} [\textit{e}] (\textit{last\_ConsL}). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{vampire}'' on goal: \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
Try this command: \textbf{by} (\textit{metis hd.simps}). \\
-To minimize: \textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{vampire}] (\textit{hd.simps}). \\[3\smallskipamount]
+To minimize: \textbf{sledgehammer} \textit{min} [\textit{vampire}] (\textit{hd.simps}). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{spass}'' on goal: \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
Try this command: \textbf{by} (\textit{metis list.inject}). \\
-To minimize: \textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{spass}]~(\textit{list.inject}). \\[3\smallskipamount]
+To minimize: \textbf{sledgehammer} \textit{min} [\textit{spass}]~(\textit{list.inject}). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{remote\_waldmeister}'' on goal: \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
Try this command: \textbf{by} (\textit{metis hd.simps insert\_Nil}). \\
-To minimize: \textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{remote\_waldmeister}] \\
+To minimize: \textbf{sledgehammer} \textit{min} [\textit{remote\_waldmeister}] \\
\phantom{To minimize: \textbf{sledgehammer}~}(\textit{hd.simps insert\_Nil}). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{remote\_sine\_e}'' on goal: \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
Try this command: \textbf{by} (\textit{metis hd.simps}). \\
-To minimize: \textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}). \\[3\smallskipamount]
+To minimize: \textbf{sledgehammer} \textit{min} [\textit{remote\_sine\_e}]~(\textit{hd.simps}). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{remote\_z3}'' on goal: \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
Try this command: \textbf{by} (\textit{metis hd.simps}). \\
-To minimize: \textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{remote\_z3}]~(\textit{hd.simps}).
+To minimize: \textbf{sledgehammer} \textit{min} [\textit{remote\_z3}]~(\textit{hd.simps}).
\postw
Sledgehammer ran E, SInE-E, SPASS, Vampire, Waldmeister, and Z3 in parallel.
@@ -338,7 +338,9 @@
\item[$\bullet$] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies
the automatic provers (ATPs and SMT solvers) that should be run whenever
Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{e spass
-remote\_vampire}'').
+remote\_vampire}''). For convenience, you can omit ``\textit{provers}~=''
+and simply write the prover names as a space-separated list (e.g., ``\textit{e
+spass remote\_vampire}'').
\item[$\bullet$] \textbf{\textit{timeout}} (\S\ref{mode-of-operation}) controls
the provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
@@ -643,18 +645,22 @@
\section{Option Reference}
\label{option-reference}
+\def\defl{\{}
+\def\defr{\}}
+
\def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
\def\qty#1{$\left<\textit{#1}\right>$}
\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$}
-\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
-\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
-\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
-\def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
+\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
+\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
+\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
+\def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
-\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
+\def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]}
+\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]}
\def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
\def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
-\def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
+\def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
Sledgehammer's options are categorized as follows:\ mode of operation
(\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}),
@@ -666,19 +672,19 @@
\begin{enum}
\item[$\bullet$] \qtybf{string}: A string.
\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
-\item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or
+\item[$\bullet$] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or
\textit{smart}.
\item[$\bullet$] \qtybf{int\/}: An integer.
%\item[$\bullet$] \qtybf{float\/}: A floating-point number (e.g., 2.5).
\item[$\bullet$] \qtybf{float\_pair\/}: A pair of floating-point numbers
(e.g., 0.6 0.95).
-\item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
+\item[$\bullet$] \qtybf{smart\_int\/}: An integer or \textit{smart}.
\item[$\bullet$] \qtybf{float\_or\_none\/}: An integer (e.g., 60) or
floating-point number (e.g., 0.5) expressing a number of seconds, or the keyword
\textit{none} ($\infty$ seconds).
\end{enum}
-Default values are indicated in square brackets. Boolean options have a negated
+Default values are indicated in braces. Boolean options have a negated
counterpart (e.g., \textit{blocking} vs.\ \textit{non\_blocking}). When setting
Boolean options, ``= \textit{true}'' may be omitted.
@@ -686,9 +692,10 @@
\label{mode-of-operation}
\begin{enum}
-\opnodefault{provers}{string}
+\opnodefaultbrk{provers}{string}
Specifies the automatic provers to use as a space-separated list (e.g.,
-``\textit{e}~\textit{spass}''). The following local provers are supported:
+``\textit{e}~\textit{spass}~\textit{remote\_vampire}''). The following local
+provers are supported:
\begin{enum}
\item[$\bullet$] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
@@ -970,7 +977,7 @@
iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems
are relevant and 1 only theorems that refer to previously seen constants.
-\opsmart{max\_relevant}{int\_or\_smart}
+\opsmart{max\_relevant}{smart\_int}
Specifies the maximum number of facts that may be returned by the relevance
filter. If the option is set to \textit{smart}, it is set to a value that was
empirically found to be appropriate for the prover. A typical value would be
@@ -1038,6 +1045,7 @@
\item[$\bullet$] \textbf{\textit{some}:} Sledgehammer found a (potentially
unsound) proof.
\item[$\bullet$] \textbf{\textit{none}:} Sledgehammer found no proof.
+\item[$\bullet$] \textbf{\textit{timeout}:} Sledgehammer timed out.
\item[$\bullet$] \textbf{\textit{unknown}:} Sledgehammer encountered some
problem.
\end{enum}