--- a/doc-src/Nitpick/nitpick.tex Fri Jul 30 18:28:18 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex Sat Jul 31 01:23:51 2010 +0200
@@ -2354,13 +2354,22 @@
\begin{enum}
+\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}
+executable.%
+\footnote{Important note for Cygwin users: The path must be specified using
+native Windows syntax. Make sure to escape backslashes properly.%
+\label{cygwin-paths}}
+The \cpp{} sources and executables for Crypto\-Mini\-Sat are available at
+\url{http://planete.inrialpes.fr/~soos/}\allowbreak\url{CryptoMiniSat2/index.php}.
+Nitpick has been tested with version 2.51.
+
\item[$\bullet$] \textbf{\textit{MiniSat}:} MiniSat is an efficient solver
written in \cpp{}. To use MiniSat, set the environment variable
\texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat}
executable.%
-\footnote{Important note for Cygwin users: The path must be specified using
-native Windows syntax. Make sure to escape backslashes properly.%
-\label{cygwin-paths}}
+\footref{cygwin-paths}
The \cpp{} sources and executables for MiniSat are available at
\url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
and 2.0 beta (2007-07-21).
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Fri Jul 30 18:28:18 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Sat Jul 31 01:23:51 2010 +0200
@@ -30,7 +30,9 @@
(* (string * sat_solver_info) list *)
val static_list =
- [("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
+ [("CryptoMiniSat", External (ToStdout, "CRYPTOMINISAT_HOME", "cryptominisat",
+ [])),
+ ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
"UNSAT")),
("PicoSAT", External (ToStdout, "PICOSAT_HOME", "picosat", [])),
("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],