document new "total_consts" option
Mon, 28 Feb 2011 17:53:10 +0100
changeset 41857 07573743208f
parent 41856 7244589c8ccc
child 41858 37ce158d6266
document new "total_consts" option
--- a/doc-src/Nitpick/nitpick.tex	Mon Feb 28 17:53:10 2011 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Mon Feb 28 17:53:10 2011 +0100
@@ -2477,6 +2477,14 @@
 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.
+Specifies whether constants occurring in the problem other than constructors can
+be assumed to be considered total for the representable values that approximate
+a datatype. This option is highly incomplete; it should be used only for
+problems that do not construct datatype values explicitly. Since this option is
+(in rare cases) unsound, counterexamples generated under these conditions are
+tagged as ``quasi genuine.''
 \opdefault{datatype\_sym\_break}{int}{\upshape 5}
 Specifies an upper bound on the number of datatypes for which Nitpick generates
 symmetry breaking predicates. Symmetry breaking can speed up the SAT solver