wneuper/isa: src/HOL/Tools/Nitpick/kodkod

     1 (*  Title:      HOL/Tools/Nitpick/kodkod_sat.ML

     2     Author:     Jasmin Blanchette, TU Muenchen

     3     Copyright   2009, 2010

     5 Kodkod SAT solver integration.

     6 *)

     8 signature KODKOD_SAT =

     9 sig

    10   val configured_sat_solvers : bool -> string list

    11   val smart_sat_solver_name : bool -> string

    12   val sat_solver_spec : string -> string * string list

    13 end;

    15 structure Kodkod_SAT : KODKOD_SAT =

    16 struct

    18 datatype sink = ToStdout | ToFile

    19 datatype availability = Java | JNI

    20 datatype mode = Batch | Incremental

    22 datatype sat_solver_info =

    23   Internal of availability * mode * string list |

    24   External of sink * string * string * string list |

    25   ExternalV2 of sink * string * string * string list * string * string * string

    27 val berkmin_exec = getenv "BERKMIN_EXE"

    29 (* (string * sat_solver_info) list *)

    30 val static_list =

    31   [("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",

    32                            "UNSAT")),

    33    ("PicoSAT", External (ToStdout, "PICOSAT_HOME", "picosat", [])),

    34    ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],

    35                           "Instance Satisfiable", "",

    36                           "Instance Unsatisfiable")),

    37    ("RSat", ExternalV2 (ToStdout, "RSAT_HOME", "rsat", ["-s"],

    38                         "s SATISFIABLE", "v ", "s UNSATISFIABLE")),

    39    ("BerkMin", ExternalV2 (ToStdout, "BERKMIN_HOME",

    40                            if berkmin_exec = "" then "BerkMin561"

    41                            else berkmin_exec, [], "Satisfiable          !!",

    42                            "solution =", "UNSATISFIABLE          !!")),

    43    ("BerkMinAlloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])),

    44    ("Jerusat", External (ToStdout, "JERUSAT_HOME", "Jerusat1.3", [])),

    45    ("MiniSatJNI", Internal (JNI, Incremental, ["MiniSat"])),

    46    ("zChaffJNI", Internal (JNI, Batch, ["zChaff"])),

    47    ("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),

    48    ("SAT4JLight", Internal (Java, Incremental, ["LightSAT4J"])),

    49    ("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"],

    50                             "s SATISFIABLE", "v ", "s UNSATISFIABLE"))]

    52 val created_temp_dir = Unsynchronized.ref false

    54 (* string -> sink -> string -> string -> string list -> string list

    55    -> (string * (unit -> string list)) option *)

    56 fun dynamic_entry_for_external name dev home exec args markers =

    57   case getenv home of

    58     "" => NONE

    59   | dir => SOME (name, fn () =>

    60                           let

    61                             val temp_dir = getenv "ISABELLE_TMP"

    62                             val _ = if !created_temp_dir then

    63                                       ()

    64                                     else

    65                                       (created_temp_dir := true;

    66                                        File.mkdir (Path.explode temp_dir))

    67                             val temp = temp_dir ^ "/" ^ name ^ serial_string ()

    68                             val out_file = temp ^ ".out"

    69                           in

    70                             [if null markers then "External" else "ExternalV2",

    71                              dir ^ "/" ^ exec, temp ^ ".cnf",

    72                              if dev = ToFile then out_file else ""] @ markers @

    73                             (if dev = ToFile then [out_file] else []) @ args

    74                           end)

    75 (* bool -> string * sat_solver_info

    76    -> (string * (unit -> string list)) option *)

    77 fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =

    78     if incremental andalso mode = Batch then NONE else SOME (name, K ss)

    79   | dynamic_entry_for_info incremental (name, Internal (JNI, mode, ss)) =

    80     if incremental andalso mode = Batch then

    81       NONE

    82     else

    83       let

    84         val lib_paths = getenv "KODKODI_JAVA_LIBRARY_PATH"

    85                         |> space_explode ":"

    86       in

    87         if exists (fn path => File.exists (Path.explode (path ^ "/")))

    88                   lib_paths then

    89           SOME (name, K ss)

    90         else

    91           NONE

    92       end

    93   | dynamic_entry_for_info false (name, External (dev, home, exec, args)) =

    94     dynamic_entry_for_external name dev home exec args []

    95   | dynamic_entry_for_info false (name, ExternalV2 (dev, home, exec, args,

    96                                                     m1, m2, m3)) =

    97     dynamic_entry_for_external name dev home exec args [m1, m2, m3]

    98   | dynamic_entry_for_info true _ = NONE

    99 (* bool -> (string * (unit -> string list)) list *)

   100 fun dynamic_list incremental =

   101   map_filter (dynamic_entry_for_info incremental) static_list

   103 (* bool -> string list *)

   104 val configured_sat_solvers = map fst o dynamic_list

   106 (* bool -> string *)

   107 val smart_sat_solver_name = dynamic_list #> hd #> fst

   109 (* (string * 'a) list -> string *)

   110 fun enum_solvers xs = commas (map (quote o fst) xs |> distinct (op =))

   111 (* string -> string * string list *)

   112 fun sat_solver_spec name =

   113   let val dynamic_list = dynamic_list false in

   114     (name, the (AList.lookup (op =) dynamic_list name) ())

   115     handle Option.Option =>

   116            error (if AList.defined (op =) static_list name then

   117                     "The SAT solver " ^ quote name ^ " is not configured. The \

   118                     \following solvers are configured:\n" ^

   119                     enum_solvers dynamic_list ^ "."

   120                   else

   121                     "Unknown SAT solver " ^ quote name ^ ". The following \

   122                     \solvers are supported:\n" ^ enum_solvers static_list ^ ".")

   123   end

   125 end;

author	blanchet
	Tue, 02 Feb 2010 11:38:38 +0100
changeset 34969	7b8c366e34a2
parent 33982	1ae222745c4a
child 34985	5e492a862b34
permissions	-rw-r--r--