# HG changeset patch # User blanchet # Date 1338971705 -7200 # Node ID 433787f8145e3bd9de8ea82f901821cfdf582563 # Parent fcb2292aa2604fea0e2f9725766d29e9bda9655b updated docs diff -r fcb2292aa260 -r 433787f8145e doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Wed Jun 06 10:35:05 2012 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Jun 06 10:35:05 2012 +0200 @@ -1037,12 +1037,12 @@ below) is enabled. \begin{enum} -\item[\labelitemi] \textbf{\textit{erased} (very unsound):} No type information is +\item[\labelitemi] \textbf{\textit{erased} (unsound):} No type information is supplied to the ATP, not even to resolve overloading. Types are simply erased. \item[\labelitemi] \textbf{\textit{poly\_guards} (sound):} Types are encoded using a predicate \const{g}$(\tau, t)$ that guards bound -variables. Constants are annotated with their types, supplied as additional +variables. Constants are annotated with their types, supplied as extra arguments, to resolve overloading. \item[\labelitemi] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is @@ -1051,7 +1051,7 @@ \item[\labelitemi] \textbf{\textit{poly\_args} (unsound):} Like for \textit{poly\_guards} constants are annotated with their types to resolve overloading, but otherwise no type information is encoded. This -coincides with the default encoding used by the \textit{metis} command. +is the default encoding used by the \textit{metis} command. \item[\labelitemi] \textbf{% @@ -1120,38 +1120,6 @@ \textit{metis} proof method, the `\hbox{@?}' suffix is replaced by \hbox{``\textit{\_at\_query\/}''}. -\item[\labelitemi] -\textbf{% -\textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\ -\textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\ -\textit{mono\_native}!, \textit{mono\_native\_higher}! (mildly unsound):} \\ -The type encodings \textit{poly\_guards}, \textit{poly\_tags}, -\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards}, -\textit{mono\_tags}, \textit{mono\_native}, and \textit{mono\_native\_higher} -also admit a mildly unsound (but very efficient) variant identified by an -exclamation mark (`\hbox{!}') that detects and erases erases all types except -those that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_native} -and \textit{mono\_native\_higher}, the types are not actually erased but rather -replaced by a shared uniform type of individuals.) As argument to the -\textit{metis} proof method, the exclamation mark is replaced by the suffix -\hbox{``\textit{\_bang\/}''}. - -\item[\labelitemi] -\textbf{% -\textit{poly\_guards}!!, \textit{poly\_tags}!!, \textit{raw\_mono\_guards}!!, \\ -\textit{raw\_mono\_tags}!!, \textit{mono\_guards}!!, \textit{mono\_tags}!! \\ -(mildly unsound):} \\ -Even lighter versions of the `\hbox{!}' encodings. As argument to the -\textit{metis} proof method, the `\hbox{!!}' suffix is replaced by -\hbox{``\textit{\_bang\_bang\/}''}. - -\item[\labelitemi] -\textbf{% -\textit{poly\_guards}@!, \textit{raw\_mono\_guards}@! (mildly unsound):} \\ -Alternative versions of the `\hbox{!!}' encodings. As argument to the -\textit{metis} proof method, the `\hbox{@!}' suffix is replaced by -\hbox{``\textit{\_at\_bang\/}''}. - \item[\labelitemi] \textbf{\textit{smart}:} The actual encoding used depends on the ATP and should be the most efficient sound encoding for that ATP. \end{enum}