# HG changeset patch
# User blanchet
# Date 1280606574 -7200
# Node ID b178a63df952a9abb488322ff11e4a173115ba58
# Parent  6538e25cf5ddd7684282e1be9120ee818e04eee6
change the order of the SAT solvers, from fastest to slowest

diff -r 6538e25cf5dd -r b178a63df952 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Sat Jul 31 16:39:32 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Sat Jul 31 22:02:54 2010 +0200
@@ -2354,22 +2354,13 @@
 
 \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}
+\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}}
-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.%
-\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).
@@ -2380,6 +2371,15 @@
 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.
 
+\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.%
+\footref{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{PicoSAT}:} PicoSAT is an efficient solver
 written in C. You can install a standard version of
 PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
@@ -2442,11 +2442,9 @@
 optimized for small problems. It can also be used incrementally.
 
 \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, 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.
+\textit{smart}, Nitpick selects the first solver among the above that is
+recognized by Isabelle. If \textit{verbose} (\S\ref{output-format}) is enabled,
+Nitpick displays which SAT solver was chosen.
 \end{enum}
 \fussy
 
diff -r 6538e25cf5dd -r b178a63df952 src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Sat Jul 31 16:39:32 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Sat Jul 31 22:02:54 2010 +0200
@@ -26,18 +26,21 @@
   External of sink * string * string * string list |
   ExternalV2 of sink * string * string * string list * string * string * string
 
+(* for compatibility with "SatSolver" *)
 val berkmin_exec = getenv "BERKMIN_EXE"
 
 (* (string * sat_solver_info) list *)
 val static_list =
-  [("CryptoMiniSat", External (ToStdout, "CRYPTOMINISAT_HOME", "cryptominisat",
+  [("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
+                           "UNSAT")),
+   ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
+   ("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", [],
                           "Instance Satisfiable", "",
                           "Instance Unsatisfiable")),
+   ("zChaff_JNI", Internal (JNI, Batch, ["zChaff"])),
    ("RSat", ExternalV2 (ToStdout, "RSAT_HOME", "rsat", ["-s"],
                         "s SATISFIABLE", "v ", "s UNSATISFIABLE")),
    ("BerkMin", ExternalV2 (ToStdout, "BERKMIN_HOME",
@@ -46,8 +49,6 @@
                            "solution =", "UNSATISFIABLE          !!")),
    ("BerkMin_Alloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])),
    ("Jerusat", External (ToStdout, "JERUSAT_HOME", "Jerusat1.3", [])),
-   ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
-   ("zChaff_JNI", Internal (JNI, Batch, ["zChaff"])),
    ("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
    ("SAT4J_Light", Internal (Java, Incremental, ["LightSAT4J"]))]