doc-src/Nitpick/nitpick.tex

 \item[$\bullet$] \qtybf{int\/}: An integer. Negative integers are prefixed with a hyphen.
 \item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
 \item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range
 of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<midarrow\char`\>}.
 \item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
-\item[$\bullet$] \qtybf{time}: An integer (e.g., 60) or floating-point number
+\item[$\bullet$] \qtybf{float\_or\_none}: An integer (e.g., 60) or floating-point number
 (e.g., 0.5) expressing a number of seconds, or the keyword \textit{none}
 ($\infty$ seconds).
 \item[$\bullet$] \qtybf{const\/}: The name of a HOL constant.
 \item[$\bullet$] \qtybf{term}: A HOL term (e.g., ``$f~x$'').
 \item[$\bullet$] \qtybf{term\_list\/}: A space-separated list of HOL terms (e.g.,

 
 \nopagebreak
 {\small See also \textit{box} (\S\ref{scope-of-search}) and \textit{mono}
 (\S\ref{scope-of-search}).}
 
-\opdefault{card}{int\_seq}{$\mathbf{1}$--$\mathbf{10}$}
+\opdefault{card}{int\_seq}{\upshape 1--10}
 Specifies the default sequence of cardinalities to use. This can be overridden
 on a per-type basis using the \textit{card}~\qty{type} option described above.
 
 \oparg{max}{const}{int\_seq}
 Specifies the sequence of maximum multiplicities to use for a given

 \textit{Suc}, \textit{gcd}, or \textit{lcm}.
 
 {\small See also \textit{bits} (\S\ref{scope-of-search}) and
 \textit{show\_datatypes} (\S\ref{output-format}).}
 
-\opdefault{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12},\mathbf{14},\mathbf{16}$}
+\opdefault{bits}{int\_seq}{\upshape 1,2,3,4,6,8,10,12,14,16}
 Specifies the number of bits to use to represent natural numbers and integers in
 binary, excluding the sign bit. The minimum is 1 and the maximum is 31.
 
 {\small See also \textit{binary\_ints} (\S\ref{scope-of-search}).}
 

 domain.
 
 {\small See also \textit{wf} (\S\ref{scope-of-search}) and
 \textit{star\_linear\_preds} (\S\ref{optimizations}).}
 
-\opdefault{iter}{int\_seq}{$\mathbf{0{,}1{,}2{,}4{,}8{,}12{,}16{,}20{,}24{,}28}$}
+\opdefault{iter}{int\_seq}{\upshape 0{,}1{,}2{,}4{,}8{,}12{,}16{,}20{,}24{,}28}
 Specifies the sequence of iteration counts to use when unrolling (co)in\-duc\-tive
 predicates. This can be overridden on a per-predicate basis using the
 \textit{iter} \qty{const} option above.
 
-\opdefault{bisim\_depth}{int\_seq}{$\mathbf{9}$}
+\opdefault{bisim\_depth}{int\_seq}{\upshape 9}
 Specifies the sequence of iteration counts to use when unrolling the
 bisimilarity predicate generated by Nitpick for coinductive datatypes. A value
 of $-1$ means that no predicate is generated, in which case Nitpick performs an
 after-the-fact check to see if the known coinductive datatype values are
 bidissimilar. If two values are found to be bisimilar, the counterexample is

 genuine, but they can clutter the output.
 
 \opnodefault{show\_all}{bool}
 Abbreviation for \textit{show\_datatypes} and \textit{show\_consts}.
 
-\opdefault{max\_potential}{int}{$\mathbf{1}$}
+\opdefault{max\_potential}{int}{\upshape 1}
 Specifies the maximum number of potential counterexamples to display. Setting
 this option to 0 speeds up the search for a genuine counterexample. This option
 is implicitly set to 0 for automatic runs. If you set this option to a value
 greater than 1, you will need an incremental SAT solver, such as
 \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that many of

 
 \nopagebreak
 {\small See also \textit{check\_potential} (\S\ref{authentication}) and
 \textit{sat\_solver} (\S\ref{optimizations}).}
 
-\opdefault{max\_genuine}{int}{$\mathbf{1}$}
+\opdefault{max\_genuine}{int}{\upshape 1}
 Specifies the maximum number of genuine counterexamples to display. If you set
 this option to a value greater than 1, you will need an incremental SAT solver,
 such as \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that
 many of the counterexamples may be identical.
 

 of values $n_1,\ldots,n_k$ tells Nitpick to show the last $n_k$ arguments as an
 $n_k$-tuple, the previous $n_{k-1}$ arguments as an $n_{k-1}$-tuple, and so on;
 arguments that are not accounted for are left alone, as if the specification had
 been $1,\ldots,1,n_1,\ldots,n_k$.
 
-\opdefault{format}{int\_seq}{$\mathbf{1}$}
+\opdefault{format}{int\_seq}{\upshape 1}
 Specifies the default format to use. Irrespective of the default format, the
 extra arguments to a Skolem constant corresponding to the outer bound variables
 are kept separated from the remaining arguments, the \textbf{for} arguments of
 an inductive definitions are kept separated from the remaining arguments, and
 the iteration counter of an unrolled inductive definition is shown alone. The

 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{datatype\_sym\_break}{int}{5}
+\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
 considerably, especially for unsatisfiable problems, but too much of it can slow
 it down.
 
-\opdefault{kodkod\_sym\_break}{int}{15}
+\opdefault{kodkod\_sym\_break}{int}{\upshape 15}
 Specifies an upper bound on the number of relations for which Kodkod generates
 symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
 considerably, especially for unsatisfiable problems, but too much of it can slow
 it down.
 
-\opdefault{max\_threads}{int}{0}
+\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
 cores available. The option is implicitly set to 1 for automatic runs.
 
 \nopagebreak

 
 \subsection{Timeouts}
 \label{timeouts}
 
 \begin{enum}
-\opdefault{timeout}{time}{$\mathbf{30}$}
+\opdefault{timeout}{float\_or\_none}{\upshape 30}
 Specifies the maximum number of seconds that the \textbf{nitpick} command should
 spend looking for a counterexample. Nitpick tries to honor this constraint as
 well as it can but offers no guarantees. For automatic runs,
 \textit{timeout} is ignored; instead, Auto Quickcheck and Auto Nitpick share
 a time slot whose length is specified by the ``Auto Counterexample Time
 Limit'' option in Proof General.
 
 \nopagebreak
 {\small See also \textit{max\_threads} (\S\ref{optimizations}).}
 
-\opdefault{tac\_timeout}{time}{$\mathbf{0.5}$}
+\opdefault{tac\_timeout}{float\_or\_none}{\upshape 0.5}
 Specifies the maximum number of seconds that the \textit{auto} tactic should use
 when checking a counterexample, and similarly that \textit{lexicographic\_order}
 and \textit{size\_change} should use when checking whether a (co)in\-duc\-tive
 predicate is well-founded. Nitpick tries to honor this constraint as well as it
 can but offers no guarantees.