# HG changeset patch
# User blanchet
# Date 1305793453 -7200
# Node ID 9eef1dc200a81837a7ffd4ae10fa6ebec19efa98
# Parent  b48529f4188812cc98faf50359a8102acfc24749
updated option documentation

diff -r b48529f41888 -r 9eef1dc200a8 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Thu May 19 10:24:13 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu May 19 10:24:13 2011 +0200
@@ -637,7 +637,7 @@
 developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
 servers. This ATP supports a fragment of the TPTP many-typed first-order format
 (TFF). It is supported primarily for experimenting with the
-\textit{type\_sys} $=$ \textit{simple\_types} option (\S\ref{problem-encoding}).
+\textit{type\_sys} $=$ \textit{simple} option (\S\ref{problem-encoding}).
 
 \item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover
 developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
@@ -768,8 +768,8 @@
 Monomorphization can simplify reasoning but also leads to larger fact bases,
 which can slow down the ATPs.
 
-\item[$\bullet$] \textbf{\textit{simple\_types}:} Use the prover's support for
-simply typed first-order logic if available; otherwise, fall back on
+\item[$\bullet$] \textbf{\textit{simple}:} Use the prover's support for simply
+typed first-order logic if available; otherwise, fall back on
 \textit{mangled\_preds}. The problem is monomorphized.
 
 \item[$\bullet$]
@@ -787,28 +787,28 @@
 
 \item[$\bullet$]
 \textbf{%
-\textit{mono\_preds}?, \textit{mono\_tags}?, \textit{simple\_types}?, \\
+\textit{mono\_preds}?, \textit{mono\_tags}?, \textit{simple}?, \\
 \textit{mangled\_preds}?, \textit{mangled\_tags}?:} \\
-The type systems \textit{mono\_preds}, \textit{mono\_tags}, \textit{simple\_types},
+The type systems \textit{mono\_preds}, \textit{mono\_tags}, \textit{simple},
 \textit{mangled\_preds}, and \textit{mangled\_tags} are fully typed and
 virtually sound---except for pathological cases, all found proofs are
 type-correct. For each of these, Sledgehammer also provides a lighter (but
 virtually sound) variant identified by a question mark (`{?}')\ that detects and
-erases monotonic types, notably infinite types. (For \textit{simple\_types}, the
-types are not actually erased but rather replaced by a shared uniform type of
+erases monotonic types, notably infinite types. (For \textit{simple}, the types
+are not actually erased but rather replaced by a shared uniform type of
 individuals.)
 
 \item[$\bullet$]
 \textbf{%
 \textit{poly\_tags}!, \textit{mono\_preds}!, \textit{mono\_tags}!, \\
-\textit{simple\_types}!, \textit{mangled\_preds}!, \textit{mangled\_tags}!:} \\
+\textit{simple}!, \textit{mangled\_preds}!, \textit{mangled\_tags}!:} \\
 The type systems \textit{poly\_preds}, \textit{poly\_tags},
-\textit{mono\_preds}, \textit{mono\_tags}, \textit{simple\_types},
+\textit{mono\_preds}, \textit{mono\_tags}, \textit{simple},
 \textit{mangled\_preds}, and \textit{mangled\_tags} also admit a somewhat
 unsound (but very efficient) variant identified by an exclamation mark (`{!}')
 that detects and erases erases all types except those that are clearly finite
-(e.g., \textit{bool}). (For \textit{simple\_types}, the types are not actually
-erased but rather replaced by a shared uniform type of individuals.)
+(e.g., \textit{bool}). (For \textit{simple}, the types are not actually erased
+but rather replaced by a shared uniform type of individuals.)
 
 \item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled,
 uses a fully typed, virtually sound encoding; otherwise, uses any encoding. The
@@ -816,15 +816,22 @@
 that ATP.
 \end{enum}
 
-For SMT solvers and ToFoF-E, the type system is always \textit{simple\_types}.
+In addition, all the \textit{preds} and \textit{tags} type systems are available
+in two variants, a lightweight and a heavyweight variant. The lightweight
+variants are generally more efficient and are the default; the heavyweight
+variants are identified by a \textit{\_heavy} suffix (e.g.,
+\textit{mangled\_preds\_heavy}{?}).
 
-\opdefault{max\_mono\_iters}{int}{\upshape 5}
+For SMT solvers and ToFoF-E, the type system is always \textit{simple},
+irrespective of the value of this option.
+
+\opdefault{max\_mono\_iters}{int}{\upshape 3}
 Specifies the maximum number of iterations for the monomorphization fixpoint
 construction. The higher this limit is, the more monomorphic instances are
 potentially generated. Whether monomorphization takes place depends on the
 type system used.
 
-\opdefault{max\_new\_mono\_instances}{int}{\upshape 250}
+\opdefault{max\_new\_mono\_instances}{int}{\upshape 400}
 Specifies the maximum number of monomorphic instances to generate beyond
 \textit{max\_relevant}. The higher this limit is, the more monomorphic instances
 are potentially generated. Whether monomorphization takes place depends on the