doc updates
authorblanchet
Wed May 23 13:37:26 2012 +0200 (2012-05-23)
changeset 4796346c73ad5f7c0
parent 47962 137883567114
child 47964 b74655182ed6
doc updates
doc-src/Sledgehammer/sledgehammer.tex
     1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Wed May 23 13:28:20 2012 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed May 23 13:37:26 2012 +0200
     1.3 @@ -766,8 +766,9 @@
     1.4  \end{enum}
     1.5  
     1.6  Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options
     1.7 -have a negated counterpart (e.g., \textit{blocking} vs.\
     1.8 -\textit{non\_blocking}). When setting them, ``= \textit{true\/}'' may be omitted.
     1.9 +have a negative counterpart (e.g., \textit{blocking} vs.\
    1.10 +\textit{non\_blocking}). When setting Boolean options or their negative
    1.11 +counterparts, ``= \textit{true\/}'' may be omitted.
    1.12  
    1.13  \subsection{Mode of Operation}
    1.14  \label{mode-of-operation}
    1.15 @@ -1183,23 +1184,27 @@
    1.16  \opdefault{max\_relevant}{smart\_int}{smart}
    1.17  Specifies the maximum number of facts that may be returned by the relevance
    1.18  filter. If the option is set to \textit{smart}, it is set to a value that was
    1.19 -empirically found to be appropriate for the prover. A typical value would be
    1.20 -250.
    1.21 +empirically found to be appropriate for the prover. Typical values range between
    1.22 +50 and 1000.
    1.23  
    1.24 -\opdefault{max\_new\_mono\_instances}{int}{\upshape 200}
    1.25 +\opdefault{max\_new\_mono\_instances}{int}{smart}
    1.26  Specifies the maximum number of monomorphic instances to generate beyond
    1.27  \textit{max\_relevant}. The higher this limit is, the more monomorphic instances
    1.28  are potentially generated. Whether monomorphization takes place depends on the
    1.29 -type encoding used.
    1.30 +type encoding used. If the option is set to \textit{smart}, it is set to a value
    1.31 +that was empirically found to be appropriate for the prover. For most provers,
    1.32 +this value is 200.
    1.33  
    1.34  \nopagebreak
    1.35  {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
    1.36  
    1.37 -\opdefault{max\_mono\_iters}{int}{\upshape 3}
    1.38 +\opdefault{max\_mono\_iters}{int}{smart}
    1.39  Specifies the maximum number of iterations for the monomorphization fixpoint
    1.40  construction. The higher this limit is, the more monomorphic instances are
    1.41  potentially generated. Whether monomorphization takes place depends on the
    1.42 -type encoding used.
    1.43 +type encoding used. If the option is set to \textit{smart}, it is set to a value
    1.44 +that was empirically found to be appropriate for the prover. For most provers,
    1.45 +this value is 3.
    1.46  
    1.47  \nopagebreak
    1.48  {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}