# HG changeset patch # User blanchet # Date 1406757176 -7200 # Node ID 2c2d5b7f29aa9da29cda8856eb71b4b84769bcb7 # Parent e4858f85e6160495064b2ce6630da20a1a28429a updated docs diff -r e4858f85e616 -r 2c2d5b7f29aa src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Wed Jul 30 23:52:56 2014 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Wed Jul 30 23:52:56 2014 +0200 @@ -554,26 +554,15 @@ \point{Are generated proofs minimal?} Automatic provers frequently use many more facts than are necessary. -Sledgehammer inclues a minimization tool that takes a set of facts returned by a -given prover and repeatedly calls the same prover, \textit{metis}, or -\textit{smt2} with subsets of those axioms in order to find a minimal set. -Reducing the number of axioms typically improves Metis's speed and success rate, -while also removing superfluous clutter from the proof scripts. +Sledgehammer includes a minimization tool that takes a set of facts returned by +a given prover and repeatedly calls a prover or proof method with subsets of +those facts to find a minimal set. Reducing the number of facts typically helps +reconstruction, while also removing superfluous clutter from the proof scripts. In earlier versions of Sledgehammer, generated proofs were systematically accompanied by a suggestion to invoke the minimization tool. This step is now -performed implicitly if it can be done in a reasonable amount of time (something -that can be guessed from the number of facts in the original proof and the time -it took to find or preplay it). - -In addition, some provers do not provide proofs or sometimes produce incomplete -proofs. The minimizer is then invoked to find out which facts are actually needed -from the (large) set of facts that was initially given to the prover. Finally, -if a prover returns a proof with lots of facts, the minimizer is invoked -automatically since Metis would be unlikely to re-find the proof. -% -Automatic minimization can be forced or disabled using the \textit{minimize} -option (\S\ref{mode-of-operation}). +performed by default but can be disabled using the \textit{minimize} option +(\S\ref{mode-of-operation}). \point{A strange error occurred---what should I do?} @@ -1008,12 +997,9 @@ \nopagebreak {\small See also \textit{verbose} (\S\ref{output-format}).} -\opsmart{minimize}{dont\_minimize} +\optrue{minimize}{dont\_minimize} Specifies whether the minimization tool should be invoked automatically after -proof search. By default, automatic minimization takes place only if -it can be done in a reasonable amount of time (as determined by -the number of facts in the original proof and the time it took to find or -preplay it) or the proof involves an unreasonably large number of facts. +proof search. \nopagebreak {\small See also \textit{preplay\_timeout} (\S\ref{timeouts})