(* Title: HOL/Tools/Nitpick/kodkod_sat.ML
Author: Jasmin Blanchette, TU Muenchen
Copyright 2009, 2010
Kodkod SAT solver integration.
*)
signature KODKOD_SAT =
sig
val configured_sat_solvers : bool -> string list
val smart_sat_solver_name : bool -> string
val sat_solver_spec : string -> string * string list
end;
structure Kodkod_SAT : KODKOD_SAT =
struct
open Kodkod
datatype sink = ToStdout | ToFile
datatype availability =
Java |
JNI of int list
datatype mode = Batch | Incremental
datatype sat_solver_info =
Internal of availability * mode * string list |
External of string * string * string list |
ExternalV2 of sink * string * string * string list * string * string * string
(* for compatibility with "SAT_Solver" *)
val berkmin_exec = getenv "BERKMIN_EXE"
val static_list =
[("Lingeling_JNI", Internal (JNI [1, 5], Batch, ["Lingeling"])),
("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
("CryptoMiniSat_JNI", Internal (JNI [1, 5], Batch, ["CryptoMiniSat"])),
("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
"UNSAT")),
("MiniSat_JNI", Internal (JNI [], Incremental, ["MiniSat"])),
("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
"Instance Satisfiable", "",
"Instance Unsatisfiable")),
("RSat", ExternalV2 (ToStdout, "RSAT_HOME", "rsat", ["-s"],
"s SATISFIABLE", "v ", "s UNSATISFIABLE")),
("Riss3g", External ("RISS3G_HOME", "riss3g", [])),
("BerkMin", ExternalV2 (ToStdout, "BERKMIN_HOME",
if berkmin_exec = "" then "BerkMin561"
else berkmin_exec, [], "Satisfiable !!",
"solution =", "UNSATISFIABLE !!")),
("BerkMin_Alloy", External ("BERKMINALLOY_HOME", "berkmin", [])),
("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
("SAT4J_Light", Internal (Java, Incremental, ["LightSAT4J"]))]
fun dynamic_entry_for_external name dev home exec args markers =
case getenv home of
"" => NONE
| dir =>
SOME (name, fn () =>
let
val serial_str = serial_string ()
val base = name ^ serial_str
val out_file = base ^ ".out"
val dir_sep =
if String.isSubstring "\\" dir andalso
not (String.isSubstring "/" dir) then
"\\"
else
"/"
in
[if null markers then "External" else "ExternalV2",
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)) =
if incremental andalso mode = Batch then NONE else SOME (name, K ss)
| dynamic_entry_for_info incremental
(name, Internal (JNI from_version, mode, ss)) =
if (incremental andalso mode = Batch) orelse
dict_ord int_ord (kodkodi_version (), from_version) = LESS 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 (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]
| dynamic_entry_for_info true _ = NONE
fun dynamic_list incremental =
map_filter (dynamic_entry_for_info incremental) static_list
val configured_sat_solvers = map fst o dynamic_list
val smart_sat_solver_name = fst o hd o dynamic_list
fun sat_solver_spec name =
let
val dyns = dynamic_list false
fun enum_solvers solvers =
commas (distinct (op =) (map (quote o fst) solvers))
in
(name, the (AList.lookup (op =) dyns name) ())
handle Option.Option =>
error (if AList.defined (op =) static_list name then
"The SAT solver " ^ quote name ^ " is not configured. The \
\following solvers are configured:\n" ^
enum_solvers dyns
else
"Unknown SAT solver " ^ quote name ^ "\nThe following \
\solvers are supported:\n" ^ enum_solvers static_list)
end
end;