--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Sat Jul 31 16:39:32 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Sat Jul 31 22:02:54 2010 +0200
@@ -26,18 +26,21 @@
External of sink * string * string * string list |
ExternalV2 of sink * string * string * string list * string * string * string
+(* for compatibility with "SatSolver" *)
val berkmin_exec = getenv "BERKMIN_EXE"
(* (string * sat_solver_info) list *)
val static_list =
- [("CryptoMiniSat", External (ToStdout, "CRYPTOMINISAT_HOME", "cryptominisat",
+ [("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
+ "UNSAT")),
+ ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
+ ("CryptoMiniSat", External (ToStdout, "CRYPTOMINISAT_HOME", "cryptominisat",
[])),
- ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
- "UNSAT")),
("PicoSAT", External (ToStdout, "PICOSAT_HOME", "picosat", [])),
("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
"Instance Satisfiable", "",
"Instance Unsatisfiable")),
+ ("zChaff_JNI", Internal (JNI, Batch, ["zChaff"])),
("RSat", ExternalV2 (ToStdout, "RSAT_HOME", "rsat", ["-s"],
"s SATISFIABLE", "v ", "s UNSATISFIABLE")),
("BerkMin", ExternalV2 (ToStdout, "BERKMIN_HOME",
@@ -46,8 +49,6 @@
"solution =", "UNSATISFIABLE !!")),
("BerkMin_Alloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])),
("Jerusat", External (ToStdout, "JERUSAT_HOME", "Jerusat1.3", [])),
- ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
- ("zChaff_JNI", Internal (JNI, Batch, ["zChaff"])),
("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
("SAT4J_Light", Internal (Java, Incremental, ["LightSAT4J"]))]