doc-src/Sledgehammer/sledgehammer.tex

 experimental and is only available for ATPs.
 
 \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}
 
 For best results, first simplify your problem by calling \textit{auto} or at

 Sledgehammer's options are fully documented in \S\ref{command-syntax}. Many of
 the options are very specialized, but serious users of the tool should at least
 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{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{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{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{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}.
-\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}$.
+\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}} (\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}} (\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}} (\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}} (\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}
+(\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}
 
 \point{Why does Metis fail to reconstruct the proof?}

 facts given using the \textit{verbose} option (\S\ref{output-format}) and the
 actual facts using \textit{debug} (\S\ref{output-format}).
 
 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?}
 
 The current implementation is experimental and explodes exponentially in the
 worst case. Work on a new implementation has begun. There is a large body of

 for 120 seconds \cite{boehme-nipkow-2010}.
 
 \opnodefault{prover}{string}
 Alias for \textit{provers}.
 
-\opnodefault{atps}{string}
-Legacy alias for \textit{provers}.
-
-\opnodefault{atp}{string}
-Legacy alias for \textit{provers}.
+%\opnodefault{atps}{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
 searching for a proof. This excludes problem preparation and is a soft limit.
 For historical reasons, the default value of this option can be overridden using

 variants are identified by a \textit{\_heavy} suffix (e.g.,
 \textit{mangled\_preds\_heavy}{?}).
 
 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}
 \label{relevance-filter}
 

 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
 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}
 \label{output-format}