# HG changeset patch
# User blanchet
# Date 1280532231 -7200
# Node ID fb5e5a42594811db2cf672e91020ef0e2a0290ff
# Parent  a9d96531c2ee645dc7270283963790e0f1e74dd6
added support for CryptoMiniSat

diff -r a9d96531c2ee -r fb5e5a425948 doc-src/Nitpick/nitpick.tex
--- 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).
diff -r a9d96531c2ee -r fb5e5a425948 src/HOL/Tools/Nitpick/kodkod_sat.ML
--- 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", [],