1.1 --- a/doc-src/Nitpick/nitpick.tex Mon Dec 14 16:48:49 2009 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Thu Dec 17 15:22:11 2009 +0100
1.3 @@ -436,12 +436,10 @@
1.4 \label{natural-numbers-and-integers}
1.5
1.6 Because of the axiom of infinity, the type \textit{nat} does not admit any
1.7 -finite models. To deal with this, Nitpick considers prefixes $\{0,\, 1,\,
1.8 -\ldots,\, K - 1\}$ of \textit{nat} (where $K = \textit{card}~\textit{nat}$) and
1.9 -maps all other numbers to the undefined value ($\unk$). The type \textit{int} is
1.10 -handled in a similar way: If $K = \textit{card}~\textit{int}$, the subset of
1.11 -\textit{int} known to Nitpick is $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor
1.12 -K/2 \rfloor\}$. Undefined values lead to a three-valued logic.
1.13 +finite models. To deal with this, Nitpick's approach is to consider finite
1.14 +subsets $N$ of \textit{nat} and maps all numbers $\notin N$ to the undefined
1.15 +value (displayed as `$\unk$'). The type \textit{int} is handled similarly.
1.16 +Internally, undefined values lead to a three-valued logic.
1.17
1.18 Here is an example involving \textit{int}:
1.19
1.20 @@ -456,15 +454,26 @@
1.21 \hbox{}\qquad\qquad $n = 0$
1.22 \postw
1.23
1.24 +Internally, Nitpick uses either a unary or a binary representation of numbers.
1.25 +The unary representation is more efficient but only suitable for numbers very
1.26 +close to zero. By default, Nitpick attempts to choose the more appropriate
1.27 +encoding by inspecting the formula at hand. This behavior can be overridden by
1.28 +passing either \textit{unary\_ints} or \textit{binary\_ints} as option. For
1.29 +binary notation, the number of bits to use can be specified using
1.30 +the \textit{bits} option. For example:
1.31 +
1.32 +\prew
1.33 +\textbf{nitpick} [\textit{binary\_ints}, \textit{bits}${} = 16$]
1.34 +\postw
1.35 +
1.36 With infinite types, we don't always have the luxury of a genuine counterexample
1.37 and must often content ourselves with a potential one. The tedious task of
1.38 finding out whether the potential counterexample is in fact genuine can be
1.39 -outsourced to \textit{auto} by passing the option \textit{check\_potential}. For
1.40 -example:
1.41 +outsourced to \textit{auto} by passing \textit{check\_potential}. For example:
1.42
1.43 \prew
1.44 \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
1.45 -\textbf{nitpick} [\textit{card~nat}~= 100,\, \textit{check\_potential}] \\[2\smallskipamount]
1.46 +\textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount]
1.47 \slshape Nitpick found a potential counterexample: \\[2\smallskipamount]
1.48 \hbox{}\qquad Free variable: \nopagebreak \\
1.49 \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
1.50 @@ -482,7 +491,7 @@
1.51
1.52 Incidentally, if you distrust the so-called genuine counterexamples, you can
1.53 enable \textit{check\_\allowbreak genuine} to verify them as well. However, be
1.54 -aware that \textit{auto} will often fail to prove that the counterexample is
1.55 +aware that \textit{auto} will usually fail to prove that the counterexample is
1.56 genuine or spurious.
1.57
1.58 Some conjectures involving elementary number theory make Nitpick look like a
1.59 @@ -495,10 +504,11 @@
1.60 Nitpick found no counterexample.
1.61 \postw
1.62
1.63 -For any cardinality $k$, \textit{Suc} is the partial function $\{0 \mapsto 1,\,
1.64 -1 \mapsto 2,\, \ldots,\, k - 1 \mapsto \unk\}$, which evaluates to $\unk$ when
1.65 -it is passed as argument to $P$. As a result, $P~\textit{Suc}$ is always $\unk$.
1.66 -The next example is similar:
1.67 +On any finite set $N$, \textit{Suc} is a partial function; for example, if $N =
1.68 +\{0, 1, \ldots, k\}$, then \textit{Suc} is $\{0 \mapsto 1,\, 1 \mapsto 2,\,
1.69 +\ldots,\, k \mapsto \unk\}$, which evaluates to $\unk$ when passed as
1.70 +argument to $P$. As a result, $P~\textit{Suc}$ is always $\unk$. The next
1.71 +example is similar:
1.72
1.73 \prew
1.74 \textbf{lemma} ``$P~(\textit{op}~{+}\Colon
1.75 @@ -822,7 +832,7 @@
1.76
1.77 \prew
1.78 \textbf{lemma} ``$\textit{even}'~(n - 2) \,\Longrightarrow\, \textit{even}'~n$'' \\
1.79 -\textbf{nitpick} [\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
1.80 +\textbf{nitpick} [\textit{card nat} = 10, \textit{show\_consts}] \\[2\smallskipamount]
1.81 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.82 \hbox{}\qquad Free variable: \nopagebreak \\
1.83 \hbox{}\qquad\qquad $n = 1$ \\
1.84 @@ -989,7 +999,7 @@
1.85 \prew
1.86 \textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk
1.87 \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
1.88 -\textbf{nitpick} [\textit{bisim\_depth} = $-1$,\, \textit{show\_datatypes}] \\[2\smallskipamount]
1.89 +\textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount]
1.90 \slshape Nitpick found a likely genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
1.91 \hbox{}\qquad Free variables: \nopagebreak \\
1.92 \hbox{}\qquad\qquad $a = a_2$ \\
1.93 @@ -1687,9 +1697,38 @@
1.94
1.95 \begin{enum}
1.96 \opu{card}{type}{int\_seq}
1.97 -Specifies the sequence of cardinalities to use for a given type. For
1.98 -\textit{nat} and \textit{int}, the cardinality fully specifies the subset used
1.99 -to approximate the type. For example:
1.100 +Specifies the sequence of cardinalities to use for a given type.
1.101 +For free types, and often also for \textbf{typedecl}'d types, it usually makes
1.102 +sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
1.103 +Although function and product types are normally mapped directly to the
1.104 +corresponding Kodkod concepts, setting
1.105 +the cardinality of such types is also allowed and implicitly enables ``boxing''
1.106 +for them, as explained in the description of the \textit{box}~\qty{type}
1.107 +and \textit{box} (\S\ref{scope-of-search}) options.
1.108 +
1.109 +\nopagebreak
1.110 +{\small See also \textit{mono} (\S\ref{scope-of-search}).}
1.111 +
1.112 +\opt{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
1.113 +Specifies the default sequence of cardinalities to use. This can be overridden
1.114 +on a per-type basis using the \textit{card}~\qty{type} option described above.
1.115 +
1.116 +\opu{max}{const}{int\_seq}
1.117 +Specifies the sequence of maximum multiplicities to use for a given
1.118 +(co)in\-duc\-tive datatype constructor. A constructor's multiplicity is the
1.119 +number of distinct values that it can construct. Nonsensical values (e.g.,
1.120 +\textit{max}~[]~$=$~2) are silently repaired. This option is only available for
1.121 +datatypes equipped with several constructors.
1.122 +
1.123 +\ops{max}{int\_seq}
1.124 +Specifies the default sequence of maximum multiplicities to use for
1.125 +(co)in\-duc\-tive datatype constructors. This can be overridden on a per-constructor
1.126 +basis using the \textit{max}~\qty{const} option described above.
1.127 +
1.128 +\opsmart{binary\_ints}{unary\_ints}
1.129 +Specifies whether natural numbers and integers should be encoded using a unary
1.130 +or binary notation. In unary mode, the cardinality fully specifies the subset
1.131 +used to approximate the type. For example:
1.132 %
1.133 $$\hbox{\begin{tabular}{@{}rll@{}}%
1.134 \textit{card nat} = 4 & induces & $\{0,\, 1,\, 2,\, 3\}$ \\
1.135 @@ -1704,32 +1743,25 @@
1.136 \textit{card int} = $K$ & induces & $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor K/2 \rfloor\}.$%
1.137 \end{tabular}}$$
1.138 %
1.139 -For free types, and often also for \textbf{typedecl}'d types, it usually makes
1.140 -sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
1.141 -Although function and product types are normally mapped directly to the
1.142 -corresponding Kodkod concepts, setting
1.143 -the cardinality of such types is also allowed and implicitly enables ``boxing''
1.144 -for them, as explained in the description of the \textit{box}~\qty{type}
1.145 -and \textit{box} (\S\ref{scope-of-search}) options.
1.146 -
1.147 -\nopagebreak
1.148 -{\small See also \textit{mono} (\S\ref{scope-of-search}).}
1.149 -
1.150 -\opt{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
1.151 -Specifies the default sequence of cardinalities to use. This can be overridden
1.152 -on a per-type basis using the \textit{card}~\qty{type} option described above.
1.153 -
1.154 -\opu{max}{const}{int\_seq}
1.155 -Specifies the sequence of maximum multiplicities to use for a given
1.156 -(co)in\-duc\-tive datatype constructor. A constructor's multiplicity is the
1.157 -number of distinct values that it can construct. Nonsensical values (e.g.,
1.158 -\textit{max}~[]~$=$~2) are silently repaired. This option is only available for
1.159 -datatypes equipped with several constructors.
1.160 -
1.161 -\ops{max}{int\_seq}
1.162 -Specifies the default sequence of maximum multiplicities to use for
1.163 -(co)in\-duc\-tive datatype constructors. This can be overridden on a per-constructor
1.164 -basis using the \textit{max}~\qty{const} option described above.
1.165 +In binary mode, the cardinality specifies the number of distinct values that can
1.166 +be constructed. Each of these value is represented by a bit pattern whose length
1.167 +is specified by the \textit{bits} (\S\ref{scope-of-search}) option. By default,
1.168 +Nitpick attempts to choose the more appropriate encoding by inspecting the
1.169 +formula at hand, preferring the binary notation for problems involving
1.170 +multiplicative operators or large constants.
1.171 +
1.172 +\textbf{Warning:} For technical reasons, Nitpick always reverts to unary for
1.173 +problems that refer to the types \textit{rat} or \textit{real} or the constants
1.174 +\textit{gcd} or \textit{lcm}.
1.175 +
1.176 +{\small See also \textit{bits} (\S\ref{scope-of-search}) and
1.177 +\textit{show\_datatypes} (\S\ref{output-format}).}
1.178 +
1.179 +\opt{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12}$}
1.180 +Specifies the number of bits to use to represent natural numbers and integers in
1.181 +binary, excluding the sign bit. The minimum is 1 and the maximum is 31.
1.182 +
1.183 +{\small See also \textit{binary\_ints} (\S\ref{scope-of-search}).}
1.184
1.185 \opusmart{wf}{const}{non\_wf}
1.186 Specifies whether the specified (co)in\-duc\-tively defined predicate is