added Riss3g
authorblanchet
Thu, 28 Nov 2013 15:14:00 +0100
changeset 5598148dadf69c44d
parent 55980 a8ad7f6dd217
child 55982 c71eb0537d37
added Riss3g
src/HOL/Tools/Nitpick/kodkod_sat.ML
     1.1 --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Thu Nov 28 13:58:12 2013 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Thu Nov 28 15:14:00 2013 +0100
     1.3 @@ -31,7 +31,6 @@
     1.4  (* for compatibility with "SatSolver" *)
     1.5  val berkmin_exec = getenv "BERKMIN_EXE"
     1.6  
     1.7 -(* (string * sat_solver_info) list *)
     1.8  val static_list =
     1.9    [("Lingeling_JNI", Internal (JNI [1, 5], Batch, ["Lingeling"])),
    1.10     ("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
    1.11 @@ -44,6 +43,7 @@
    1.12                            "Instance Unsatisfiable")),
    1.13     ("RSat", ExternalV2 (ToStdout, "RSAT_HOME", "rsat", ["-s"],
    1.14                          "s SATISFIABLE", "v ", "s UNSATISFIABLE")),
    1.15 +   ("Riss3g", External ("RISS3G_HOME", "riss3g", [])),
    1.16     ("BerkMin", ExternalV2 (ToStdout, "BERKMIN_HOME",
    1.17                             if berkmin_exec = "" then "BerkMin561"
    1.18                             else berkmin_exec, [], "Satisfiable          !!",