# 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", [],