1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Tue Jul 26 22:53:06 2011 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue Jul 26 22:53:06 2011 +0200
     1.3 @@ -886,24 +886,24 @@
     1.4  \item[$\bullet$] \textbf{\textit{erased} (very unsound):} No type information is
     1.5  supplied to the ATP. Types are simply erased.
     1.6  
     1.7 -\item[$\bullet$] \textbf{\textit{poly\_preds} (sound):} Types are encoded using
     1.8 -a predicate \textit{has\_\allowbreak type\/}$(\tau, t)$ that restricts the range
     1.9 -of bound variables. Constants are annotated with their types, supplied as extra
    1.10 +\item[$\bullet$] \textbf{\textit{poly\_guards} (sound):} Types are encoded using
    1.11 +a predicate \textit{has\_\allowbreak type\/}$(\tau, t)$ that guards bound
    1.12 +variables. Constants are annotated with their types, supplied as additional
    1.13  arguments, to resolve overloading.
    1.14  
    1.15  \item[$\bullet$] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
    1.16  tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$.
    1.17  
    1.18  \item[$\bullet$] \textbf{\textit{poly\_args} (unsound):}
    1.19 -Like for \textit{poly\_preds} constants are annotated with their types to
    1.20 +Like for \textit{poly\_guards} constants are annotated with their types to
    1.21  resolve overloading, but otherwise no type information is encoded. This
    1.22  coincides with the default encoding used by the \textit{metis} command.
    1.23  
    1.24  \item[$\bullet$]
    1.25  \textbf{%
    1.26 -\textit{mono\_preds}, \textit{mono\_tags} (sound);
    1.27 +\textit{mono\_guards}, \textit{mono\_tags} (sound);
    1.28  \textit{mono\_args} (unsound):} \\
    1.29 -Similar to \textit{poly\_preds}, \textit{poly\_tags}, and \textit{poly\_args},
    1.30 +Similar to \textit{poly\_guards}, \textit{poly\_tags}, and \textit{poly\_args},
    1.31  respectively, but the problem is additionally monomorphized, meaning that type
    1.32  variables are instantiated with heuristically chosen ground types.
    1.33  Monomorphization can simplify reasoning but also leads to larger fact bases,
    1.34 @@ -911,11 +911,11 @@
    1.35  
    1.36  \item[$\bullet$]
    1.37  \textbf{%
    1.38 -\textit{mangled\_preds},
    1.39 +\textit{mangled\_guards},
    1.40  \textit{mangled\_tags} (sound); \\
    1.41  \textit{mangled\_args} (unsound):} \\
    1.42  Similar to
    1.43 -\textit{mono\_preds}, \textit{mono\_tags}, and \textit{mono\_args},
    1.44 +\textit{mono\_guards}, \textit{mono\_tags}, and \textit{mono\_args},
    1.45  respectively but types are mangled in constant names instead of being supplied
    1.46  as ground term arguments. The binary predicate $\mathit{has\_type\/}(\tau, t)$
    1.47  becomes a unary predicate $\mathit{has\_type\_}\tau(t)$, and the binary function
    1.48 @@ -924,35 +924,35 @@
    1.49  
    1.50  \item[$\bullet$] \textbf{\textit{simple} (sound):} Exploit simple first-order
    1.51  types if the prover supports the TFF or THF syntax; otherwise, fall back on
    1.52 -\textit{mangled\_preds}. The problem is monomorphized.
    1.53 +\textit{mangled\_guards}. The problem is monomorphized.
    1.54  
    1.55  \item[$\bullet$] \textbf{\textit{simple\_higher} (sound):} Exploit simple
    1.56  higher-order types if the prover supports the THF syntax; otherwise, fall back
    1.57 -on \textit{simple} or \textit{mangled\_preds\_heavy}. The problem is
    1.58 +on \textit{simple} or \textit{mangled\_guards\_heavy}. The problem is
    1.59  monomorphized.
    1.60  
    1.61  \item[$\bullet$]
    1.62  \textbf{%
    1.63 -\textit{poly\_preds}?, \textit{poly\_tags}?, \textit{mono\_preds}?, \textit{mono\_tags}?, \\
    1.64 -\textit{mangled\_preds}?, \textit{mangled\_tags}?, \textit{simple}?, \textit{simple\_higher}? (quasi-sound):} \\
    1.65 -The type encodings \textit{poly\_preds}, \textit{poly\_tags},
    1.66 -\textit{mono\_preds}, \textit{mono\_tags}, \textit{mangled\_preds},
    1.67 -\textit{mangled\_tags}, \textit{simple}, and \textit{simple\_higher} are fully
    1.68 +\textit{poly\_guards}?, \textit{poly\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\
    1.69 +\textit{mangled\_guards}?, \textit{mangled\_tags}?, \textit{simple}? (quasi-sound):} \\
    1.70 +The type encodings \textit{poly\_guards}, \textit{poly\_tags},
    1.71 +\textit{mono\_guards}, \textit{mono\_tags}, \textit{mangled\_guards},
    1.72 +\textit{mangled\_tags}, and \textit{simple} are fully
    1.73  typed and sound. For each of these, Sledgehammer also provides a lighter,
    1.74  virtually sound variant identified by a question mark (`{?}')\ that detects and
    1.75 -erases monotonic types, notably infinite types. (For \textit{simple} and
    1.76 -\textit{simple\_higher}, the types are not actually erased but rather replaced
    1.77 -by a shared uniform type of individuals.) As argument to the \textit{metis}
    1.78 -proof method, the question mark is replaced by a \hbox{``\textit{\_query}''}
    1.79 -suffix. If the \emph{sound} option is enabled, these encodings are fully sound.
    1.80 +erases monotonic types, notably infinite types. (For \textit{simple}, the types
    1.81 +are not actually erased but rather replaced by a shared uniform type of
    1.82 +individuals.) As argument to the \textit{metis} proof method, the question mark
    1.83 +is replaced by a \hbox{``\textit{\_query}''} suffix. If the \emph{sound} option
    1.84 +is enabled, these encodings are fully sound.
    1.85  
    1.86  \item[$\bullet$]
    1.87  \textbf{%
    1.88 -\textit{poly\_preds}!, \textit{poly\_tags}!, \textit{mono\_preds}!, \textit{mono\_tags}!, \\
    1.89 -\textit{mangled\_preds}!, \textit{mangled\_tags}!, \textit{simple}!, \textit{simple\_higher}! \\
    1.90 +\textit{poly\_guards}!, \textit{poly\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\
    1.91 +\textit{mangled\_guards}!, \textit{mangled\_tags}!, \textit{simple}!, \textit{simple\_higher}! \\
    1.92  (mildly unsound):} \\
    1.93 -The type encodings \textit{poly\_preds}, \textit{poly\_tags},
    1.94 -\textit{mono\_preds}, \textit{mono\_tags}, \textit{mangled\_preds},
    1.95 +The type encodings \textit{poly\_guards}, \textit{poly\_tags},
    1.96 +\textit{mono\_guards}, \textit{mono\_tags}, \textit{mangled\_guards},
    1.97  \textit{mangled\_tags}, \textit{simple}, and \textit{simple\_higher} also admit
    1.98  a mildly unsound (but very efficient) variant identified by an exclamation mark
    1.99  (`{!}') that detects and erases erases all types except those that are clearly
   1.100 @@ -965,11 +965,11 @@
   1.101  the ATP and should be the most efficient virtually sound encoding for that ATP.
   1.102  \end{enum}
   1.103  
   1.104 -In addition, all the \textit{preds} and \textit{tags} type encodings are
   1.105 +In addition, all the \textit{guards} and \textit{tags} type encodings are
   1.106  available in two variants, a lightweight and a heavyweight variant. The
   1.107  lightweight variants are generally more efficient and are the default; the
   1.108  heavyweight variants are identified by a \textit{\_heavy} suffix (e.g.,
   1.109 -\textit{mangled\_preds\_heavy}{?}).
   1.110 +\textit{mangled\_guards\_heavy}{?}).
   1.111  
   1.112  For SMT solvers, the type encoding is always \textit{simple}, irrespective of
   1.113  the value of this option.