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