# HG changeset patch # User blanchet # Date 1306485007 -7200 # Node ID 29be053ec75ba8847f42ec52cb029c146b5f5e48 # Parent e23f61546cf0850fb4e00c1b74a793937b6904e4 document relevance filter a bit more diff -r e23f61546cf0 -r 29be053ec75b doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Fri May 27 10:30:07 2011 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Fri May 27 10:30:07 2011 +0200 @@ -461,6 +461,34 @@ number of facts, by setting the \textit{max\_relevant} option (\S\ref{relevance-filter}) to, say, 50 or 100. +You can also influence which facts are actually selected in a number of ways. If +you simply want to ensure that a fact is included, you can specify it using the +``$(\textit{add}{:}~\textit{my\_facts})$'' syntax. For example: +% +\prew +\textbf{sledgehammer} (\textit{add}: \textit{hd.simps} \textit{tl.simps}) +\postw +% +The specified facts then replace the least relevant facts that would otherwise be +included; the other selected facts remain the same. +If you want to direct the selection in a particular direction, you can specify +the facts via \textbf{using}: +% +\prew +\textbf{using} \textit{hd.simps} \textit{tl.simps} \\ +\textbf{sledgehammer} +\postw +% +The facts are then more likely to be selected than otherwise, and if they are +selected at iteration $j$ they also influence which facts are selected at +iterations $j + 1$, $j + 2$, etc. To give them even more weight, try +% +\prew +\textbf{using} \textit{hd.simps} \textit{tl.simps} \\ +\textbf{apply}~\textbf{--} \\ +\textbf{sledgehammer} +\postw + \point{Why are the Isar proofs generated by Sledgehammer so ugly?} The current implementation is experimental and explodes exponentially in the @@ -478,11 +506,11 @@ \point{Why does the minimizer sometimes starts of its own?} -There are two scenarios in which this can happen. First, some provers (e.g., -CVC3 and Yices) do not provide proofs or provide incomplete proofs. The -minimizer is then invoked to find out which facts are actually needed from the -(large) set of facts that was initinally given to the prover. Second, if a -prover returns a proof with lots of facts, the minimizer is invoked +There are two scenarios in which this can happen. First, some provers (notably +CVC3, Satallax, and Yices) do not provide proofs or sometimes provide incomplete +proofs. The minimizer is then invoked to find out which facts are actually +needed from the (large) set of facts that was initinally given to the prover. +Second, if a prover returns a proof with lots of facts, the minimizer is invoked automatically since Metis is unlikely to refind the proof. \point{What is metisFT?}