author blanchet Wed, 23 May 2012 13:37:26 +0200 changeset 47963 46c73ad5f7c0 parent 47962 137883567114 child 47964 b74655182ed6
--- a/doc-src/Sledgehammer/sledgehammer.tex	Wed May 23 13:28:20 2012 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed May 23 13:37:26 2012 +0200
@@ -766,8 +766,9 @@
\end{enum}

Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options
-have a negated counterpart (e.g., \textit{blocking} vs.\
-\textit{non\_blocking}). When setting them, = \textit{true\/}'' may be omitted.
+have a negative counterpart (e.g., \textit{blocking} vs.\
+\textit{non\_blocking}). When setting Boolean options or their negative
+counterparts, = \textit{true\/}'' may be omitted.

\subsection{Mode of Operation}
\label{mode-of-operation}
@@ -1183,23 +1184,27 @@
\opdefault{max\_relevant}{smart\_int}{smart}
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
-250.
+empirically found to be appropriate for the prover. Typical values range between
+50 and 1000.

-\opdefault{max\_new\_mono\_instances}{int}{\upshape 200}
+\opdefault{max\_new\_mono\_instances}{int}{smart}
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 encoding used.
+type encoding used. If the option is set to \textit{smart}, it is set to a value
+that was empirically found to be appropriate for the prover. For most provers,
+this value is 200.

\nopagebreak
{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}