# HG changeset patch
# User blanchet
# Date 1258363468 -3600
# Node ID 040852c7177997fb2174010fbc7126d995d85328
# Parent  7017aee615d69376c89c473c6f791dfcd291a630
change the order in which Nitpick tries SAT solvers;
so that the binary JNIs come further down the list and can
easily be overridden

diff -r 7017aee615d6 -r 040852c71779 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Mon Nov 16 10:03:58 2009 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Mon Nov 16 10:24:28 2009 +0100
@@ -2019,9 +2019,11 @@
 you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
 version of MiniSat, the JNI version can be used incrementally.
 
+%%% No longer true:
+%%% "It is bundled with Kodkodi and requires no further installation or
+%%% configuration steps. Alternatively,"
 \item[$\bullet$] \textbf{\textit{PicoSAT}}: PicoSAT is an efficient solver
-written in C. It is bundled with Kodkodi and requires no further installation or
-configuration steps. Alternatively, you can install a standard version of
+written in C. You can install a standard version of
 PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
 that contains the \texttt{picosat} executable. The C sources for PicoSAT are
 available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi.
@@ -2078,11 +2080,11 @@
 \url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}.
 
 \item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to
-\textit{smart}, Nitpick selects the first solver among MiniSatJNI, MiniSat,
-PicoSAT, zChaffJNI, zChaff, RSat, BerkMin, BerkMinAlloy, and Jerusat that is
-recognized by Isabelle. If none is found, it falls back on SAT4J, which should
-always be available. If \textit{verbose} is enabled, Nitpick displays which SAT
-solver was chosen.
+\textit{smart}, Nitpick selects the first solver among MiniSat,
+PicoSAT, zChaff, RSat, BerkMin, BerkMinAlloy, Jerusat, MiniSatJNI, and zChaffJNI
+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.
 \end{enum}
 \fussy
 
@@ -2469,8 +2471,8 @@
 
 \item[$\bullet$] Local definitions are not supported and result in an error.
 
-\item[$\bullet$] All constants and types whose names start with
-\textit{Nitpick}{.} are reserved for internal use.
+%\item[$\bullet$] All constants and types whose names start with
+%\textit{Nitpick}{.} are reserved for internal use.
 \end{enum}
 
 \let\em=\sl
diff -r 7017aee615d6 -r 040852c71779 src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Mon Nov 16 10:03:58 2009 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Mon Nov 16 10:24:28 2009 +0100
@@ -28,11 +28,9 @@
 
 (* (string * sat_solver_info) list *)
 val static_list =
-  [("MiniSatJNI", Internal (JNI, Incremental, ["MiniSat"])),
-   ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
+  [("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
                            "UNSAT")),
    ("PicoSAT", External (ToStdout, "PICOSAT_HOME", "picosat", [])),
-   ("zChaffJNI", Internal (JNI, Batch, ["zChaff"])),
    ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
                           "Instance Satisfiable", "",
                           "Instance Unsatisfiable")),
@@ -44,6 +42,8 @@
                            "solution =", "UNSATISFIABLE          !!")),
    ("BerkMinAlloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])),
    ("Jerusat", External (ToStdout, "JERUSAT_HOME", "Jerusat1.3", [])),
+   ("MiniSatJNI", Internal (JNI, Incremental, ["MiniSat"])),
+   ("zChaffJNI", Internal (JNI, Batch, ["zChaff"])),
    ("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
    ("SAT4JLight", Internal (Java, Incremental, ["LightSAT4J"])),
    ("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"],