# HG changeset patch # User blanchet # Date 1342593843 -7200 # Node ID 2b0c5553dc46601eb77566459adc918198289c7b # Parent 914ca082780450e2ce25cc251f313cfe5e80647d doc updates diff -r 914ca0827804 -r 2b0c5553dc46 NEWS --- 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 *** diff -r 914ca0827804 -r 2b0c5553dc46 doc-src/Sledgehammer/sledgehammer.tex --- 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,