# HG changeset patch # User blanchet # Date 1305888479 -7200 # Node ID 75c94e3319ae9856d81307400fbaa481fb0ada1a # Parent ec1ea24d49bcad9dac706cb7ebddd6ec549bf7af more doc fiddling diff -r ec1ea24d49bc -r 75c94e3319ae doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Fri May 20 12:47:59 2011 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Fri May 20 12:47:59 2011 +0200 @@ -296,6 +296,10 @@ \section{Hints} \label{hints} +This section presents a few hints that should help you get the most out of +Sledgehammer and Metis. Frequently (and infrequently) asked questions are +answered in \S\ref{frequently-asked-questions}. + \newcommand\point[1]{{\sl\bfseries#1}\par\nopagebreak} \point{Presimplify the goal} @@ -321,35 +325,40 @@ familiarize themselves with the following options: \begin{enum} -\item[$\bullet$] \textbf{\textit{provers}} specifies the ATP and SMT solvers to -use (e.g., ``\textit{provers} = \textit{e spass remote\_vampire}''). +\item[$\bullet$] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies +the automatic provers (ATPs and SMT solvers) that should be run whenever +Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{e spass +remote\_vampire}''). -\item[$\bullet$] \textbf{\textit{timeout}} controls the provers' time limit. It -is set to 30 seconds, but since Sledgehammer runs asynchronously you should not -hesitate to raise this limit to 60 or 120 seconds if you are the kind of user -who can think clearly while ATPs are active. +\item[$\bullet$] \textbf{\textit{timeout}} (\S\ref{mode-of-operation}) controls +the provers' time limit. It is set to 30 seconds, but since Sledgehammer runs +asynchronously you should not hesitate to raise this limit to 60 or 120 seconds +if you are the kind of user who can think clearly while ATPs are active. -\item[$\bullet$] \textbf{\textit{full\_types}} specifies whether type-sound -encodings should be used. By default, Sledgehammer employs a mixture of -type-sound and type-unsound encodings, occasionally yielding unsound ATP proofs. -(SMT solver proofs should always be sound, although we occasionally find -soundness bugs in the solvers.) +\item[$\bullet$] \textbf{\textit{full\_types}} (\S\ref{problem-encoding}) +specifies whether type-sound encodings should be used. By default, Sledgehammer +employs a mixture of type-sound and type-unsound encodings, occasionally +yielding unsound ATP proofs. (SMT solver proofs should always be sound, although +we occasionally find soundness bugs in the solvers.) -\item[$\bullet$] \textbf{\textit{max\_relevant}} 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 if that helps. +\item[$\bullet$] \textbf{\textit{max\_relevant}} (\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 +if that helps. -\item[$\bullet$] \textbf{\textit{isar\_proof}} specifies that Isar proofs should -be generated, instead of one-liner Metis proofs. The length of the Isar proofs -can be controlled by setting \textit{isar\_shrink\_factor}. +\item[$\bullet$] \textbf{\textit{isar\_proof}} (\S\ref{output-format}) specifies +that Isar proofs should be generated, instead of one-liner Metis proofs. The +length of the Isar proofs can be controlled by setting +\textit{isar\_shrink\_factor} (\S\ref{output-format}). \end{enum} -Options can be set globally using \textbf{sledgehammer\_params}. Fact selection -can be influenced by specifying ``$(\textit{add}{:}~\textit{some\_facts})$'' after -the \textbf{sledgehammer} call to ensure that certain facts are included, or -simply ``$(\textit{some\_facts})$'' to force Sledgehammer to run only with -$\textit{some\_facts}$. +Options can be set globally using \textbf{sledgehammer\_params} +(\S\ref{command-syntax}). Fact selection can be influenced by specifying +``$(\textit{add}{:}~\textit{my\_facts})$'' after the \textbf{sledgehammer} +call to ensure that certain facts are included, or simply +``$(\textit{my\_facts})$'' to force Sledgehammer to run only with +$\textit{my\_facts}$. \section{Frequently Asked Questions} \label{frequently-asked-questions} @@ -429,7 +438,8 @@ 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 \textit{max\_relevant} to, say, 50 or 100. +number of facts, by setting the \textit{max\_relevant} option +(\S\ref{relevance-filter}) to, say, 50 or 100. \point{Why are the Isar proofs generated by Sledgehammer so ugly?} @@ -725,11 +735,11 @@ \opnodefault{prover}{string} Alias for \textit{provers}. -\opnodefault{atps}{string} -Legacy alias for \textit{provers}. +%\opnodefault{atps}{string} +%Legacy alias for \textit{provers}. -\opnodefault{atp}{string} -Legacy alias for \textit{provers}. +%\opnodefault{atp}{string} +%Legacy alias for \textit{provers}. \opdefault{timeout}{float\_or\_none}{\upshape 30} Specifies the maximum number of seconds that the automatic provers should spend @@ -875,18 +885,6 @@ For SMT solvers and ToFoF-E, the type system is always \textit{simple}, irrespective of the value of this option. - -\opdefault{max\_mono\_iters}{int}{\upshape 3} -Specifies the maximum number of iterations for the monomorphization fixpoint -construction. The higher this limit is, the more monomorphic instances are -potentially generated. Whether monomorphization takes place depends on the -type system used. - -\opdefault{max\_new\_mono\_instances}{int}{\upshape 400} -Specifies the maximum number of monomorphic instances to generate beyond -\textit{max\_relevant}. The higher this limit is, the more monomorphic instances -are potentially generated. Whether monomorphization takes place depends on the -type system used. \end{enum} \subsection{Relevance Filter} @@ -907,6 +905,23 @@ empirically found to be appropriate for the prover. A typical value would be 300. +\opdefault{max\_new\_mono\_instances}{int}{\upshape 400} +Specifies the maximum number of monomorphic instances to generate beyond +\textit{max\_relevant}. The higher this limit is, the more monomorphic instances +are potentially generated. Whether monomorphization takes place depends on the +type system used. + +\nopagebreak +{\small See also \textit{type\_sys} (\S\ref{problem-encoding}).} + +\opdefault{max\_mono\_iters}{int}{\upshape 3} +Specifies the maximum number of iterations for the monomorphization fixpoint +construction. The higher this limit is, the more monomorphic instances are +potentially generated. Whether monomorphization takes place depends on the +type system used. + +\nopagebreak +{\small See also \textit{type\_sys} (\S\ref{problem-encoding}).} \end{enum} \subsection{Output Format} diff -r ec1ea24d49bc -r 75c94e3319ae doc-src/manual.bib --- a/doc-src/manual.bib Fri May 20 12:47:59 2011 +0200 +++ b/doc-src/manual.bib Fri May 20 12:47:59 2011 +0200 @@ -421,7 +421,7 @@ @misc{yices, author = {Bruno Dutertre and Leonardo de Moura}, title = {The {Yices} {SMT} Solver}, - publisher = "\url{http://yices.csl.sri.com/tool-paper.pdf}", + howpublished = "\url{http://yices.csl.sri.com/tool-paper.pdf}", year = 2006} @incollection{dybjer91, @@ -648,10 +648,15 @@ number = 5, month = May} -@misc{sine, - author = "Kry\v{s}tof Hoder", - title = "{SInE} (Sumo Inference Engine)", - note = "\url{http://www.cs.man.ac.uk/~hoderk/sine/}"} +@inproceedings{sine, + author = "Kry\v{s}tof Hoder and Andrei Voronkov", + title = "Sine Qua Non for Large Theory Reasoning", + booktitle = {Automated Deduction --- CADE-23}, + publisher = Springer, + series = LNCS, + editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans", + year = 2011, + note = "To appear."} @book{Hudak-Haskell,author={Paul Hudak}, title={The Haskell School of Expression},publisher=CUP,year=2000}