# HG changeset patch
# User blanchet
# Date 1306485008 -7200
# Node ID 0dca147765f45fd1d8848f1dc712fde7a7b3d1f7
# Parent  3a95b1ae796d5afab132a4c30ff0bf04954c26ab
minor fixes to Sledgehammer docs

diff -r 3a95b1ae796d -r 0dca147765f4 doc-src/Sledgehammer/sledgehammer.tex
--- 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}