author blanchet Mon, 21 Feb 2011 18:02:14 +0100 changeset 41804 90dd5291afd8 parent 41803 ef13e3b7cbaf child 41805 a96684499e85
document new "preconstr" option
--- 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 @@

-\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.
+
to 0, Kodkod will compute an appropriate value based on the number of processor