author blanchet Wed, 18 Jul 2012 08:44:03 +0200 changeset 48294 2b0c5553dc46 parent 48293 914ca0827804 child 48295 e0cf12269e60
 NEWS file | annotate | diff | comparison | revisions doc-src/Sledgehammer/sledgehammer.tex file | annotate | diff | comparison | revisions
--- a/NEWS	Wed Jul 18 08:44:03 2012 +0200
+++ b/NEWS	Wed Jul 18 08:44:03 2012 +0200
@@ -42,6 +42,9 @@
* Sledgehammer:

- Rationalized type encodings ("type_enc" option).
+  - Renamed options:
+      max_relevant ~> max_facts
+      relevance_thresholds ~> fact_thresholds

*** Document preparation ***
--- a/doc-src/Sledgehammer/sledgehammer.tex	Wed Jul 18 08:44:03 2012 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed Jul 18 08:44:03 2012 +0200
@@ -358,10 +358,10 @@
and simply write the prover names as a space-separated list (e.g., \textit{e
spass remote\_vampire\/}'').

-\item[\labelitemi] \textbf{\textit{max\_relevant}} (\S\ref{relevance-filter})
+\item[\labelitemi] \textbf{\textit{max\_facts}} (\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
+default, the value is prover-dependent but varies between about 50 and 1000. If
+the provers time out, you can try lowering this value to, say, 25 or 50 and see
if that helps.

\item[\labelitemi] \textbf{\textit{isar\_proof}} (\S\ref{output-format}) specifies
@@ -409,7 +409,7 @@

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 the \textit{max\_relevant} option
+number of facts, by setting the \textit{max\_facts} option
(\S\ref{relevance-filter}) to, say, 25 or 50.

You can also influence which facts are actually selected in a number of ways. If
@@ -1147,7 +1147,13 @@
\label{relevance-filter}

\begin{enum}
-\opdefault{relevance\_thresholds}{float\_pair}{\upshape 0.45~0.85}
+\opdefault{max\_facts}{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. Typical values range between
+50 and 1000.
+
+\opdefault{fact\_thresholds}{float\_pair}{\upshape 0.45~0.85}
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
@@ -1155,15 +1161,9 @@
iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems
are relevant and 1 only theorems that refer to previously seen constants.

-\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. Typical values range between
-50 and 1000.
-
\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
+\textit{max\_facts}. The higher this limit is, the more monomorphic instances
are potentially generated. Whether monomorphization takes place depends on the
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,