# HG changeset patch
# User blanchet
# Date 1282758445 -7200
# Node ID 9b465a288c621806dc766b313177c7b2d15a16c7
# Parent  ad577fd62ee46858252eaf49faad1ce02293516e
update docs

diff -r ad577fd62ee4 -r 9b465a288c62 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Wed Aug 25 19:41:18 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed Aug 25 19:47:25 2010 +0200
@@ -447,33 +447,29 @@
 \label{relevance-filter}
 
 \begin{enum}
-\opdefault{relevance\_threshold}{int}{40}
-Specifies the threshold above which facts are considered relevant by the
-relevance filter. The option ranges from 0 to 100, where 0 means that all
-theorems are relevant.
+\opdefault{relevance\_thresholds}{int\_pair}{45~95}
+Specifies the thresholds above which facts are considered relevant by the
+relevance filter. The first threshold is used for the first iteration of the
+relevance filter and the second threshold is used for the last iteration (if it
+is reached). The effective threshold is quadratically interpolated for the other
+iterations. Each threshold ranges from 0 to 100, where 0 means that all theorems
+are relevant and 100 only theorems that refer to previously seen constants.
 
-\opdefault{relevance\_decay}{int}{31}
-Specifies the decay factor, expressed as a percentage, used by the relevance
-filter. This factor is used by the relevance filter to scale down the relevance
-of new facts at each iteration of the filter.
-
-\opdefault{max\_relevant\_per\_iter}{int\_or\_smart}{\textit{smart}}
-Specifies the maximum number of facts that may be added during one iteration of
-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 ATP. A typical value
-would be 50.
+\opdefault{max\_relevant}{int\_or\_smart}{\textit{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 ATP. A typical value would be 300.
 
 \opsmartx{theory\_relevant}{theory\_irrelevant}
 Specifies whether the theory from which a fact comes should be taken into
 consideration by the relevance filter. If the option is set to \textit{smart},
-it is taken to be \textit{true} for SPASS and \textit{false} for E and Vampire,
-because empirical results suggest that these are the best settings.
+it is taken to be \textit{true} for SPASS and \textit{false} for the other ATPs;
+empirical results suggest that these are the best settings.
 
 %\opfalse{defs\_relevant}{defs\_irrelevant}
 %Specifies whether the definition of constants occurring in the formula to prove
 %should be considered particularly relevant. Enabling this option tends to lead
 %to larger problems and typically slows down the ATPs.
-
 \end{enum}
 
 \subsection{Output Format}