src/HOL/Tools/Nitpick/kodkod_sat.ML
author haftmann
Sun, 23 Feb 2014 10:33:43 +0100
changeset 55684 ee49b4f7edc8
parent 54608 48dadf69c44d
child 55889 6bfbec3dff62
permissions -rw-r--r--
keep only identifiers public which are explicitly requested or demanded by dependencies
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33982
1ae222745c4a fixed paths in Nitpick's ML file headers
blanchet
parents: 33731
diff changeset
     1
(*  Title:      HOL/Tools/Nitpick/kodkod_sat.ML
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 33982
diff changeset
     3
    Copyright   2009, 2010
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     4
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     5
Kodkod SAT solver integration.
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     6
*)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     7
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     8
signature KODKOD_SAT =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     9
sig
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    10
  val configured_sat_solvers : bool -> string list
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    11
  val smart_sat_solver_name : bool -> string
35177
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
    12
  val sat_solver_spec : string -> string * string list
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    13
end;
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    14
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33229
diff changeset
    15
structure Kodkod_SAT : KODKOD_SAT =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    16
struct
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    17
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
    18
open Kodkod
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
    19
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    20
datatype sink = ToStdout | ToFile
50488
1b3eb579e08b use modern SAT solvers with modern Kodkod versions
blanchet
parents: 45085
diff changeset
    21
datatype availability =
1b3eb579e08b use modern SAT solvers with modern Kodkod versions
blanchet
parents: 45085
diff changeset
    22
  Java |
1b3eb579e08b use modern SAT solvers with modern Kodkod versions
blanchet
parents: 45085
diff changeset
    23
  JNI of int list
33229
fba7527c3ef1 made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
blanchet
parents: 33192
diff changeset
    24
datatype mode = Batch | Incremental
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    25
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    26
datatype sat_solver_info =
33229
fba7527c3ef1 made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
blanchet
parents: 33192
diff changeset
    27
  Internal of availability * mode * string list |
45077
3cb902212af5 update list of SAT solvers reflecting Kodkod 1.5
blanchet
parents: 39221
diff changeset
    28
  External of string * string * string list |
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    29
  ExternalV2 of sink * string * string * string list * string * string * string
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    30
38125
b178a63df952 change the order of the SAT solvers, from fastest to slowest
blanchet
parents: 38122
diff changeset
    31
(* for compatibility with "SatSolver" *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    32
val berkmin_exec = getenv "BERKMIN_EXE"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    33
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    34
val static_list =
50488
1b3eb579e08b use modern SAT solvers with modern Kodkod versions
blanchet
parents: 45085
diff changeset
    35
  [("Lingeling_JNI", Internal (JNI [1, 5], Batch, ["Lingeling"])),
1b3eb579e08b use modern SAT solvers with modern Kodkod versions
blanchet
parents: 45085
diff changeset
    36
   ("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
1b3eb579e08b use modern SAT solvers with modern Kodkod versions
blanchet
parents: 45085
diff changeset
    37
   ("CryptoMiniSat_JNI", Internal (JNI [1, 5], Batch, ["CryptoMiniSat"])),
1b3eb579e08b use modern SAT solvers with modern Kodkod versions
blanchet
parents: 45085
diff changeset
    38
   ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
45085
eb7a797ade0f put MiniSat back first -- Torlak's eval seemed to suggest that Crypto and Lingeling were better, but Crypto is slower on "Nitpick_Examples" and Crypto crashes
blanchet
parents: 45083
diff changeset
    39
                           "UNSAT")),
50488
1b3eb579e08b use modern SAT solvers with modern Kodkod versions
blanchet
parents: 45085
diff changeset
    40
   ("MiniSat_JNI", Internal (JNI [], Incremental, ["MiniSat"])),
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    41
   ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    42
                          "Instance Satisfiable", "",
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    43
                          "Instance Unsatisfiable")),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    44
   ("RSat", ExternalV2 (ToStdout, "RSAT_HOME", "rsat", ["-s"],
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    45
                        "s SATISFIABLE", "v ", "s UNSATISFIABLE")),
54608
48dadf69c44d added Riss3g
blanchet
parents: 50489
diff changeset
    46
   ("Riss3g", External ("RISS3G_HOME", "riss3g", [])),
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    47
   ("BerkMin", ExternalV2 (ToStdout, "BERKMIN_HOME",
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    48
                           if berkmin_exec = "" then "BerkMin561"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    49
                           else berkmin_exec, [], "Satisfiable          !!",
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    50
                           "solution =", "UNSATISFIABLE          !!")),
45077
3cb902212af5 update list of SAT solvers reflecting Kodkod 1.5
blanchet
parents: 39221
diff changeset
    51
   ("BerkMin_Alloy", External ("BERKMINALLOY_HOME", "berkmin", [])),
33229
fba7527c3ef1 made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
blanchet
parents: 33192
diff changeset
    52
   ("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
36923
538cf3fdfe4d remove support for crashing beta solver HaifaSat
blanchet
parents: 36385
diff changeset
    53
   ("SAT4J_Light", Internal (Java, Incremental, ["LightSAT4J"]))]
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    54
35177
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
    55
fun dynamic_entry_for_external name dev home exec args markers =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    56
  case getenv home of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    57
    "" => NONE
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
    58
  | dir =>
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
    59
    SOME (name, fn () =>
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
    60
                   let
35177
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
    61
                     val serial_str = serial_string ()
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
    62
                     val base = name ^ serial_str
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
    63
                     val out_file = base ^ ".out"
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
    64
                     val dir_sep =
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
    65
                       if String.isSubstring "\\" dir andalso
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
    66
                          not (String.isSubstring "/" dir) then
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
    67
                         "\\"
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
    68
                       else
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
    69
                         "/"
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
    70
                   in
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
    71
                     [if null markers then "External" else "ExternalV2",
45077
3cb902212af5 update list of SAT solvers reflecting Kodkod 1.5
blanchet
parents: 39221
diff changeset
    72
                      dir ^ dir_sep ^ exec, base ^ ".cnf"] @
3cb902212af5 update list of SAT solvers reflecting Kodkod 1.5
blanchet
parents: 39221
diff changeset
    73
                      (if null markers then []
3cb902212af5 update list of SAT solvers reflecting Kodkod 1.5
blanchet
parents: 39221
diff changeset
    74
                       else [if dev = ToFile then out_file else ""]) @ markers @
39221
70fd4a3c41ed remove "minipick" (the toy version of Nitpick) and some tests;
blanchet
parents: 38125
diff changeset
    75
                     (if dev = ToFile then [out_file] else []) @ args
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
    76
                   end)
35177
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
    77
fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
33229
fba7527c3ef1 made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
blanchet
parents: 33192
diff changeset
    78
    if incremental andalso mode = Batch then NONE else SOME (name, K ss)
50488
1b3eb579e08b use modern SAT solvers with modern Kodkod versions
blanchet
parents: 45085
diff changeset
    79
  | dynamic_entry_for_info incremental
1b3eb579e08b use modern SAT solvers with modern Kodkod versions
blanchet
parents: 45085
diff changeset
    80
        (name, Internal (JNI from_version, mode, ss)) =
1b3eb579e08b use modern SAT solvers with modern Kodkod versions
blanchet
parents: 45085
diff changeset
    81
    if (incremental andalso mode = Batch) orelse
1b3eb579e08b use modern SAT solvers with modern Kodkod versions
blanchet
parents: 45085
diff changeset
    82
       dict_ord int_ord (kodkodi_version (), from_version) = LESS then
33229
fba7527c3ef1 made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
blanchet
parents: 33192
diff changeset
    83
      NONE
fba7527c3ef1 made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
blanchet
parents: 33192
diff changeset
    84
    else
fba7527c3ef1 made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
blanchet
parents: 33192
diff changeset
    85
      let
fba7527c3ef1 made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
blanchet
parents: 33192
diff changeset
    86
        val lib_paths = getenv "KODKODI_JAVA_LIBRARY_PATH"
fba7527c3ef1 made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
blanchet
parents: 33192
diff changeset
    87
                        |> space_explode ":"
fba7527c3ef1 made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
blanchet
parents: 33192
diff changeset
    88
      in
fba7527c3ef1 made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
blanchet
parents: 33192
diff changeset
    89
        if exists (fn path => File.exists (Path.explode (path ^ "/")))
fba7527c3ef1 made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
blanchet
parents: 33192
diff changeset
    90
                  lib_paths then
fba7527c3ef1 made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
blanchet
parents: 33192
diff changeset
    91
          SOME (name, K ss)
fba7527c3ef1 made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
blanchet
parents: 33192
diff changeset
    92
        else
fba7527c3ef1 made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
blanchet
parents: 33192
diff changeset
    93
          NONE
fba7527c3ef1 made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
blanchet
parents: 33192
diff changeset
    94
      end
45077
3cb902212af5 update list of SAT solvers reflecting Kodkod 1.5
blanchet
parents: 39221
diff changeset
    95
  | dynamic_entry_for_info false (name, External (home, exec, args)) =
3cb902212af5 update list of SAT solvers reflecting Kodkod 1.5
blanchet
parents: 39221
diff changeset
    96
    dynamic_entry_for_external name ToStdout home exec args []
35177
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
    97
  | dynamic_entry_for_info false
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
    98
        (name, ExternalV2 (dev, home, exec, args, m1, m2, m3)) =
35177
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
    99
    dynamic_entry_for_external name dev home exec args [m1, m2, m3]
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   100
  | dynamic_entry_for_info true _ = NONE
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   101
fun dynamic_list incremental =
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   102
  map_filter (dynamic_entry_for_info incremental) static_list
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   103
35177
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   104
val configured_sat_solvers = map fst o dynamic_list
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   105
val smart_sat_solver_name = fst o hd o dynamic_list
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   106
35177
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   107
fun sat_solver_spec name =
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   108
  let
50489
blanchet
parents: 50488
diff changeset
   109
    val dyns = dynamic_list false
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   110
    fun enum_solvers solvers =
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   111
      commas (distinct (op =) (map (quote o fst) solvers))
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   112
  in
50489
blanchet
parents: 50488
diff changeset
   113
    (name, the (AList.lookup (op =) dyns name) ())
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   114
    handle Option.Option =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   115
           error (if AList.defined (op =) static_list name then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   116
                    "The SAT solver " ^ quote name ^ " is not configured. The \
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   117
                    \following solvers are configured:\n" ^
50489
blanchet
parents: 50488
diff changeset
   118
                    enum_solvers dyns ^ "."
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   119
                  else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   120
                    "Unknown SAT solver " ^ quote name ^ ". The following \
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   121
                    \solvers are supported:\n" ^ enum_solvers static_list ^ ".")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   122
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   123
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   124
end;