1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Wed Aug 25 19:41:18 2010 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed Aug 25 19:47:25 2010 +0200
     1.3 @@ -447,33 +447,29 @@
     1.4  \label{relevance-filter}
     1.5  
     1.6  \begin{enum}
     1.7 -\opdefault{relevance\_threshold}{int}{40}
     1.8 -Specifies the threshold above which facts are considered relevant by the
     1.9 -relevance filter. The option ranges from 0 to 100, where 0 means that all
    1.10 -theorems are relevant.
    1.11 +\opdefault{relevance\_thresholds}{int\_pair}{45~95}
    1.12 +Specifies the thresholds above which facts are considered relevant by the
    1.13 +relevance filter. The first threshold is used for the first iteration of the
    1.14 +relevance filter and the second threshold is used for the last iteration (if it
    1.15 +is reached). The effective threshold is quadratically interpolated for the other
    1.16 +iterations. Each threshold ranges from 0 to 100, where 0 means that all theorems
    1.17 +are relevant and 100 only theorems that refer to previously seen constants.
    1.18  
    1.19 -\opdefault{relevance\_decay}{int}{31}
    1.20 -Specifies the decay factor, expressed as a percentage, used by the relevance
    1.21 -filter. This factor is used by the relevance filter to scale down the relevance
    1.22 -of new facts at each iteration of the filter.
    1.23 -
    1.24 -\opdefault{max\_relevant\_per\_iter}{int\_or\_smart}{\textit{smart}}
    1.25 -Specifies the maximum number of facts that may be added during one iteration of
    1.26 -the relevance filter. If the option is set to \textit{smart}, it is set to a
    1.27 -value that was empirically found to be appropriate for the ATP. A typical value
    1.28 -would be 50.
    1.29 +\opdefault{max\_relevant}{int\_or\_smart}{\textit{smart}}
    1.30 +Specifies the maximum number of facts that may be returned by the relevance
    1.31 +filter. If the option is set to \textit{smart}, it is set to a value that was
    1.32 +empirically found to be appropriate for the ATP. A typical value would be 300.
    1.33  
    1.34  \opsmartx{theory\_relevant}{theory\_irrelevant}
    1.35  Specifies whether the theory from which a fact comes should be taken into
    1.36  consideration by the relevance filter. If the option is set to \textit{smart},
    1.37 -it is taken to be \textit{true} for SPASS and \textit{false} for E and Vampire,
    1.38 -because empirical results suggest that these are the best settings.
    1.39 +it is taken to be \textit{true} for SPASS and \textit{false} for the other ATPs;
    1.40 +empirical results suggest that these are the best settings.
    1.41  
    1.42  %\opfalse{defs\_relevant}{defs\_irrelevant}
    1.43  %Specifies whether the definition of constants occurring in the formula to prove
    1.44  %should be considered particularly relevant. Enabling this option tends to lead
    1.45  %to larger problems and typically slows down the ATPs.
    1.46 -
    1.47  \end{enum}
    1.48  
    1.49  \subsection{Output Format}