--- a/doc-src/Sledgehammer/sledgehammer.tex Fri May 20 12:47:59 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Fri May 20 12:47:59 2011 +0200
@@ -296,6 +296,10 @@
\section{Hints}
\label{hints}
+This section presents a few hints that should help you get the most out of
+Sledgehammer and Metis. Frequently (and infrequently) asked questions are
+answered in \S\ref{frequently-asked-questions}.
+
\newcommand\point[1]{{\sl\bfseries#1}\par\nopagebreak}
\point{Presimplify the goal}
@@ -321,35 +325,40 @@
familiarize themselves with the following options:
\begin{enum}
-\item[$\bullet$] \textbf{\textit{provers}} specifies the ATP and SMT solvers to
-use (e.g., ``\textit{provers} = \textit{e spass remote\_vampire}'').
+\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}'').
-\item[$\bullet$] \textbf{\textit{timeout}} controls the provers' time limit. It
-is set to 30 seconds, but since Sledgehammer runs asynchronously you should not
-hesitate to raise this limit to 60 or 120 seconds if you are the kind of user
-who can think clearly while ATPs are active.
+\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
+asynchronously you should not hesitate to raise this limit to 60 or 120 seconds
+if you are the kind of user who can think clearly while ATPs are active.
-\item[$\bullet$] \textbf{\textit{full\_types}} specifies whether type-sound
-encodings should be used. By default, Sledgehammer employs a mixture of
-type-sound and type-unsound encodings, occasionally yielding unsound ATP proofs.
-(SMT solver proofs should always be sound, although we occasionally find
-soundness bugs in the solvers.)
+\item[$\bullet$] \textbf{\textit{full\_types}} (\S\ref{problem-encoding})
+specifies whether type-sound encodings should be used. By default, Sledgehammer
+employs a mixture of type-sound and type-unsound encodings, occasionally
+yielding unsound ATP proofs. (SMT solver proofs should always be sound, although
+we occasionally find soundness bugs in the solvers.)
-\item[$\bullet$] \textbf{\textit{max\_relevant}} specifies the maximum number of
-facts that should be passed to the provers. By default, the value is
-prover-dependent but varies between about 150 and 1000. If the provers time out,
-you can try lowering this value to, say, 100 or 50 and see if that helps.
+\item[$\bullet$] \textbf{\textit{max\_relevant}} (\S\ref{relevance-filter})
+specifies the maximum number of facts that should be passed to the provers. By
+default, the value is prover-dependent but varies between about 150 and 1000. If
+the provers time out, you can try lowering this value to, say, 100 or 50 and see
+if that helps.
-\item[$\bullet$] \textbf{\textit{isar\_proof}} specifies that Isar proofs should
-be generated, instead of one-liner Metis proofs. The length of the Isar proofs
-can be controlled by setting \textit{isar\_shrink\_factor}.
+\item[$\bullet$] \textbf{\textit{isar\_proof}} (\S\ref{output-format}) specifies
+that Isar proofs should be generated, instead of one-liner Metis proofs. The
+length of the Isar proofs can be controlled by setting
+\textit{isar\_shrink\_factor} (\S\ref{output-format}).
\end{enum}
-Options can be set globally using \textbf{sledgehammer\_params}. Fact selection
-can be influenced by specifying ``$(\textit{add}{:}~\textit{some\_facts})$'' after
-the \textbf{sledgehammer} call to ensure that certain facts are included, or
-simply ``$(\textit{some\_facts})$'' to force Sledgehammer to run only with
-$\textit{some\_facts}$.
+Options can be set globally using \textbf{sledgehammer\_params}
+(\S\ref{command-syntax}). Fact selection can be influenced by specifying
+``$(\textit{add}{:}~\textit{my\_facts})$'' after the \textbf{sledgehammer}
+call to ensure that certain facts are included, or simply
+``$(\textit{my\_facts})$'' to force Sledgehammer to run only with
+$\textit{my\_facts}$.
\section{Frequently Asked Questions}
\label{frequently-asked-questions}
@@ -429,7 +438,8 @@
Sledgehammer is good at finding short proofs combining a handful of existing
lemmas. If you are looking for longer proofs, you must typically restrict the
-number of facts, by setting \textit{max\_relevant} to, say, 50 or 100.
+number of facts, by setting the \textit{max\_relevant} option
+(\S\ref{relevance-filter}) to, say, 50 or 100.
\point{Why are the Isar proofs generated by Sledgehammer so ugly?}
@@ -725,11 +735,11 @@
\opnodefault{prover}{string}
Alias for \textit{provers}.
-\opnodefault{atps}{string}
-Legacy alias for \textit{provers}.
+%\opnodefault{atps}{string}
+%Legacy alias for \textit{provers}.
-\opnodefault{atp}{string}
-Legacy alias for \textit{provers}.
+%\opnodefault{atp}{string}
+%Legacy alias for \textit{provers}.
\opdefault{timeout}{float\_or\_none}{\upshape 30}
Specifies the maximum number of seconds that the automatic provers should spend
@@ -875,18 +885,6 @@
For SMT solvers and ToFoF-E, the type system is always \textit{simple},
irrespective of the value of this option.
-
-\opdefault{max\_mono\_iters}{int}{\upshape 3}
-Specifies the maximum number of iterations for the monomorphization fixpoint
-construction. The higher this limit is, the more monomorphic instances are
-potentially generated. Whether monomorphization takes place depends on the
-type system used.
-
-\opdefault{max\_new\_mono\_instances}{int}{\upshape 400}
-Specifies the maximum number of monomorphic instances to generate beyond
-\textit{max\_relevant}. The higher this limit is, the more monomorphic instances
-are potentially generated. Whether monomorphization takes place depends on the
-type system used.
\end{enum}
\subsection{Relevance Filter}
@@ -907,6 +905,23 @@
empirically found to be appropriate for the prover. A typical value would be
300.
+\opdefault{max\_new\_mono\_instances}{int}{\upshape 400}
+Specifies the maximum number of monomorphic instances to generate beyond
+\textit{max\_relevant}. The higher this limit is, the more monomorphic instances
+are potentially generated. Whether monomorphization takes place depends on the
+type system used.
+
+\nopagebreak
+{\small See also \textit{type\_sys} (\S\ref{problem-encoding}).}
+
+\opdefault{max\_mono\_iters}{int}{\upshape 3}
+Specifies the maximum number of iterations for the monomorphization fixpoint
+construction. The higher this limit is, the more monomorphic instances are
+potentially generated. Whether monomorphization takes place depends on the
+type system used.
+
+\nopagebreak
+{\small See also \textit{type\_sys} (\S\ref{problem-encoding}).}
\end{enum}
\subsection{Output Format}
--- a/doc-src/manual.bib Fri May 20 12:47:59 2011 +0200
+++ b/doc-src/manual.bib Fri May 20 12:47:59 2011 +0200
@@ -421,7 +421,7 @@
@misc{yices,
author = {Bruno Dutertre and Leonardo de Moura},
title = {The {Yices} {SMT} Solver},
- publisher = "\url{http://yices.csl.sri.com/tool-paper.pdf}",
+ howpublished = "\url{http://yices.csl.sri.com/tool-paper.pdf}",
year = 2006}
@incollection{dybjer91,
@@ -648,10 +648,15 @@
number = 5,
month = May}
-@misc{sine,
- author = "Kry\v{s}tof Hoder",
- title = "{SInE} (Sumo Inference Engine)",
- note = "\url{http://www.cs.man.ac.uk/~hoderk/sine/}"}
+@inproceedings{sine,
+ author = "Kry\v{s}tof Hoder and Andrei Voronkov",
+ title = "Sine Qua Non for Large Theory Reasoning",
+ booktitle = {Automated Deduction --- CADE-23},
+ publisher = Springer,
+ series = LNCS,
+ editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans",
+ year = 2011,
+ note = "To appear."}
@book{Hudak-Haskell,author={Paul Hudak},
title={The Haskell School of Expression},publisher=CUP,year=2000}