1.1 --- a/doc-src/Nitpick/nitpick.tex	Mon Oct 26 14:57:49 2009 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Mon Oct 26 18:52:16 2009 +0100
     1.3 @@ -2091,11 +2091,11 @@
     1.4  \url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}.
     1.5  
     1.6  \item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to
     1.7 -\textit{smart}, Nitpick selects the first solver among MiniSat, PicoSAT, zChaff,
     1.8 -RSat, BerkMin, BerkMinAlloy, and Jerusat that is recognized by Isabelle. If none
     1.9 -is found, it falls back on SAT4J, which should always be available. If
    1.10 -\textit{verbose} is enabled, Nitpick displays which SAT solver was chosen.
    1.11 -
    1.12 +\textit{smart}, Nitpick selects the first solver among MiniSatJNI, MiniSat,
    1.13 +PicoSAT, zChaffJNI, zChaff, RSat, BerkMin, BerkMinAlloy, and Jerusat that is
    1.14 +recognized by Isabelle. If none is found, it falls back on SAT4J, which should
    1.15 +always be available. If \textit{verbose} is enabled, Nitpick displays which SAT
    1.16 +solver was chosen.
    1.17  \end{enum}
    1.18  \fussy
    1.19  

     2.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Mon Oct 26 14:57:49 2009 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Mon Oct 26 18:52:16 2009 +0100
     2.3 @@ -1043,7 +1043,8 @@
     2.4              let
     2.5                val code =
     2.6                  system ("env CLASSPATH=\"$KODKODI_CLASSPATH:$CLASSPATH\" \
     2.7 -                        \\"$ISABELLE_TOOL\" java \
     2.8 +                        \JAVA_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
     2.9 +                        \$JAVA_LIBRARY_PATH\" \"$ISABELLE_TOOL\" java \
    2.10                          \de.tum.in.isabelle.Kodkodi.Kodkodi" ^
    2.11                          (if ms >= 0 then " -max-msecs " ^ Int.toString ms
    2.12                           else "") ^

     3.1 --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Mon Oct 26 14:57:49 2009 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Mon Oct 26 18:52:16 2009 +0100
     3.3 @@ -16,9 +16,11 @@
     3.4  struct
     3.5  
     3.6  datatype sink = ToStdout | ToFile
     3.7 +datatype availability = Java | JNI
     3.8 +datatype mode = Batch | Incremental
     3.9  
    3.10  datatype sat_solver_info =
    3.11 -  Internal of bool * string list |
    3.12 +  Internal of availability * mode * string list |
    3.13    External of sink * string * string * string list |
    3.14    ExternalV2 of sink * string * string * string list * string * string * string
    3.15  
    3.16 @@ -26,9 +28,11 @@
    3.17  
    3.18  (* (string * sat_solver_info) list *)
    3.19  val static_list =
    3.20 -  [("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
    3.21 +  [("MiniSatJNI", Internal (JNI, Incremental, ["MiniSat"])),
    3.22 +   ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
    3.23                             "UNSAT")),
    3.24     ("PicoSAT", External (ToStdout, "PICOSAT_HOME", "picosat", [])),
    3.25 +   ("zChaffJNI", Internal (JNI, Batch, ["zChaff"])),
    3.26     ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
    3.27                            "Instance Satisfiable", "",
    3.28                            "Instance Unsatisfiable")),
    3.29 @@ -40,10 +44,8 @@
    3.30                             "solution =", "UNSATISFIABLE          !!")),
    3.31     ("BerkMinAlloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])),
    3.32     ("Jerusat", External (ToStdout, "JERUSAT_HOME", "Jerusat1.3", [])),
    3.33 -   ("SAT4J", Internal (true, ["DefaultSAT4J"])),
    3.34 -   ("MiniSatJNI", Internal (true, ["MiniSat"])),
    3.35 -   ("zChaffJNI", Internal (false, ["zChaff"])),
    3.36 -   ("SAT4JLight", Internal (true, ["LightSAT4J"])),
    3.37 +   ("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
    3.38 +   ("SAT4JLight", Internal (Java, Incremental, ["LightSAT4J"])),
    3.39     ("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"],
    3.40                              "s SATISFIABLE", "v ", "s UNSATISFIABLE"))]
    3.41  
    3.42 @@ -72,13 +74,27 @@
    3.43                            end)
    3.44  (* bool -> string * sat_solver_info
    3.45     -> (string * (unit -> string list)) option *)
    3.46 -fun dynamic_entry_for_info false (name, Internal (_, ss)) = SOME (name, K ss)
    3.47 +fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
    3.48 +    if incremental andalso mode = Batch then NONE else SOME (name, K ss)
    3.49 +  | dynamic_entry_for_info incremental (name, Internal (JNI, mode, ss)) =
    3.50 +    if incremental andalso mode = Batch then
    3.51 +      NONE
    3.52 +    else
    3.53 +      let
    3.54 +        val lib_paths = getenv "KODKODI_JAVA_LIBRARY_PATH"
    3.55 +                        |> space_explode ":"
    3.56 +      in
    3.57 +        if exists (fn path => File.exists (Path.explode (path ^ "/")))
    3.58 +                  lib_paths then
    3.59 +          SOME (name, K ss)
    3.60 +        else
    3.61 +          NONE
    3.62 +      end
    3.63    | dynamic_entry_for_info false (name, External (dev, home, exec, args)) =
    3.64      dynamic_entry_for_external name dev home exec args []
    3.65    | dynamic_entry_for_info false (name, ExternalV2 (dev, home, exec, args,
    3.66                                                      m1, m2, m3)) =
    3.67      dynamic_entry_for_external name dev home exec args [m1, m2, m3]
    3.68 -  | dynamic_entry_for_info true (name, Internal (true, ss)) = SOME (name, K ss)
    3.69    | dynamic_entry_for_info true _ = NONE
    3.70  (* bool -> (string * (unit -> string list)) list *)
    3.71  fun dynamic_list incremental =