# HG changeset patch
# User blanchet
# Date 1316969005 -7200
# Node ID 3cb902212af520559061e5c4f29df01eb30b1d44
# Parent  dd803d319d5b23e97c3894fcc5e91e0f0071c651
update list of SAT solvers reflecting Kodkod 1.5

diff -r dd803d319d5b -r 3cb902212af5 src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Sun Sep 25 17:25:34 2011 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Sun Sep 25 18:43:25 2011 +0200
@@ -23,7 +23,7 @@
 
 datatype sat_solver_info =
   Internal of availability * mode * string list |
-  External of sink * string * string * string list |
+  External of string * string * string list |
   ExternalV2 of sink * string * string * string list * string * string * string
 
 (* for compatibility with "SatSolver" *)
@@ -31,12 +31,12 @@
 
 (* (string * sat_solver_info) list *)
 val static_list =
-  [("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
+  [("Lingeling_JNI", Internal (JNI, Batch, ["Lingeling"])),
+   ("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
+   ("CryptoMiniSat_JNI", Internal (JNI, Batch, ["CryptoMiniSat"])),
+   ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
                            "UNSAT")),
    ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
-   ("CryptoMiniSat", External (ToStdout, "CRYPTOMINISAT_HOME", "cryptominisat",
-                               [])),
-   ("PicoSAT", External (ToStdout, "PICOSAT_HOME", "picosat", [])),
    ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
                           "Instance Satisfiable", "",
                           "Instance Unsatisfiable")),
@@ -47,8 +47,7 @@
                            if berkmin_exec = "" then "BerkMin561"
                            else berkmin_exec, [], "Satisfiable          !!",
                            "solution =", "UNSATISFIABLE          !!")),
-   ("BerkMin_Alloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])),
-   ("Jerusat", External (ToStdout, "JERUSAT_HOME", "Jerusat1.3", [])),
+   ("BerkMin_Alloy", External ("BERKMINALLOY_HOME", "berkmin", [])),
    ("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
    ("SAT4J_Light", Internal (Java, Incremental, ["LightSAT4J"]))]
 
@@ -69,8 +68,9 @@
                          "/"
                    in
                      [if null markers then "External" else "ExternalV2",
-                      dir ^ dir_sep ^ exec, base ^ ".cnf",
-                      if dev = ToFile then out_file else ""] @ markers @
+                      dir ^ dir_sep ^ exec, base ^ ".cnf"] @
+                      (if null markers then []
+                       else [if dev = ToFile then out_file else ""]) @ markers @
                      (if dev = ToFile then [out_file] else []) @ args
                    end)
 fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
@@ -89,8 +89,8 @@
         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, External (home, exec, args)) =
+    dynamic_entry_for_external name ToStdout 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]