# HG changeset patch
# User blanchet
# Date 1298307734 -3600
# Node ID 90dd5291afd81c46d6d2f47b7e788b1e18cb5137
# Parent  ef13e3b7cbaf12b7fc9bb781fbfd2db0fa577e07
document new "preconstr" option

diff -r ef13e3b7cbaf -r 90dd5291afd8 doc-src/Nitpick/nitpick.tex
--- 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