summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Wed, 30 Jul 2014 23:52:56 +0200 | |

changeset 57722 | 2c2d5b7f29aa |

parent 57721 | e4858f85e616 |

child 57723 | 668322cd58f4 |

updated docs

--- 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})