# HG changeset patch
# User blanchet
# Date 1317030112 -7200
# Node ID 01434214409182e0c66fbedeba0ccb48ab332365
# Parent  54c4e12bb5e032a4811ffcdf96b27e12670d61e7
put CryptoMiniSat first and remove warning about unsoundness now that it has been fixed in Kodkod

diff -r 54c4e12bb5e0 -r 014342144091 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Mon Sep 26 10:57:20 2011 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Mon Sep 26 11:41:52 2011 +0200
@@ -34,7 +34,7 @@
 \def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
 
 \hyphenation{Mini-Sat size-change First-Steps grand-parent nit-pick
-counter-example counter-examples data-type data-types co-data-type 
+counter-example counter-examples data-type data-types co-data-type
 co-data-types in-duc-tive co-in-duc-tive}
 
 \urlstyle{tt}
@@ -1072,7 +1072,7 @@
 \slshape Nitpick found no counterexample.
 \postw
 
-In the first \textbf{nitpick} invocation, the after-the-fact check discovered 
+In the first \textbf{nitpick} invocation, the after-the-fact check discovered
 that the two known elements of type $'a~\textit{llist}$ are bisimilar.
 
 A compromise between leaving out the bisimilarity predicate from the Kodkod
@@ -1925,7 +1925,7 @@
 \textit{falsify} is enabled.
 
 \opsmart{user\_axioms}{no\_user\_axioms}
-Specifies whether the user-defined axioms (specified using 
+Specifies whether the user-defined axioms (specified using
 \textbf{axiomatization} and \textbf{axioms}) should be considered. If the option
 is set to \textit{smart}, Nitpick performs an ad hoc axiom selection based on
 the constants that occur in the formula to falsify. The option is implicitly set
@@ -2337,11 +2337,6 @@
 
 \begin{enum}
 
-\item[$\bullet$] \textbf{\textit{Lingeling\_JNI}:}
-Lingeling is an efficient solver written in C. The JNI (Java Native Interface)
-version of Lingeling is bundled with Kodkodi and is precompiled for Linux and
-Mac~OS~X. It is also available from the Kodkod web site \cite{kodkod-2009}. 
-
 \item[$\bullet$] \textbf{\textit{CryptoMiniSat}:} CryptoMiniSat is the winner of
 the 2010 SAT Race. To use CryptoMiniSat, set the environment variable
 \texttt{CRYPTO\-MINISAT\_}\discretionary{}{}{}\texttt{HOME} to the directory that contains the \texttt{crypto\-minisat}
@@ -2356,8 +2351,12 @@
 \item[$\bullet$] \textbf{\textit{CryptoMiniSat\_JNI}:} The JNI (Java Native
 Interface) version of CryptoMiniSat is bundled with Kodkodi and is precompiled
 for Linux and Mac~OS~X. It is also available from the Kodkod web site
-\cite{kodkod-2009}. \textbf{Warning:} The CryptoMiniSat--Kodkod integration
-appears to be unsound. Use at your own risk and peril.
+\cite{kodkod-2009}.
+
+\item[$\bullet$] \textbf{\textit{Lingeling\_JNI}:}
+Lingeling is an efficient solver written in C. The JNI (Java Native Interface)
+version of Lingeling is bundled with Kodkodi and is precompiled for Linux and
+Mac~OS~X. It is also available from the Kodkod web site \cite{kodkod-2009}.
 
 \item[$\bullet$] \textbf{\textit{MiniSat}:} MiniSat is an efficient solver
 written in \cpp{}. To use MiniSat, set the environment variable
@@ -2848,7 +2847,7 @@
 ``$\textit{prec}~(\textit{Suc}~n) = n$'' \\[2\smallskipamount]
 \textbf{lemma} ``$\textit{prec}~0 = \undef$'' \\
 \textbf{nitpick} \\[2\smallskipamount]
-\quad{\slshape Nitpick found a counterexample for \textit{card nat}~= 2: 
+\quad{\slshape Nitpick found a counterexample for \textit{card nat}~= 2:
 \nopagebreak
 \\[2\smallskipamount]
 \hbox{}\qquad Empty assignment} \nopagebreak\\[2\smallskipamount]
diff -r 54c4e12bb5e0 -r 014342144091 src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Mon Sep 26 10:57:20 2011 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Mon Sep 26 11:41:52 2011 +0200
@@ -31,9 +31,9 @@
 
 (* (string * sat_solver_info) list *)
 val static_list =
-  [("Lingeling_JNI", Internal (JNI, Batch, ["Lingeling"])),
-   ("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
+  [("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
    ("CryptoMiniSat_JNI", Internal (JNI, Batch, ["CryptoMiniSat"])),
+   ("Lingeling_JNI", Internal (JNI, Batch, ["Lingeling"])),
    ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
                            "UNSAT")),
    ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),