# HG changeset patch
# User blanchet
# Date 1256642186 -3600
# Node ID 1711610c5b7d7020d2dbbe836ba9f3c01063061f
# Parent  11a1af478dac0fd69ad00ba672de0ed977c83524# Parent  8b770ed796f1d18dae46ad7d732d959bea2bf846
merged

diff -r 11a1af478dac -r 1711610c5b7d doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Tue Oct 27 11:25:56 2009 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Tue Oct 27 12:16:26 2009 +0100
@@ -2091,11 +2091,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 MiniSat, PicoSAT, 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 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.
 \end{enum}
 \fussy
 
diff -r 11a1af478dac -r 1711610c5b7d src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Tue Oct 27 11:25:56 2009 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Tue Oct 27 12:16:26 2009 +0100
@@ -1043,7 +1043,8 @@
             let
               val code =
                 system ("env CLASSPATH=\"$KODKODI_CLASSPATH:$CLASSPATH\" \
-                        \\"$ISABELLE_TOOL\" java \
+                        \JAVA_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
+                        \$JAVA_LIBRARY_PATH\" \"$ISABELLE_TOOL\" java \
                         \de.tum.in.isabelle.Kodkodi.Kodkodi" ^
                         (if ms >= 0 then " -max-msecs " ^ Int.toString ms
                          else "") ^
diff -r 11a1af478dac -r 1711610c5b7d src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Tue Oct 27 11:25:56 2009 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Tue Oct 27 12:16:26 2009 +0100
@@ -16,9 +16,11 @@
 struct
 
 datatype sink = ToStdout | ToFile
+datatype availability = Java | JNI
+datatype mode = Batch | Incremental
 
 datatype sat_solver_info =
-  Internal of bool * string list |
+  Internal of availability * mode * string list |
   External of sink * string * string * string list |
   ExternalV2 of sink * string * string * string list * string * string * string
 
@@ -26,9 +28,11 @@
 
 (* (string * sat_solver_info) list *)
 val static_list =
-  [("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
+  [("MiniSatJNI", Internal (JNI, Incremental, ["MiniSat"])),
+   ("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")),
@@ -40,10 +44,8 @@
                            "solution =", "UNSATISFIABLE          !!")),
    ("BerkMinAlloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])),
    ("Jerusat", External (ToStdout, "JERUSAT_HOME", "Jerusat1.3", [])),
-   ("SAT4J", Internal (true, ["DefaultSAT4J"])),
-   ("MiniSatJNI", Internal (true, ["MiniSat"])),
-   ("zChaffJNI", Internal (false, ["zChaff"])),
-   ("SAT4JLight", Internal (true, ["LightSAT4J"])),
+   ("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
+   ("SAT4JLight", Internal (Java, Incremental, ["LightSAT4J"])),
    ("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"],
                             "s SATISFIABLE", "v ", "s UNSATISFIABLE"))]
 
@@ -72,13 +74,27 @@
                           end)
 (* bool -> string * sat_solver_info
    -> (string * (unit -> string list)) option *)
-fun dynamic_entry_for_info false (name, Internal (_, ss)) = SOME (name, K ss)
+fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
+    if incremental andalso mode = Batch then NONE else SOME (name, K ss)
+  | dynamic_entry_for_info incremental (name, Internal (JNI, mode, ss)) =
+    if incremental andalso mode = Batch then
+      NONE
+    else
+      let
+        val lib_paths = getenv "KODKODI_JAVA_LIBRARY_PATH"
+                        |> space_explode ":"
+      in
+        if exists (fn path => File.exists (Path.explode (path ^ "/")))
+                  lib_paths then
+          SOME (name, K ss)
+        else
+          NONE
+      end
   | dynamic_entry_for_info false (name, External (dev, home, exec, args)) =
     dynamic_entry_for_external name dev home exec args []
   | dynamic_entry_for_info false (name, ExternalV2 (dev, home, exec, args,
                                                     m1, m2, m3)) =
     dynamic_entry_for_external name dev home exec args [m1, m2, m3]
-  | dynamic_entry_for_info true (name, Internal (true, ss)) = SOME (name, K ss)
   | dynamic_entry_for_info true _ = NONE
 (* bool -> (string * (unit -> string list)) list *)
 fun dynamic_list incremental =