1.1 --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Sun Sep 25 17:25:34 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Sun Sep 25 18:43:25 2011 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4  
     1.5  datatype sat_solver_info =
     1.6    Internal of availability * mode * string list |
     1.7 -  External of sink * string * string * string list |
     1.8 +  External of string * string * string list |
     1.9    ExternalV2 of sink * string * string * string list * string * string * string
    1.10  
    1.11  (* for compatibility with "SatSolver" *)
    1.12 @@ -31,12 +31,12 @@
    1.13  
    1.14  (* (string * sat_solver_info) list *)
    1.15  val static_list =
    1.16 -  [("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
    1.17 +  [("Lingeling_JNI", Internal (JNI, Batch, ["Lingeling"])),
    1.18 +   ("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
    1.19 +   ("CryptoMiniSat_JNI", Internal (JNI, Batch, ["CryptoMiniSat"])),
    1.20 +   ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
    1.21                             "UNSAT")),
    1.22     ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
    1.23 -   ("CryptoMiniSat", External (ToStdout, "CRYPTOMINISAT_HOME", "cryptominisat",
    1.24 -                               [])),
    1.25 -   ("PicoSAT", External (ToStdout, "PICOSAT_HOME", "picosat", [])),
    1.26     ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
    1.27                            "Instance Satisfiable", "",
    1.28                            "Instance Unsatisfiable")),
    1.29 @@ -47,8 +47,7 @@
    1.30                             if berkmin_exec = "" then "BerkMin561"
    1.31                             else berkmin_exec, [], "Satisfiable          !!",
    1.32                             "solution =", "UNSATISFIABLE          !!")),
    1.33 -   ("BerkMin_Alloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])),
    1.34 -   ("Jerusat", External (ToStdout, "JERUSAT_HOME", "Jerusat1.3", [])),
    1.35 +   ("BerkMin_Alloy", External ("BERKMINALLOY_HOME", "berkmin", [])),
    1.36     ("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
    1.37     ("SAT4J_Light", Internal (Java, Incremental, ["LightSAT4J"]))]
    1.38  
    1.39 @@ -69,8 +68,9 @@
    1.40                           "/"
    1.41                     in
    1.42                       [if null markers then "External" else "ExternalV2",
    1.43 -                      dir ^ dir_sep ^ exec, base ^ ".cnf",
    1.44 -                      if dev = ToFile then out_file else ""] @ markers @
    1.45 +                      dir ^ dir_sep ^ exec, base ^ ".cnf"] @
    1.46 +                      (if null markers then []
    1.47 +                       else [if dev = ToFile then out_file else ""]) @ markers @
    1.48                       (if dev = ToFile then [out_file] else []) @ args
    1.49                     end)
    1.50  fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
    1.51 @@ -89,8 +89,8 @@
    1.52          else
    1.53            NONE
    1.54        end
    1.55 -  | dynamic_entry_for_info false (name, External (dev, home, exec, args)) =
    1.56 -    dynamic_entry_for_external name dev home exec args []
    1.57 +  | dynamic_entry_for_info false (name, External (home, exec, args)) =
    1.58 +    dynamic_entry_for_external name ToStdout home exec args []
    1.59    | dynamic_entry_for_info false
    1.60          (name, ExternalV2 (dev, home, exec, args, m1, m2, m3)) =
    1.61      dynamic_entry_for_external name dev home exec args [m1, m2, m3]