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