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
authorblanchet
Mon, 26 Sep 2011 14:03:43 +0200
changeset 45085 eb7a797ade0f
parent 45084 91d1a932fc18
child 45086 3933a0cbd049
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
src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Mon Sep 26 11:41:52 2011 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Mon Sep 26 14:03:43 2011 +0200
@@ -31,12 +31,12 @@
 
 (* (string * sat_solver_info) list *)
 val static_list =
-  [("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
+  [("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
+                           "UNSAT")),
+   ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
+   ("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
    ("CryptoMiniSat_JNI", Internal (JNI, Batch, ["CryptoMiniSat"])),
    ("Lingeling_JNI", Internal (JNI, Batch, ["Lingeling"])),
-   ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
-                           "UNSAT")),
-   ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
    ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
                           "Instance Satisfiable", "",
                           "Instance Unsatisfiable")),