optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
--- a/doc-src/Nitpick/nitpick.tex Tue Feb 09 16:05:49 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Tue Feb 09 16:07:51 2010 +0100
@@ -154,7 +154,7 @@
the line
\prew
-\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSatJNI}, \,\textit{max\_threads}~= 1]
+\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1]
\postw
after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
@@ -311,9 +311,9 @@
\slshape Constant: \nopagebreak \\
\hbox{}\qquad $\mathit{The} = \undef{}
(\!\begin{aligned}[t]%
- & \{\} := a_3,\> \{a_3\} := a_3,\> \{a_2\} := a_2, \\[-2pt] %% TYPESETTING
- & \{a_2, a_3\} := a_1,\> \{a_1\} := a_1,\> \{a_1, a_3\} := a_3, \\[-2pt]
- & \{a_1, a_2\} := a_3,\> \{a_1, a_2, a_3\} := a_3)\end{aligned}$
+ & \{a_1, a_2, a_3\} := a_3,\> \{a_1, a_2\} := a_3,\> \{a_1, a_3\} := a_3, \\[-2pt] %% TYPESETTING
+ & \{a_1\} := a_1,\> \{a_2, a_3\} := a_1,\> \{a_2\} := a_2, \\[-2pt]
+ & \{a_3\} := a_3,\> \{\} := a_3)\end{aligned}$
\postw
Notice that $\textit{The}~(\lambda y.\;P~y) = \textit{The}~\{a_2, a_3\} = a_1$,
@@ -550,7 +550,7 @@
\slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $\textit{xs} = []$ \\
-\hbox{}\qquad\qquad $\textit{y} = a_3$
+\hbox{}\qquad\qquad $\textit{y} = a_1$
\postw
To see why the counterexample is genuine, we enable \textit{show\_consts}
@@ -558,21 +558,21 @@
\prew
{\slshape Datatype:} \\
-\hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_3, a_3],\, [a_3],\, \unr\}$ \\
+\hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_1],\, [a_1, a_1],\, \unr\}$ \\
{\slshape Constants:} \\
-\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_3, a_3])$ \\
-\hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_3, a_3] := a_3,\> [a_3] := a_3)$
+\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_1, a_1])$ \\
+\hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_1] := a_1,\> [a_1, a_1] := a_1)$
\postw
Since $\mathit{hd}~[]$ is undefined in the logic, it may be given any value,
including $a_2$.
The second constant, $\lambda x_1.\; x_1 \mathbin{@} [y, y]$, is simply the
-append operator whose second argument is fixed to be $[y, y]$. Appending $[a_3,
-a_3]$ to $[a_3]$ would normally give $[a_3, a_3, a_3]$, but this value is not
+append operator whose second argument is fixed to be $[y, y]$. Appending $[a_1,
+a_1]$ to $[a_1]$ would normally give $[a_1, a_1, a_1]$, but this value is not
representable in the subset of $'a$~\textit{list} considered by Nitpick, which
is shown under the ``Datatype'' heading; hence the result is $\unk$. Similarly,
-appending $[a_3, a_3]$ to itself gives $\unk$.
+appending $[a_1, a_1]$ to itself gives $\unk$.
Given \textit{card}~$'a = 3$ and \textit{card}~$'a~\textit{list} = 3$, Nitpick
considers the following subsets:
@@ -600,8 +600,8 @@
All subterm-closed subsets of $'a~\textit{list}$ consisting of three values
are listed and only those. As an example of a non-subterm-closed subset,
-consider $\mathcal{S} = \{[],\, [a_1],\,\allowbreak [a_1, a_3]\}$, and observe
-that $[a_1, a_3]$ (i.e., $a_1 \mathbin{\#} [a_3]$) has $[a_3] \notin
+consider $\mathcal{S} = \{[],\, [a_1],\,\allowbreak [a_1, a_2]\}$, and observe
+that $[a_1, a_2]$ (i.e., $a_1 \mathbin{\#} [a_2]$) has $[a_2] \notin
\mathcal{S}$ as a subterm.
Here's another m\"ochtegern-lemma that Nitpick can refute without a blink:
@@ -613,11 +613,11 @@
\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
-\hbox{}\qquad\qquad $\textit{xs} = [a_2]$ \\
-\hbox{}\qquad\qquad $\textit{ys} = [a_3]$ \\
+\hbox{}\qquad\qquad $\textit{xs} = [a_1]$ \\
+\hbox{}\qquad\qquad $\textit{ys} = [a_2]$ \\
\hbox{}\qquad Datatypes: \\
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
-\hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_3],\, [a_2],\, \unr\}$
+\hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_1],\, [a_2],\, \unr\}$
\postw
Because datatypes are approximated using a three-valued logic, there is usually
@@ -642,11 +642,11 @@
\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
-\hbox{}\qquad\qquad $P = \{\Abs{1},\, \Abs{0}\}$ \\
+\hbox{}\qquad\qquad $P = \{\Abs{0},\, \Abs{1}\}$ \\
\hbox{}\qquad\qquad $x = \Abs{2}$ \\
\hbox{}\qquad Datatypes: \\
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
-\hbox{}\qquad\qquad $\textit{three} = \{\Abs{2},\, \Abs{1},\, \Abs{0},\, \unr\}$
+\hbox{}\qquad\qquad $\textit{three} = \{\Abs{0},\, \Abs{1},\, \Abs{2},\, \unr\}$
\postw
%% MARK
@@ -664,12 +664,13 @@
\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
-\hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\
-\hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
+\hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
+\hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\
\hbox{}\qquad Datatypes: \\
\hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, \unr\}$ \\
-\hbox{}\qquad\qquad $\textit{point} = \{\lparr\textit{Xcoord} = 1,\>
-\textit{Ycoord} = 1\rparr,\> \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr,\, \unr\}$\kern-1pt %% QUIET
+\hbox{}\qquad\qquad $\textit{point} = \{\!\begin{aligned}[t]
+& \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr, \\[-2pt] %% TYPESETTING
+& \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$
\postw
Finally, Nitpick provides rudimentary support for rationals and reals using a
@@ -956,16 +957,16 @@
depth}~= 1:
\\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
-\hbox{}\qquad\qquad $\textit{a} = a_2$ \\
-\hbox{}\qquad\qquad $\textit{b} = a_1$ \\
-\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega$ \\
-\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_1~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega)$ \\[2\smallskipamount]
+\hbox{}\qquad\qquad $\textit{a} = a_1$ \\
+\hbox{}\qquad\qquad $\textit{b} = a_2$ \\
+\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
+\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_2~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega)$ \\[2\smallskipamount]
Total time: 726 ms.
\postw
-The lazy list $\textit{xs}$ is simply $[a_2, a_2, a_2, \ldots]$, whereas
-$\textit{ys}$ is $[a_1, a_2, a_2, a_2, \ldots]$, i.e., a lasso-shaped list with
-$[a_1]$ as its stem and $[a_2]$ as its cycle. In general, the list segment
+The lazy list $\textit{xs}$ is simply $[a_1, a_1, a_1, \ldots]$, whereas
+$\textit{ys}$ is $[a_2, a_1, a_1, a_1, \ldots]$, i.e., a lasso-shaped list with
+$[a_2]$ as its stem and $[a_1]$ as its cycle. In general, the list segment
within the scope of the {THE} binder corresponds to the lasso's cycle, whereas
the segment leading to the binder is the stem.
@@ -1000,15 +1001,15 @@
\textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount]
\slshape Nitpick found a likely genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
-\hbox{}\qquad\qquad $a = a_2$ \\
+\hbox{}\qquad\qquad $a = a_1$ \\
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega =
-\textit{LCons}~a_2~\omega$ \\
-\hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega$ \\
+\textit{LCons}~a_1~\omega$ \\
+\hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
\hbox{}\qquad Codatatype:\strut \nopagebreak \\
\hbox{}\qquad\qquad $'a~\textit{llist} =
\{\!\begin{aligned}[t]
- & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega, \\[-2pt]
- & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega,\> \unr\}\end{aligned}$
+ & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega, \\[-2pt]
+ & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega,\> \unr\}\end{aligned}$
\\[2\smallskipamount]
Try again with ``\textit{bisim\_depth}'' set to a nonnegative value to confirm
that the counterexample is genuine. \\[2\smallskipamount]
@@ -1198,8 +1199,8 @@
\textit{card} ``\kern1pt$'b$ \textit{list}''~= 5:
\\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
-\hbox{}\qquad\qquad $\textit{xs} = [a_4, a_5]$ \\
-\hbox{}\qquad\qquad $\textit{ys} = [b_3, b_3]$ \\[2\smallskipamount]
+\hbox{}\qquad\qquad $\textit{xs} = [a_1, a_2]$ \\
+\hbox{}\qquad\qquad $\textit{ys} = [b_1, b_1]$ \\[2\smallskipamount]
Total time: 1636 ms.
\postw
@@ -1377,21 +1378,21 @@
\prew
\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
-\hbox{}\qquad\qquad $a = a_4$ \\
-\hbox{}\qquad\qquad $b = a_3$ \\
-\hbox{}\qquad\qquad $t = \xi_3$ \\
-\hbox{}\qquad\qquad $u = \xi_4$ \\
+\hbox{}\qquad\qquad $a = a_1$ \\
+\hbox{}\qquad\qquad $b = a_2$ \\
+\hbox{}\qquad\qquad $t = \xi_1$ \\
+\hbox{}\qquad\qquad $u = \xi_2$ \\
\hbox{}\qquad {\slshape Constants:} \nopagebreak \\
\hbox{}\qquad\qquad $\textit{labels} = \undef
(\!\begin{aligned}[t]%
- & \xi_3 := \{a_4\},\> \xi_4 := \{a_1, a_3\}, \\[-2pt] %% TYPESETTING
- & \textit{Branch}~\xi_3~\xi_3 := \{a_4\}, \\[-2pt]
- & \textit{Branch}~\xi_3~\xi_4 := \{a_1, a_3, a_4\})\end{aligned}$ \\
+ & \xi_1 := \{a_1, a_4, a_3^\Q\},\> \xi_2 := \{a_2, a_3^\Q\}, \\[-2pt] %% TYPESETTING
+ & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_4, a_3^\Q\}, \\[-2pt]
+ & \textit{Branch}~\xi_2~\xi_2 := \{a_2, a_3^\Q\})\end{aligned}$ \\
\hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef
(\!\begin{aligned}[t]%
- & \xi_3 := \xi_3,\> \xi_4 := \xi_3, \\[-2pt]
- & \textit{Branch}~\xi_3~\xi_3 := \textit{Branch}~\xi_3~\xi_3, \\[-2pt]
- & \textit{Branch}~\xi_4~\xi_3 := \textit{Branch}~\xi_3~\xi_3)\end{aligned}$ \\[2\smallskipamount]
+ & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
+ & \textit{Branch}~\xi_1~\xi_2 := \textit{Branch}~\xi_2~\xi_2, \\[-2pt]
+ & \textit{Branch}~\xi_2~\xi_2 := \textit{Branch}~\xi_2~\xi_2)\end{aligned}$ \\[2\smallskipamount]
The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps
even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
\postw
@@ -1406,7 +1407,7 @@
allowing unreachable states in the preceding example (by removing the ``$n \in
\textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
set of objects over which the induction is performed while doing the step
-so as to test the induction hypothesis's strength.}
+in order to test the induction hypothesis's strength.}
The new trees are so nonstandard that we know nothing about them, except what
the induction hypothesis states and what can be proved about all trees without
relying on induction or case distinction. The key observation is,
@@ -1417,8 +1418,8 @@
objects, and Nitpick won't find any nonstandard counterexample.}
\end{quote}
%
-But here, Nitpick did find some nonstandard trees $t = \xi_3$
-and $u = \xi_4$ such that $a \in \textit{labels}~t$, $b \notin
+But here, Nitpick did find some nonstandard trees $t = \xi_1$
+and $u = \xi_2$ such that $a \in \textit{labels}~t$, $b \notin
\textit{labels}~t$, $a \notin \textit{labels}~u$, and $b \in \textit{labels}~u$.
Because neither tree contains both $a$ and $b$, the induction hypothesis tells
us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$,
@@ -1441,7 +1442,7 @@
\postw
This time, Nitpick won't find any nonstandard counterexample, and we can perform
-the induction step using \textbf{auto}.
+the induction step using \textit{auto}.
\section{Case Studies}
\label{case-studies}
@@ -1726,8 +1727,8 @@
\textbf{nitpick} \\[2\smallskipamount]
\slshape Nitpick found a counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
-\hbox{}\qquad\qquad $t = N~a_3~1~\Lambda~\Lambda$ \\
-\hbox{}\qquad\qquad $x = a_4$
+\hbox{}\qquad\qquad $t = N~a_1~1~\Lambda~\Lambda$ \\
+\hbox{}\qquad\qquad $x = a_2$
\postw
It's hard to see why this is a counterexample. To improve readability, we will
@@ -2138,7 +2139,7 @@
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: For efficiency, it is
recommended to install the JNI version of MiniSat and set \textit{sat\_solver} =
-\textit{MiniSatJNI}. Also be aware that many of the counterexamples may look
+\textit{MiniSat\_JNI}. Also be aware that many of the counterexamples may look
identical, unless the \textit{show\_all} (\S\ref{output-format}) option is
enabled.
@@ -2150,7 +2151,7 @@
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:
For efficiency, it is recommended to install the JNI version of MiniSat and set
-\textit{sat\_solver} = \textit{MiniSatJNI}. Also be aware that many of the
+\textit{sat\_solver} = \textit{MiniSat\_JNI}. Also be aware that many of the
counterexamples may look identical, unless the \textit{show\_all}
(\S\ref{output-format}) option is enabled.
@@ -2243,7 +2244,7 @@
to be faster than their Java counterparts, but they can be more difficult to
install. Also, if you set the \textit{max\_potential} (\S\ref{output-format}) or
\textit{max\_genuine} (\S\ref{output-format}) option to a value greater than 1,
-you will need an incremental SAT solver, such as \textit{MiniSatJNI}
+you will need an incremental SAT solver, such as \textit{MiniSat\_JNI}
(recommended) or \textit{SAT4J}.
The supported solvers are listed below:
@@ -2257,7 +2258,7 @@
\url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
and 2.0 beta (2007-07-21).
-\item[$\bullet$] \textbf{\textit{MiniSatJNI}}: The JNI (Java Native Interface)
+\item[$\bullet$] \textbf{\textit{MiniSat\_JNI}}: The JNI (Java Native Interface)
version of MiniSat is bundled in \texttt{nativesolver.\allowbreak tgz}, which
you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
version of MiniSat, the JNI version can be used incrementally.
@@ -2279,7 +2280,7 @@
\url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
versions 2004-05-13, 2004-11-15, and 2007-03-12.
-\item[$\bullet$] \textbf{\textit{zChaffJNI}}: The JNI version of zChaff is
+\item[$\bullet$] \textbf{\textit{zChaff\_JNI}}: The JNI version of zChaff is
bundled in \texttt{native\-solver.\allowbreak tgz}, which you will find on
Kodkod's web site \cite{kodkod-2009}.
@@ -2295,7 +2296,7 @@
executable. The BerkMin executables are available at
\url{http://eigold.tripod.com/BerkMin.html}.
-\item[$\bullet$] \textbf{\textit{BerkMinAlloy}}: Variant of BerkMin that is
+\item[$\bullet$] \textbf{\textit{BerkMin\_Alloy}}: Variant of BerkMin that is
included with Alloy 4 and calls itself ``sat56'' in its banner text. To use this
version of BerkMin, set the environment variable
\texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin}
@@ -2313,7 +2314,7 @@
install the official SAT4J packages, because their API is incompatible with
Kodkod.
-\item[$\bullet$] \textbf{\textit{SAT4JLight}}: Variant of SAT4J that is
+\item[$\bullet$] \textbf{\textit{SAT4J\_Light}}: Variant of SAT4J that is
optimized for small problems. It can also be used incrementally.
\item[$\bullet$] \textbf{\textit{HaifaSat}}: HaifaSat 1.0 beta is an
@@ -2324,7 +2325,7 @@
\item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to
\textit{smart}, Nitpick selects the first solver among MiniSat,
-PicoSAT, zChaff, RSat, BerkMin, BerkMinAlloy, Jerusat, MiniSatJNI, and zChaffJNI
+PicoSAT, zChaff, RSat, BerkMin, BerkMin\_Alloy, Jerusat, MiniSat\_JNI, and zChaff\_JNI
that is recognized by Isabelle. If none is found, it falls back on SAT4J, which
should always be available. If \textit{verbose} (\S\ref{output-format}) is
enabled, Nitpick displays which SAT solver was chosen.
--- a/doc-src/manual.bib Tue Feb 09 16:05:49 2010 +0100
+++ b/doc-src/manual.bib Tue Feb 09 16:07:51 2010 +0100
@@ -3,7 +3,7 @@
%publishers
@string{AP="Academic Press"}
@string{CUP="Cambridge University Press"}
-@string{IEEE="{\sc ieee} Computer Society Press"}
+@string{IEEE="IEEE Computer Society Press"}
@string{LNCS="Lecture Notes in Computer Science"}
@string{MIT="MIT Press"}
@string{NH="North-Holland"}
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Feb 09 16:05:49 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Tue Feb 09 16:07:51 2010 +0100
@@ -11,7 +11,7 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
subsection {* Curry in a Hurry *}
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Tue Feb 09 16:05:49 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Tue Feb 09 16:07:51 2010 +0100
@@ -11,7 +11,7 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
primrec rot where
"rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Tue Feb 09 16:05:49 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Tue Feb 09 16:07:51 2010 +0100
@@ -12,7 +12,7 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 120 s]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 120 s]
typedecl guest
typedecl key
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy Tue Feb 09 16:05:49 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Tue Feb 09 16:07:51 2010 +0100
@@ -11,7 +11,7 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
inductive p1 :: "nat \<Rightarrow> bool" where
"p1 0" |
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Tue Feb 09 16:05:49 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Tue Feb 09 16:07:51 2010 +0100
@@ -11,7 +11,7 @@
imports Nitpick
begin
-nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s,
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
card = 1\<midarrow>6, bits = 1,2,3,4,6,8]
lemma "Suc x = x + 1"
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Feb 09 16:05:49 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Feb 09 16:07:51 2010 +0100
@@ -13,7 +13,7 @@
chapter {* 3. First Steps *}
-nitpick_params [sat_solver = MiniSatJNI, max_threads = 1]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1]
subsection {* 3.1. Propositional Logic *}
--- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy Tue Feb 09 16:05:49 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy Tue Feb 09 16:07:51 2010 +0100
@@ -11,7 +11,7 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s,
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
card = 14]
lemma "x = (case u of () \<Rightarrow> y)"
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy Tue Feb 09 16:05:49 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy Tue Feb 09 16:07:51 2010 +0100
@@ -11,7 +11,7 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
record point2d =
xc :: int
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue Feb 09 16:05:49 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue Feb 09 16:07:51 2010 +0100
@@ -11,7 +11,7 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
lemma "P \<and> Q"
apply (rule conjI)
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy Tue Feb 09 16:05:49 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Tue Feb 09 16:07:51 2010 +0100
@@ -11,7 +11,7 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s,
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
card = 4]
fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Feb 09 16:05:49 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Feb 09 16:07:51 2010 +0100
@@ -11,7 +11,8 @@
imports Main Rational
begin
-nitpick_params [card = 1\<midarrow>4, timeout = 30 s]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
+ card = 1\<midarrow>4]
typedef three = "{0\<Colon>nat, 1, 2}"
by blast
--- a/src/HOL/Tools/Nitpick/HISTORY Tue Feb 09 16:05:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY Tue Feb 09 16:07:51 2010 +0100
@@ -4,6 +4,8 @@
* Added "std" option and implemented support for nonstandard models
* Fixed soundness bugs related to "destroy_constrs" optimization and record
getters
+ * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
+ "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
Version 2009-1
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Tue Feb 09 16:05:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Tue Feb 09 16:07:51 2010 +0100
@@ -42,12 +42,12 @@
if berkmin_exec = "" then "BerkMin561"
else berkmin_exec, [], "Satisfiable !!",
"solution =", "UNSATISFIABLE !!")),
- ("BerkMinAlloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])),
+ ("BerkMin_Alloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])),
("Jerusat", External (ToStdout, "JERUSAT_HOME", "Jerusat1.3", [])),
- ("MiniSatJNI", Internal (JNI, Incremental, ["MiniSat"])),
- ("zChaffJNI", Internal (JNI, Batch, ["zChaff"])),
+ ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
+ ("zChaff_JNI", Internal (JNI, Batch, ["zChaff"])),
("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
- ("SAT4JLight", Internal (Java, Incremental, ["LightSAT4J"])),
+ ("SAT4J_Light", Internal (Java, Incremental, ["LightSAT4J"])),
("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"],
"s SATISFIABLE", "v ", "s UNSATISFIABLE"))]
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Feb 09 16:05:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Feb 09 16:07:51 2010 +0100
@@ -122,6 +122,7 @@
val nth_sel_for_constr : styp -> int -> styp
val boxed_nth_sel_for_constr : hol_context -> styp -> int -> styp
val sel_no_from_name : string -> int
+ val close_form : term -> term
val eta_expand : typ list -> term -> int -> term
val extensionalize : term -> term
val distinctness_formula : typ -> term list -> term
@@ -782,6 +783,22 @@
else
0
+(* term -> term *)
+val close_form =
+ let
+ (* (indexname * typ) list -> (indexname * typ) list -> term -> term *)
+ fun close_up zs zs' =
+ fold (fn (z as ((s, _), T)) => fn t' =>
+ Term.all T $ Abs (s, T, abstract_over (Var z, t')))
+ (take (length zs' - length zs) zs')
+ (* (indexname * typ) list -> term -> term *)
+ fun aux zs (@{const "==>"} $ t1 $ t2) =
+ let val zs' = Term.add_vars t1 zs in
+ close_up zs zs' (Logic.mk_implies (t1, aux zs' t2))
+ end
+ | aux zs t = close_up zs (Term.add_vars t zs) t
+ in aux [] end
+
(* typ list -> term -> int -> term *)
fun eta_expand _ t 0 = t
| eta_expand Ts (Abs (s, T, t')) n =
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Feb 09 16:05:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Feb 09 16:07:51 2010 +0100
@@ -317,7 +317,7 @@
[ts] |> not exclusive ? cons (KK.TupleSet [])
else
[KK.TupleSet [],
- if exclusive andalso T1 = T2 andalso epsilon > delta then
+ if (* ### exclusive andalso*) T1 = T2 andalso epsilon > delta then
index_seq delta (epsilon - delta)
|> map (fn j =>
KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]],
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Feb 09 16:05:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Feb 09 16:07:51 2010 +0100
@@ -943,7 +943,7 @@
|> map Logic.mk_equals,
Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
list_comb (Const x2, bounds2 @ args2)))
- |> Refute.close_form (* TODO: needed? *)
+ |> close_form (* TODO: needed? *)
end
(* hol_context -> styp list -> term list *)
@@ -1391,7 +1391,7 @@
val skolem_depth = if skolemize then 4 else ~1
val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
core_t) = t |> unfold_defs_in_term hol_ctxt
- |> Refute.close_form
+ |> close_form
|> skolemize_term_and_more hol_ctxt skolem_depth
|> specialize_consts_in_term hol_ctxt 0
|> `(axioms_for_term hol_ctxt)
@@ -1420,7 +1420,7 @@
#> simplify_constrs_and_sels thy
#> distribute_quantifiers
#> push_quantifiers_inward thy
- #> not core ? Refute.close_form
+ #> close_form
#> Term.map_abs_vars shortest_name
in
(((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),