1.1 --- a/doc-src/Nitpick/nitpick.tex Mon Nov 16 10:03:58 2009 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Mon Nov 16 10:24:28 2009 +0100
1.3 @@ -2019,9 +2019,11 @@
1.4 you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
1.5 version of MiniSat, the JNI version can be used incrementally.
1.6
1.7 +%%% No longer true:
1.8 +%%% "It is bundled with Kodkodi and requires no further installation or
1.9 +%%% configuration steps. Alternatively,"
1.10 \item[$\bullet$] \textbf{\textit{PicoSAT}}: PicoSAT is an efficient solver
1.11 -written in C. It is bundled with Kodkodi and requires no further installation or
1.12 -configuration steps. Alternatively, you can install a standard version of
1.13 +written in C. You can install a standard version of
1.14 PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
1.15 that contains the \texttt{picosat} executable. The C sources for PicoSAT are
1.16 available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi.
1.17 @@ -2078,11 +2080,11 @@
1.18 \url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}.
1.19
1.20 \item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to
1.21 -\textit{smart}, Nitpick selects the first solver among MiniSatJNI, MiniSat,
1.22 -PicoSAT, zChaffJNI, zChaff, RSat, BerkMin, BerkMinAlloy, and Jerusat that is
1.23 -recognized by Isabelle. If none is found, it falls back on SAT4J, which should
1.24 -always be available. If \textit{verbose} is enabled, Nitpick displays which SAT
1.25 -solver was chosen.
1.26 +\textit{smart}, Nitpick selects the first solver among MiniSat,
1.27 +PicoSAT, zChaff, RSat, BerkMin, BerkMinAlloy, Jerusat, MiniSatJNI, and zChaffJNI
1.28 +that is recognized by Isabelle. If none is found, it falls back on SAT4J, which
1.29 +should always be available. If \textit{verbose} (\S\ref{output-format}) is
1.30 +enabled, Nitpick displays which SAT solver was chosen.
1.31 \end{enum}
1.32 \fussy
1.33
1.34 @@ -2469,8 +2471,8 @@
1.35
1.36 \item[$\bullet$] Local definitions are not supported and result in an error.
1.37
1.38 -\item[$\bullet$] All constants and types whose names start with
1.39 -\textit{Nitpick}{.} are reserved for internal use.
1.40 +%\item[$\bullet$] All constants and types whose names start with
1.41 +%\textit{Nitpick}{.} are reserved for internal use.
1.42 \end{enum}
1.43
1.44 \let\em=\sl
2.1 --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Mon Nov 16 10:03:58 2009 +0100
2.2 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Mon Nov 16 10:24:28 2009 +0100
2.3 @@ -28,11 +28,9 @@
2.4
2.5 (* (string * sat_solver_info) list *)
2.6 val static_list =
2.7 - [("MiniSatJNI", Internal (JNI, Incremental, ["MiniSat"])),
2.8 - ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
2.9 + [("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
2.10 "UNSAT")),
2.11 ("PicoSAT", External (ToStdout, "PICOSAT_HOME", "picosat", [])),
2.12 - ("zChaffJNI", Internal (JNI, Batch, ["zChaff"])),
2.13 ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
2.14 "Instance Satisfiable", "",
2.15 "Instance Unsatisfiable")),
2.16 @@ -44,6 +42,8 @@
2.17 "solution =", "UNSATISFIABLE !!")),
2.18 ("BerkMinAlloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])),
2.19 ("Jerusat", External (ToStdout, "JERUSAT_HOME", "Jerusat1.3", [])),
2.20 + ("MiniSatJNI", Internal (JNI, Incremental, ["MiniSat"])),
2.21 + ("zChaffJNI", Internal (JNI, Batch, ["zChaff"])),
2.22 ("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
2.23 ("SAT4JLight", Internal (Java, Incremental, ["LightSAT4J"])),
2.24 ("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"],