src/HOL/Tools/Nitpick/kodkod_sat.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (24 months ago)
changeset 66695 91500c024c7f
parent 63693 5b02f7757a4c
child 67560 0fa87bd86566
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/Tools/Nitpick/kodkod_sat.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2009, 2010
     4 
     5 Kodkod SAT solver integration.
     6 *)
     7 
     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;
    14 
    15 structure Kodkod_SAT : KODKOD_SAT =
    16 struct
    17 
    18 open Kodkod
    19 
    20 datatype sink = ToStdout | ToFile
    21 datatype availability =
    22   Java |
    23   JNI of int list
    24 datatype mode = Batch | Incremental
    25 
    26 datatype sat_solver_info =
    27   Internal of availability * mode * string list |
    28   External of string * string * string list |
    29   ExternalV2 of sink * string * string * string list * string * string * string
    30 
    31 (* for compatibility with "SAT_Solver" *)
    32 val berkmin_exec = getenv "BERKMIN_EXE"
    33 
    34 val static_list =
    35   [("Lingeling_JNI", Internal (JNI [1, 5], Batch, ["Lingeling"])),
    36    ("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
    37    ("CryptoMiniSat_JNI", Internal (JNI [1, 5], Batch, ["CryptoMiniSat"])),
    38    ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
    39                            "UNSAT")),
    40    ("MiniSat_JNI", Internal (JNI [], Incremental, ["MiniSat"])),
    41    ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
    42                           "Instance Satisfiable", "",
    43                           "Instance Unsatisfiable")),
    44    ("RSat", ExternalV2 (ToStdout, "RSAT_HOME", "rsat", ["-s"],
    45                         "s SATISFIABLE", "v ", "s UNSATISFIABLE")),
    46    ("Riss3g", External ("RISS3G_HOME", "riss3g", [])),
    47    ("BerkMin", ExternalV2 (ToStdout, "BERKMIN_HOME",
    48                            if berkmin_exec = "" then "BerkMin561"
    49                            else berkmin_exec, [], "Satisfiable          !!",
    50                            "solution =", "UNSATISFIABLE          !!")),
    51    ("BerkMin_Alloy", External ("BERKMINALLOY_HOME", "berkmin", [])),
    52    ("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
    53    ("SAT4J_Light", Internal (Java, Incremental, ["LightSAT4J"]))]
    54 
    55 fun dynamic_entry_for_external name dev home exec args markers =
    56   case getenv home of
    57     "" => NONE
    58   | dir =>
    59     SOME (name, fn () =>
    60                    let
    61                      val serial_str = serial_string ()
    62                      val base = name ^ serial_str
    63                      val out_file = base ^ ".out"
    64                      val dir_sep =
    65                        if String.isSubstring "\\" dir andalso
    66                           not (String.isSubstring "/" dir) then
    67                          "\\"
    68                        else
    69                          "/"
    70                    in
    71                      [if null markers then "External" else "ExternalV2",
    72                       dir ^ dir_sep ^ exec, base ^ ".cnf"] @
    73                       (if null markers then []
    74                        else [if dev = ToFile then out_file else ""]) @ markers @
    75                      (if dev = ToFile then [out_file] else []) @ args
    76                    end)
    77 
    78 fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
    79     if incremental andalso mode = Batch then NONE else SOME (name, K ss)
    80   | dynamic_entry_for_info incremental
    81         (name, Internal (JNI from_version, mode, ss)) =
    82     if (incremental andalso mode = Batch) orelse
    83        dict_ord int_ord (kodkodi_version (), from_version) = LESS then
    84       NONE
    85     else
    86       let
    87         val lib_paths = getenv "KODKODI_JAVA_LIBRARY_PATH"
    88                         |> space_explode ":"
    89       in
    90         if exists (fn path => File.exists (Path.explode (path ^ "/")))
    91                   lib_paths then
    92           SOME (name, K ss)
    93         else
    94           NONE
    95       end
    96   | dynamic_entry_for_info false (name, External (home, exec, args)) =
    97     dynamic_entry_for_external name ToStdout home exec args []
    98   | dynamic_entry_for_info false
    99         (name, ExternalV2 (dev, home, exec, args, m1, m2, m3)) =
   100     dynamic_entry_for_external name dev home exec args [m1, m2, m3]
   101   | dynamic_entry_for_info true _ = NONE
   102 
   103 fun dynamic_list incremental =
   104   map_filter (dynamic_entry_for_info incremental) static_list
   105 
   106 val configured_sat_solvers = map fst o dynamic_list
   107 val smart_sat_solver_name = fst o hd o dynamic_list
   108 
   109 fun sat_solver_spec name =
   110   let
   111     val dyns = dynamic_list false
   112     fun enum_solvers solvers =
   113       commas (distinct (op =) (map (quote o fst) solvers))
   114   in
   115     (name, the (AList.lookup (op =) dyns name) ())
   116     handle Option.Option =>
   117            error (if AList.defined (op =) static_list name then
   118                     "The SAT solver " ^ quote name ^ " is not configured. The \
   119                     \following solvers are configured:\n" ^
   120                     enum_solvers dyns
   121                   else
   122                     "Unknown SAT solver " ^ quote name ^ "\nThe following \
   123                     \solvers are supported:\n" ^ enum_solvers static_list)
   124   end
   125 
   126 end;