1.1 --- a/doc-src/Nitpick/nitpick.tex Wed Nov 03 22:33:23 2010 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Wed Nov 03 22:51:32 2010 +0100
1.3 @@ -1888,7 +1888,7 @@
1.4 \item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range
1.5 of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<midarrow\char`\>}.
1.6 \item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
1.7 -\item[$\bullet$] \qtybf{time}: An integer (e.g., 60) or floating-point number
1.8 +\item[$\bullet$] \qtybf{float\_or\_none}: An integer (e.g., 60) or floating-point number
1.9 (e.g., 0.5) expressing a number of seconds, or the keyword \textit{none}
1.10 ($\infty$ seconds).
1.11 \item[$\bullet$] \qtybf{const\/}: The name of a HOL constant.
1.12 @@ -1966,7 +1966,7 @@
1.13 {\small See also \textit{box} (\S\ref{scope-of-search}) and \textit{mono}
1.14 (\S\ref{scope-of-search}).}
1.15
1.16 -\opdefault{card}{int\_seq}{$\mathbf{1}$--$\mathbf{10}$}
1.17 +\opdefault{card}{int\_seq}{\upshape 1--10}
1.18 Specifies the default sequence of cardinalities to use. This can be overridden
1.19 on a per-type basis using the \textit{card}~\qty{type} option described above.
1.20
1.21 @@ -2014,7 +2014,7 @@
1.22 {\small See also \textit{bits} (\S\ref{scope-of-search}) and
1.23 \textit{show\_datatypes} (\S\ref{output-format}).}
1.24
1.25 -\opdefault{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12},\mathbf{14},\mathbf{16}$}
1.26 +\opdefault{bits}{int\_seq}{\upshape 1,2,3,4,6,8,10,12,14,16}
1.27 Specifies the number of bits to use to represent natural numbers and integers in
1.28 binary, excluding the sign bit. The minimum is 1 and the maximum is 31.
1.29
1.30 @@ -2064,12 +2064,12 @@
1.31 {\small See also \textit{wf} (\S\ref{scope-of-search}) and
1.32 \textit{star\_linear\_preds} (\S\ref{optimizations}).}
1.33
1.34 -\opdefault{iter}{int\_seq}{$\mathbf{0{,}1{,}2{,}4{,}8{,}12{,}16{,}20{,}24{,}28}$}
1.35 +\opdefault{iter}{int\_seq}{\upshape 0{,}1{,}2{,}4{,}8{,}12{,}16{,}20{,}24{,}28}
1.36 Specifies the sequence of iteration counts to use when unrolling (co)in\-duc\-tive
1.37 predicates. This can be overridden on a per-predicate basis using the
1.38 \textit{iter} \qty{const} option above.
1.39
1.40 -\opdefault{bisim\_depth}{int\_seq}{$\mathbf{9}$}
1.41 +\opdefault{bisim\_depth}{int\_seq}{\upshape 9}
1.42 Specifies the sequence of iteration counts to use when unrolling the
1.43 bisimilarity predicate generated by Nitpick for coinductive datatypes. A value
1.44 of $-1$ means that no predicate is generated, in which case Nitpick performs an
1.45 @@ -2214,7 +2214,7 @@
1.46 \opnodefault{show\_all}{bool}
1.47 Abbreviation for \textit{show\_datatypes} and \textit{show\_consts}.
1.48
1.49 -\opdefault{max\_potential}{int}{$\mathbf{1}$}
1.50 +\opdefault{max\_potential}{int}{\upshape 1}
1.51 Specifies the maximum number of potential counterexamples to display. Setting
1.52 this option to 0 speeds up the search for a genuine counterexample. This option
1.53 is implicitly set to 0 for automatic runs. If you set this option to a value
1.54 @@ -2226,7 +2226,7 @@
1.55 {\small See also \textit{check\_potential} (\S\ref{authentication}) and
1.56 \textit{sat\_solver} (\S\ref{optimizations}).}
1.57
1.58 -\opdefault{max\_genuine}{int}{$\mathbf{1}$}
1.59 +\opdefault{max\_genuine}{int}{\upshape 1}
1.60 Specifies the maximum number of genuine counterexamples to display. If you set
1.61 this option to a value greater than 1, you will need an incremental SAT solver,
1.62 such as \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that
1.63 @@ -2267,7 +2267,7 @@
1.64 arguments that are not accounted for are left alone, as if the specification had
1.65 been $1,\ldots,1,n_1,\ldots,n_k$.
1.66
1.67 -\opdefault{format}{int\_seq}{$\mathbf{1}$}
1.68 +\opdefault{format}{int\_seq}{\upshape 1}
1.69 Specifies the default format to use. Irrespective of the default format, the
1.70 extra arguments to a Skolem constant corresponding to the outer bound variables
1.71 are kept separated from the remaining arguments, the \textbf{for} arguments of
1.72 @@ -2484,19 +2484,19 @@
1.73 Unless you are tracking down a bug in Nitpick or distrust the peephole
1.74 optimizer, you should leave this option enabled.
1.75
1.76 -\opdefault{datatype\_sym\_break}{int}{5}
1.77 +\opdefault{datatype\_sym\_break}{int}{\upshape 5}
1.78 Specifies an upper bound on the number of datatypes for which Nitpick generates
1.79 symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
1.80 considerably, especially for unsatisfiable problems, but too much of it can slow
1.81 it down.
1.82
1.83 -\opdefault{kodkod\_sym\_break}{int}{15}
1.84 +\opdefault{kodkod\_sym\_break}{int}{\upshape 15}
1.85 Specifies an upper bound on the number of relations for which Kodkod generates
1.86 symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
1.87 considerably, especially for unsatisfiable problems, but too much of it can slow
1.88 it down.
1.89
1.90 -\opdefault{max\_threads}{int}{0}
1.91 +\opdefault{max\_threads}{int}{\upshape 0}
1.92 Specifies the maximum number of threads to use in Kodkod. If this option is set
1.93 to 0, Kodkod will compute an appropriate value based on the number of processor
1.94 cores available. The option is implicitly set to 1 for automatic runs.
1.95 @@ -2510,7 +2510,7 @@
1.96 \label{timeouts}
1.97
1.98 \begin{enum}
1.99 -\opdefault{timeout}{time}{$\mathbf{30}$}
1.100 +\opdefault{timeout}{float\_or\_none}{\upshape 30}
1.101 Specifies the maximum number of seconds that the \textbf{nitpick} command should
1.102 spend looking for a counterexample. Nitpick tries to honor this constraint as
1.103 well as it can but offers no guarantees. For automatic runs,
1.104 @@ -2521,7 +2521,7 @@
1.105 \nopagebreak
1.106 {\small See also \textit{max\_threads} (\S\ref{optimizations}).}
1.107
1.108 -\opdefault{tac\_timeout}{time}{$\mathbf{0.5}$}
1.109 +\opdefault{tac\_timeout}{float\_or\_none}{\upshape 0.5}
1.110 Specifies the maximum number of seconds that the \textit{auto} tactic should use
1.111 when checking a counterexample, and similarly that \textit{lexicographic\_order}
1.112 and \textit{size\_change} should use when checking whether a (co)in\-duc\-tive