1.1 --- a/doc-src/Nitpick/nitpick.tex Tue Feb 09 16:05:49 2010 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Tue Feb 09 16:07:51 2010 +0100
1.3 @@ -154,7 +154,7 @@
1.4 the line
1.5
1.6 \prew
1.7 -\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSatJNI}, \,\textit{max\_threads}~= 1]
1.8 +\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1]
1.9 \postw
1.10
1.11 after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
1.12 @@ -311,9 +311,9 @@
1.13 \slshape Constant: \nopagebreak \\
1.14 \hbox{}\qquad $\mathit{The} = \undef{}
1.15 (\!\begin{aligned}[t]%
1.16 - & \{\} := a_3,\> \{a_3\} := a_3,\> \{a_2\} := a_2, \\[-2pt] %% TYPESETTING
1.17 - & \{a_2, a_3\} := a_1,\> \{a_1\} := a_1,\> \{a_1, a_3\} := a_3, \\[-2pt]
1.18 - & \{a_1, a_2\} := a_3,\> \{a_1, a_2, a_3\} := a_3)\end{aligned}$
1.19 + & \{a_1, a_2, a_3\} := a_3,\> \{a_1, a_2\} := a_3,\> \{a_1, a_3\} := a_3, \\[-2pt] %% TYPESETTING
1.20 + & \{a_1\} := a_1,\> \{a_2, a_3\} := a_1,\> \{a_2\} := a_2, \\[-2pt]
1.21 + & \{a_3\} := a_3,\> \{\} := a_3)\end{aligned}$
1.22 \postw
1.23
1.24 Notice that $\textit{The}~(\lambda y.\;P~y) = \textit{The}~\{a_2, a_3\} = a_1$,
1.25 @@ -550,7 +550,7 @@
1.26 \slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
1.27 \hbox{}\qquad Free variables: \nopagebreak \\
1.28 \hbox{}\qquad\qquad $\textit{xs} = []$ \\
1.29 -\hbox{}\qquad\qquad $\textit{y} = a_3$
1.30 +\hbox{}\qquad\qquad $\textit{y} = a_1$
1.31 \postw
1.32
1.33 To see why the counterexample is genuine, we enable \textit{show\_consts}
1.34 @@ -558,21 +558,21 @@
1.35
1.36 \prew
1.37 {\slshape Datatype:} \\
1.38 -\hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_3, a_3],\, [a_3],\, \unr\}$ \\
1.39 +\hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_1],\, [a_1, a_1],\, \unr\}$ \\
1.40 {\slshape Constants:} \\
1.41 -\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_3, a_3])$ \\
1.42 -\hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_3, a_3] := a_3,\> [a_3] := a_3)$
1.43 +\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_1, a_1])$ \\
1.44 +\hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_1] := a_1,\> [a_1, a_1] := a_1)$
1.45 \postw
1.46
1.47 Since $\mathit{hd}~[]$ is undefined in the logic, it may be given any value,
1.48 including $a_2$.
1.49
1.50 The second constant, $\lambda x_1.\; x_1 \mathbin{@} [y, y]$, is simply the
1.51 -append operator whose second argument is fixed to be $[y, y]$. Appending $[a_3,
1.52 -a_3]$ to $[a_3]$ would normally give $[a_3, a_3, a_3]$, but this value is not
1.53 +append operator whose second argument is fixed to be $[y, y]$. Appending $[a_1,
1.54 +a_1]$ to $[a_1]$ would normally give $[a_1, a_1, a_1]$, but this value is not
1.55 representable in the subset of $'a$~\textit{list} considered by Nitpick, which
1.56 is shown under the ``Datatype'' heading; hence the result is $\unk$. Similarly,
1.57 -appending $[a_3, a_3]$ to itself gives $\unk$.
1.58 +appending $[a_1, a_1]$ to itself gives $\unk$.
1.59
1.60 Given \textit{card}~$'a = 3$ and \textit{card}~$'a~\textit{list} = 3$, Nitpick
1.61 considers the following subsets:
1.62 @@ -600,8 +600,8 @@
1.63
1.64 All subterm-closed subsets of $'a~\textit{list}$ consisting of three values
1.65 are listed and only those. As an example of a non-subterm-closed subset,
1.66 -consider $\mathcal{S} = \{[],\, [a_1],\,\allowbreak [a_1, a_3]\}$, and observe
1.67 -that $[a_1, a_3]$ (i.e., $a_1 \mathbin{\#} [a_3]$) has $[a_3] \notin
1.68 +consider $\mathcal{S} = \{[],\, [a_1],\,\allowbreak [a_1, a_2]\}$, and observe
1.69 +that $[a_1, a_2]$ (i.e., $a_1 \mathbin{\#} [a_2]$) has $[a_2] \notin
1.70 \mathcal{S}$ as a subterm.
1.71
1.72 Here's another m\"ochtegern-lemma that Nitpick can refute without a blink:
1.73 @@ -613,11 +613,11 @@
1.74 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
1.75 \slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
1.76 \hbox{}\qquad Free variables: \nopagebreak \\
1.77 -\hbox{}\qquad\qquad $\textit{xs} = [a_2]$ \\
1.78 -\hbox{}\qquad\qquad $\textit{ys} = [a_3]$ \\
1.79 +\hbox{}\qquad\qquad $\textit{xs} = [a_1]$ \\
1.80 +\hbox{}\qquad\qquad $\textit{ys} = [a_2]$ \\
1.81 \hbox{}\qquad Datatypes: \\
1.82 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
1.83 -\hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_3],\, [a_2],\, \unr\}$
1.84 +\hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_1],\, [a_2],\, \unr\}$
1.85 \postw
1.86
1.87 Because datatypes are approximated using a three-valued logic, there is usually
1.88 @@ -642,11 +642,11 @@
1.89 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
1.90 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.91 \hbox{}\qquad Free variables: \nopagebreak \\
1.92 -\hbox{}\qquad\qquad $P = \{\Abs{1},\, \Abs{0}\}$ \\
1.93 +\hbox{}\qquad\qquad $P = \{\Abs{0},\, \Abs{1}\}$ \\
1.94 \hbox{}\qquad\qquad $x = \Abs{2}$ \\
1.95 \hbox{}\qquad Datatypes: \\
1.96 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
1.97 -\hbox{}\qquad\qquad $\textit{three} = \{\Abs{2},\, \Abs{1},\, \Abs{0},\, \unr\}$
1.98 +\hbox{}\qquad\qquad $\textit{three} = \{\Abs{0},\, \Abs{1},\, \Abs{2},\, \unr\}$
1.99 \postw
1.100
1.101 %% MARK
1.102 @@ -664,12 +664,13 @@
1.103 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
1.104 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.105 \hbox{}\qquad Free variables: \nopagebreak \\
1.106 -\hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\
1.107 -\hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
1.108 +\hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
1.109 +\hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\
1.110 \hbox{}\qquad Datatypes: \\
1.111 \hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, \unr\}$ \\
1.112 -\hbox{}\qquad\qquad $\textit{point} = \{\lparr\textit{Xcoord} = 1,\>
1.113 -\textit{Ycoord} = 1\rparr,\> \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr,\, \unr\}$\kern-1pt %% QUIET
1.114 +\hbox{}\qquad\qquad $\textit{point} = \{\!\begin{aligned}[t]
1.115 +& \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr, \\[-2pt] %% TYPESETTING
1.116 +& \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$
1.117 \postw
1.118
1.119 Finally, Nitpick provides rudimentary support for rationals and reals using a
1.120 @@ -956,16 +957,16 @@
1.121 depth}~= 1:
1.122 \\[2\smallskipamount]
1.123 \hbox{}\qquad Free variables: \nopagebreak \\
1.124 -\hbox{}\qquad\qquad $\textit{a} = a_2$ \\
1.125 -\hbox{}\qquad\qquad $\textit{b} = a_1$ \\
1.126 -\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega$ \\
1.127 -\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_1~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega)$ \\[2\smallskipamount]
1.128 +\hbox{}\qquad\qquad $\textit{a} = a_1$ \\
1.129 +\hbox{}\qquad\qquad $\textit{b} = a_2$ \\
1.130 +\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
1.131 +\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_2~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega)$ \\[2\smallskipamount]
1.132 Total time: 726 ms.
1.133 \postw
1.134
1.135 -The lazy list $\textit{xs}$ is simply $[a_2, a_2, a_2, \ldots]$, whereas
1.136 -$\textit{ys}$ is $[a_1, a_2, a_2, a_2, \ldots]$, i.e., a lasso-shaped list with
1.137 -$[a_1]$ as its stem and $[a_2]$ as its cycle. In general, the list segment
1.138 +The lazy list $\textit{xs}$ is simply $[a_1, a_1, a_1, \ldots]$, whereas
1.139 +$\textit{ys}$ is $[a_2, a_1, a_1, a_1, \ldots]$, i.e., a lasso-shaped list with
1.140 +$[a_2]$ as its stem and $[a_1]$ as its cycle. In general, the list segment
1.141 within the scope of the {THE} binder corresponds to the lasso's cycle, whereas
1.142 the segment leading to the binder is the stem.
1.143
1.144 @@ -1000,15 +1001,15 @@
1.145 \textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount]
1.146 \slshape Nitpick found a likely genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
1.147 \hbox{}\qquad Free variables: \nopagebreak \\
1.148 -\hbox{}\qquad\qquad $a = a_2$ \\
1.149 +\hbox{}\qquad\qquad $a = a_1$ \\
1.150 \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega =
1.151 -\textit{LCons}~a_2~\omega$ \\
1.152 -\hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega$ \\
1.153 +\textit{LCons}~a_1~\omega$ \\
1.154 +\hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
1.155 \hbox{}\qquad Codatatype:\strut \nopagebreak \\
1.156 \hbox{}\qquad\qquad $'a~\textit{llist} =
1.157 \{\!\begin{aligned}[t]
1.158 - & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega, \\[-2pt]
1.159 - & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega,\> \unr\}\end{aligned}$
1.160 + & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega, \\[-2pt]
1.161 + & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega,\> \unr\}\end{aligned}$
1.162 \\[2\smallskipamount]
1.163 Try again with ``\textit{bisim\_depth}'' set to a nonnegative value to confirm
1.164 that the counterexample is genuine. \\[2\smallskipamount]
1.165 @@ -1198,8 +1199,8 @@
1.166 \textit{card} ``\kern1pt$'b$ \textit{list}''~= 5:
1.167 \\[2\smallskipamount]
1.168 \hbox{}\qquad Free variables: \nopagebreak \\
1.169 -\hbox{}\qquad\qquad $\textit{xs} = [a_4, a_5]$ \\
1.170 -\hbox{}\qquad\qquad $\textit{ys} = [b_3, b_3]$ \\[2\smallskipamount]
1.171 +\hbox{}\qquad\qquad $\textit{xs} = [a_1, a_2]$ \\
1.172 +\hbox{}\qquad\qquad $\textit{ys} = [b_1, b_1]$ \\[2\smallskipamount]
1.173 Total time: 1636 ms.
1.174 \postw
1.175
1.176 @@ -1377,21 +1378,21 @@
1.177 \prew
1.178 \slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
1.179 \hbox{}\qquad Free variables: \nopagebreak \\
1.180 -\hbox{}\qquad\qquad $a = a_4$ \\
1.181 -\hbox{}\qquad\qquad $b = a_3$ \\
1.182 -\hbox{}\qquad\qquad $t = \xi_3$ \\
1.183 -\hbox{}\qquad\qquad $u = \xi_4$ \\
1.184 +\hbox{}\qquad\qquad $a = a_1$ \\
1.185 +\hbox{}\qquad\qquad $b = a_2$ \\
1.186 +\hbox{}\qquad\qquad $t = \xi_1$ \\
1.187 +\hbox{}\qquad\qquad $u = \xi_2$ \\
1.188 \hbox{}\qquad {\slshape Constants:} \nopagebreak \\
1.189 \hbox{}\qquad\qquad $\textit{labels} = \undef
1.190 (\!\begin{aligned}[t]%
1.191 - & \xi_3 := \{a_4\},\> \xi_4 := \{a_1, a_3\}, \\[-2pt] %% TYPESETTING
1.192 - & \textit{Branch}~\xi_3~\xi_3 := \{a_4\}, \\[-2pt]
1.193 - & \textit{Branch}~\xi_3~\xi_4 := \{a_1, a_3, a_4\})\end{aligned}$ \\
1.194 + & \xi_1 := \{a_1, a_4, a_3^\Q\},\> \xi_2 := \{a_2, a_3^\Q\}, \\[-2pt] %% TYPESETTING
1.195 + & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_4, a_3^\Q\}, \\[-2pt]
1.196 + & \textit{Branch}~\xi_2~\xi_2 := \{a_2, a_3^\Q\})\end{aligned}$ \\
1.197 \hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef
1.198 (\!\begin{aligned}[t]%
1.199 - & \xi_3 := \xi_3,\> \xi_4 := \xi_3, \\[-2pt]
1.200 - & \textit{Branch}~\xi_3~\xi_3 := \textit{Branch}~\xi_3~\xi_3, \\[-2pt]
1.201 - & \textit{Branch}~\xi_4~\xi_3 := \textit{Branch}~\xi_3~\xi_3)\end{aligned}$ \\[2\smallskipamount]
1.202 + & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
1.203 + & \textit{Branch}~\xi_1~\xi_2 := \textit{Branch}~\xi_2~\xi_2, \\[-2pt]
1.204 + & \textit{Branch}~\xi_2~\xi_2 := \textit{Branch}~\xi_2~\xi_2)\end{aligned}$ \\[2\smallskipamount]
1.205 The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps
1.206 even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
1.207 \postw
1.208 @@ -1406,7 +1407,7 @@
1.209 allowing unreachable states in the preceding example (by removing the ``$n \in
1.210 \textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
1.211 set of objects over which the induction is performed while doing the step
1.212 -so as to test the induction hypothesis's strength.}
1.213 +in order to test the induction hypothesis's strength.}
1.214 The new trees are so nonstandard that we know nothing about them, except what
1.215 the induction hypothesis states and what can be proved about all trees without
1.216 relying on induction or case distinction. The key observation is,
1.217 @@ -1417,8 +1418,8 @@
1.218 objects, and Nitpick won't find any nonstandard counterexample.}
1.219 \end{quote}
1.220 %
1.221 -But here, Nitpick did find some nonstandard trees $t = \xi_3$
1.222 -and $u = \xi_4$ such that $a \in \textit{labels}~t$, $b \notin
1.223 +But here, Nitpick did find some nonstandard trees $t = \xi_1$
1.224 +and $u = \xi_2$ such that $a \in \textit{labels}~t$, $b \notin
1.225 \textit{labels}~t$, $a \notin \textit{labels}~u$, and $b \in \textit{labels}~u$.
1.226 Because neither tree contains both $a$ and $b$, the induction hypothesis tells
1.227 us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$,
1.228 @@ -1441,7 +1442,7 @@
1.229 \postw
1.230
1.231 This time, Nitpick won't find any nonstandard counterexample, and we can perform
1.232 -the induction step using \textbf{auto}.
1.233 +the induction step using \textit{auto}.
1.234
1.235 \section{Case Studies}
1.236 \label{case-studies}
1.237 @@ -1726,8 +1727,8 @@
1.238 \textbf{nitpick} \\[2\smallskipamount]
1.239 \slshape Nitpick found a counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
1.240 \hbox{}\qquad Free variables: \nopagebreak \\
1.241 -\hbox{}\qquad\qquad $t = N~a_3~1~\Lambda~\Lambda$ \\
1.242 -\hbox{}\qquad\qquad $x = a_4$
1.243 +\hbox{}\qquad\qquad $t = N~a_1~1~\Lambda~\Lambda$ \\
1.244 +\hbox{}\qquad\qquad $x = a_2$
1.245 \postw
1.246
1.247 It's hard to see why this is a counterexample. To improve readability, we will
1.248 @@ -2138,7 +2139,7 @@
1.249 is implicitly set to 0 for automatic runs. If you set this option to a value
1.250 greater than 1, you will need an incremental SAT solver: For efficiency, it is
1.251 recommended to install the JNI version of MiniSat and set \textit{sat\_solver} =
1.252 -\textit{MiniSatJNI}. Also be aware that many of the counterexamples may look
1.253 +\textit{MiniSat\_JNI}. Also be aware that many of the counterexamples may look
1.254 identical, unless the \textit{show\_all} (\S\ref{output-format}) option is
1.255 enabled.
1.256
1.257 @@ -2150,7 +2151,7 @@
1.258 Specifies the maximum number of genuine counterexamples to display. If you set
1.259 this option to a value greater than 1, you will need an incremental SAT solver:
1.260 For efficiency, it is recommended to install the JNI version of MiniSat and set
1.261 -\textit{sat\_solver} = \textit{MiniSatJNI}. Also be aware that many of the
1.262 +\textit{sat\_solver} = \textit{MiniSat\_JNI}. Also be aware that many of the
1.263 counterexamples may look identical, unless the \textit{show\_all}
1.264 (\S\ref{output-format}) option is enabled.
1.265
1.266 @@ -2243,7 +2244,7 @@
1.267 to be faster than their Java counterparts, but they can be more difficult to
1.268 install. Also, if you set the \textit{max\_potential} (\S\ref{output-format}) or
1.269 \textit{max\_genuine} (\S\ref{output-format}) option to a value greater than 1,
1.270 -you will need an incremental SAT solver, such as \textit{MiniSatJNI}
1.271 +you will need an incremental SAT solver, such as \textit{MiniSat\_JNI}
1.272 (recommended) or \textit{SAT4J}.
1.273
1.274 The supported solvers are listed below:
1.275 @@ -2257,7 +2258,7 @@
1.276 \url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
1.277 and 2.0 beta (2007-07-21).
1.278
1.279 -\item[$\bullet$] \textbf{\textit{MiniSatJNI}}: The JNI (Java Native Interface)
1.280 +\item[$\bullet$] \textbf{\textit{MiniSat\_JNI}}: The JNI (Java Native Interface)
1.281 version of MiniSat is bundled in \texttt{nativesolver.\allowbreak tgz}, which
1.282 you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
1.283 version of MiniSat, the JNI version can be used incrementally.
1.284 @@ -2279,7 +2280,7 @@
1.285 \url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
1.286 versions 2004-05-13, 2004-11-15, and 2007-03-12.
1.287
1.288 -\item[$\bullet$] \textbf{\textit{zChaffJNI}}: The JNI version of zChaff is
1.289 +\item[$\bullet$] \textbf{\textit{zChaff\_JNI}}: The JNI version of zChaff is
1.290 bundled in \texttt{native\-solver.\allowbreak tgz}, which you will find on
1.291 Kodkod's web site \cite{kodkod-2009}.
1.292
1.293 @@ -2295,7 +2296,7 @@
1.294 executable. The BerkMin executables are available at
1.295 \url{http://eigold.tripod.com/BerkMin.html}.
1.296
1.297 -\item[$\bullet$] \textbf{\textit{BerkMinAlloy}}: Variant of BerkMin that is
1.298 +\item[$\bullet$] \textbf{\textit{BerkMin\_Alloy}}: Variant of BerkMin that is
1.299 included with Alloy 4 and calls itself ``sat56'' in its banner text. To use this
1.300 version of BerkMin, set the environment variable
1.301 \texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin}
1.302 @@ -2313,7 +2314,7 @@
1.303 install the official SAT4J packages, because their API is incompatible with
1.304 Kodkod.
1.305
1.306 -\item[$\bullet$] \textbf{\textit{SAT4JLight}}: Variant of SAT4J that is
1.307 +\item[$\bullet$] \textbf{\textit{SAT4J\_Light}}: Variant of SAT4J that is
1.308 optimized for small problems. It can also be used incrementally.
1.309
1.310 \item[$\bullet$] \textbf{\textit{HaifaSat}}: HaifaSat 1.0 beta is an
1.311 @@ -2324,7 +2325,7 @@
1.312
1.313 \item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to
1.314 \textit{smart}, Nitpick selects the first solver among MiniSat,
1.315 -PicoSAT, zChaff, RSat, BerkMin, BerkMinAlloy, Jerusat, MiniSatJNI, and zChaffJNI
1.316 +PicoSAT, zChaff, RSat, BerkMin, BerkMin\_Alloy, Jerusat, MiniSat\_JNI, and zChaff\_JNI
1.317 that is recognized by Isabelle. If none is found, it falls back on SAT4J, which
1.318 should always be available. If \textit{verbose} (\S\ref{output-format}) is
1.319 enabled, Nitpick displays which SAT solver was chosen.