--- a/doc-src/Nitpick/nitpick.tex Mon Feb 21 17:36:32 2011 +0100
+++ b/doc-src/Nitpick/nitpick.tex Mon Feb 21 18:02:14 2011 +0100
@@ -2465,11 +2465,17 @@
{\small See also \textit{debug} (\S\ref{output-format}).}
-\optrue{peephole\_optim}{no\_peephole\_optim}
-Specifies whether Nitpick should simplify the generated Kodkod formulas using a
-peephole optimizer. These optimizations can make a significant difference.
-Unless you are tracking down a bug in Nitpick or distrust the peephole
-optimizer, you should leave this option enabled.
+\opargboolorsmart{preconstr}{term}{dont\_preconstr}
+Specifies whether a datatype value should be preconstructed, meaning Nitpick
+will reserve a Kodkod atom for it. If a value must necessarily belong to the
+subset of representable values that approximates a datatype, preconstructing
+it can speed up the search significantly, especially for high cardinalities. By
+default, Nitpick inspects the conjecture to infer terms that can be
+preconstructed.
+
+\opsmart{preconstr}{dont\_preconstr}
+Specifies the default preconstruction setting to use. This can be overridden on
+a per-term basis using the \textit{preconstr}~\qty{term} option described above.
\opdefault{datatype\_sym\_break}{int}{\upshape 5}
Specifies an upper bound on the number of datatypes for which Nitpick generates
@@ -2483,6 +2489,12 @@
considerably, especially for unsatisfiable problems, but too much of it can slow
it down.
+\optrue{peephole\_optim}{no\_peephole\_optim}
+Specifies whether Nitpick should simplify the generated Kodkod formulas using a
+peephole optimizer. These optimizations can make a significant difference.
+Unless you are tracking down a bug in Nitpick or distrust the peephole
+optimizer, you should leave this option enabled.
+
\opdefault{max\_threads}{int}{\upshape 0}
Specifies the maximum number of threads to use in Kodkod. If this option is set
to 0, Kodkod will compute an appropriate value based on the number of processor