1.1 --- a/doc-src/Nitpick/nitpick.tex Mon Feb 21 17:36:32 2011 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Mon Feb 21 18:02:14 2011 +0100
1.3 @@ -2465,24 +2465,36 @@
1.4
1.5 {\small See also \textit{debug} (\S\ref{output-format}).}
1.6
1.7 +\opargboolorsmart{preconstr}{term}{dont\_preconstr}
1.8 +Specifies whether a datatype value should be preconstructed, meaning Nitpick
1.9 +will reserve a Kodkod atom for it. If a value must necessarily belong to the
1.10 +subset of representable values that approximates a datatype, preconstructing
1.11 +it can speed up the search significantly, especially for high cardinalities. By
1.12 +default, Nitpick inspects the conjecture to infer terms that can be
1.13 +preconstructed.
1.14 +
1.15 +\opsmart{preconstr}{dont\_preconstr}
1.16 +Specifies the default preconstruction setting to use. This can be overridden on
1.17 +a per-term basis using the \textit{preconstr}~\qty{term} option described above.
1.18 +
1.19 +\opdefault{datatype\_sym\_break}{int}{\upshape 5}
1.20 +Specifies an upper bound on the number of datatypes for which Nitpick generates
1.21 +symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
1.22 +considerably, especially for unsatisfiable problems, but too much of it can slow
1.23 +it down.
1.24 +
1.25 +\opdefault{kodkod\_sym\_break}{int}{\upshape 15}
1.26 +Specifies an upper bound on the number of relations for which Kodkod generates
1.27 +symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
1.28 +considerably, especially for unsatisfiable problems, but too much of it can slow
1.29 +it down.
1.30 +
1.31 \optrue{peephole\_optim}{no\_peephole\_optim}
1.32 Specifies whether Nitpick should simplify the generated Kodkod formulas using a
1.33 peephole optimizer. These optimizations can make a significant difference.
1.34 Unless you are tracking down a bug in Nitpick or distrust the peephole
1.35 optimizer, you should leave this option enabled.
1.36
1.37 -\opdefault{datatype\_sym\_break}{int}{\upshape 5}
1.38 -Specifies an upper bound on the number of datatypes for which Nitpick generates
1.39 -symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
1.40 -considerably, especially for unsatisfiable problems, but too much of it can slow
1.41 -it down.
1.42 -
1.43 -\opdefault{kodkod\_sym\_break}{int}{\upshape 15}
1.44 -Specifies an upper bound on the number of relations for which Kodkod generates
1.45 -symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
1.46 -considerably, especially for unsatisfiable problems, but too much of it can slow
1.47 -it down.
1.48 -
1.49 \opdefault{max\_threads}{int}{\upshape 0}
1.50 Specifies the maximum number of threads to use in Kodkod. If this option is set
1.51 to 0, Kodkod will compute an appropriate value based on the number of processor