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

author | blanchet |

Fri, 20 Jul 2012 22:19:46 +0200 | |

changeset 48388 | fd7958ebee96 |

parent 48387 | 302cf211fb3f |

child 48389 | 65679f12df4c |

more MaSh docs

doc-src/Sledgehammer/sledgehammer.tex | file | annotate | diff | comparison | revisions | |

src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML | file | annotate | diff | comparison | revisions |

--- a/doc-src/Sledgehammer/sledgehammer.tex Fri Jul 20 22:19:46 2012 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Fri Jul 20 22:19:46 2012 +0200 @@ -397,15 +397,16 @@ \begin{enum} \item[\labelitemi] -The traditional relevance filter, called \emph{MePo}, assigns a score to every -available fact (lemma, theorem, definition, or axiom) based upon how many -constants that fact shares with the conjecture. This process iterates to include -facts relevant to those just accepted. The constants are weighted to give -unusual ones greater significance. MePo copes best when the conjecture contains -some unusual constants; if all the constants are common, it is unable to -discriminate among the hundreds of facts that are picked up. The filter is also -memoryless: It has no information about how many times a particular fact has -been used in a proof, and it cannot learn. +The traditional relevance filter, called \emph{MePo} +(\underline{Me}ng--\underline{Pau}lson), assigns a score to every available fact +(lemma, theorem, definition, or axiom) based upon how many constants that fact +shares with the conjecture. This process iterates to include facts relevant to +those just accepted. The constants are weighted to give unusual ones greater +significance. MePo copes best when the conjecture contains some unusual +constants; if all the constants are common, it is unable to discriminate among +the hundreds of facts that are picked up. The filter is also memoryless: It has +no information about how many times a particular fact has been used in a proof, +and it cannot learn. \item[\labelitemi] An experimental, memoryful alternative to MePo is \emph{MaSh} @@ -1019,6 +1020,25 @@ \label{relevance-filter} \begin{enum} +\opdefault{fact\_filter}{string}{smart} +Specifies the relevance filter to use. The following filters are available: + +\begin{enum} +\item[\labelitemi] \textbf{\textit{mepo}:} +The traditional memoryless MePo relevance filter. + +\item[\labelitemi] \textbf{\textit{mash}:} +The memoryful MaSh machine learner. MaSh relies on the external program +\texttt{mash}, which can be obtained from the author at \authoremail. To install +it, set the environment variable \texttt{MASH\_HOME} to the directory that +contains the \texttt{mash} executable. + +\item[\labelitemi] \textbf{\textit{mesh}:} A combination of MePo and MaSh. + +\item[\labelitemi] \textbf{\textit{smart}:} Use Mesh if \texttt{mash} is +installed and the target prover is an ATP; otherwise, use MePo. +\end{enum} + \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 @@ -1033,6 +1053,11 @@ 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. +\optrue{learn}{dont\_learn} +Specifies whether MaSh should be run automatically by Sledgehammer to learn the +available theories (and hence provide more accurate results). Learning only +takes place if \texttt{mash} is installed. + \opdefault{max\_new\_mono\_instances}{int}{smart} Specifies the maximum number of monomorphic instances to generate beyond \textit{max\_facts}. The higher this limit is, the more monomorphic instances

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:46 2012 +0200 @@ -323,7 +323,7 @@ lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, - max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, + max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, slice = slice, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}