14 |
14 |
15 structure KodkodSAT : KODKOD_SAT = |
15 structure KodkodSAT : KODKOD_SAT = |
16 struct |
16 struct |
17 |
17 |
18 datatype sink = ToStdout | ToFile |
18 datatype sink = ToStdout | ToFile |
|
19 datatype availability = Java | JNI |
|
20 datatype mode = Batch | Incremental |
19 |
21 |
20 datatype sat_solver_info = |
22 datatype sat_solver_info = |
21 Internal of bool * string list | |
23 Internal of availability * mode * string list | |
22 External of sink * string * string * string list | |
24 External of sink * string * string * string list | |
23 ExternalV2 of sink * string * string * string list * string * string * string |
25 ExternalV2 of sink * string * string * string list * string * string * string |
24 |
26 |
25 val berkmin_exec = getenv "BERKMIN_EXE" |
27 val berkmin_exec = getenv "BERKMIN_EXE" |
26 |
28 |
27 (* (string * sat_solver_info) list *) |
29 (* (string * sat_solver_info) list *) |
28 val static_list = |
30 val static_list = |
29 [("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "", |
31 [("MiniSatJNI", Internal (JNI, Incremental, ["MiniSat"])), |
|
32 ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "", |
30 "UNSAT")), |
33 "UNSAT")), |
31 ("PicoSAT", External (ToStdout, "PICOSAT_HOME", "picosat", [])), |
34 ("PicoSAT", External (ToStdout, "PICOSAT_HOME", "picosat", [])), |
|
35 ("zChaffJNI", Internal (JNI, Batch, ["zChaff"])), |
32 ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [], |
36 ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [], |
33 "Instance Satisfiable", "", |
37 "Instance Satisfiable", "", |
34 "Instance Unsatisfiable")), |
38 "Instance Unsatisfiable")), |
35 ("RSat", ExternalV2 (ToStdout, "RSAT_HOME", "rsat", ["-s"], |
39 ("RSat", ExternalV2 (ToStdout, "RSAT_HOME", "rsat", ["-s"], |
36 "s SATISFIABLE", "v ", "s UNSATISFIABLE")), |
40 "s SATISFIABLE", "v ", "s UNSATISFIABLE")), |
38 if berkmin_exec = "" then "BerkMin561" |
42 if berkmin_exec = "" then "BerkMin561" |
39 else berkmin_exec, [], "Satisfiable !!", |
43 else berkmin_exec, [], "Satisfiable !!", |
40 "solution =", "UNSATISFIABLE !!")), |
44 "solution =", "UNSATISFIABLE !!")), |
41 ("BerkMinAlloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])), |
45 ("BerkMinAlloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])), |
42 ("Jerusat", External (ToStdout, "JERUSAT_HOME", "Jerusat1.3", [])), |
46 ("Jerusat", External (ToStdout, "JERUSAT_HOME", "Jerusat1.3", [])), |
43 ("SAT4J", Internal (true, ["DefaultSAT4J"])), |
47 ("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])), |
44 ("MiniSatJNI", Internal (true, ["MiniSat"])), |
48 ("SAT4JLight", Internal (Java, Incremental, ["LightSAT4J"])), |
45 ("zChaffJNI", Internal (false, ["zChaff"])), |
|
46 ("SAT4JLight", Internal (true, ["LightSAT4J"])), |
|
47 ("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"], |
49 ("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"], |
48 "s SATISFIABLE", "v ", "s UNSATISFIABLE"))] |
50 "s SATISFIABLE", "v ", "s UNSATISFIABLE"))] |
49 |
51 |
50 val created_temp_dir = Unsynchronized.ref false |
52 val created_temp_dir = Unsynchronized.ref false |
51 |
53 |
70 if dev = ToFile then out_file else ""] @ markers @ |
72 if dev = ToFile then out_file else ""] @ markers @ |
71 (if dev = ToFile then [out_file] else []) @ args |
73 (if dev = ToFile then [out_file] else []) @ args |
72 end) |
74 end) |
73 (* bool -> string * sat_solver_info |
75 (* bool -> string * sat_solver_info |
74 -> (string * (unit -> string list)) option *) |
76 -> (string * (unit -> string list)) option *) |
75 fun dynamic_entry_for_info false (name, Internal (_, ss)) = SOME (name, K ss) |
77 fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) = |
|
78 if incremental andalso mode = Batch then NONE else SOME (name, K ss) |
|
79 | dynamic_entry_for_info incremental (name, Internal (JNI, mode, ss)) = |
|
80 if incremental andalso mode = Batch then |
|
81 NONE |
|
82 else |
|
83 let |
|
84 val lib_paths = getenv "KODKODI_JAVA_LIBRARY_PATH" |
|
85 |> space_explode ":" |
|
86 in |
|
87 if exists (fn path => File.exists (Path.explode (path ^ "/"))) |
|
88 lib_paths then |
|
89 SOME (name, K ss) |
|
90 else |
|
91 NONE |
|
92 end |
76 | dynamic_entry_for_info false (name, External (dev, home, exec, args)) = |
93 | dynamic_entry_for_info false (name, External (dev, home, exec, args)) = |
77 dynamic_entry_for_external name dev home exec args [] |
94 dynamic_entry_for_external name dev home exec args [] |
78 | dynamic_entry_for_info false (name, ExternalV2 (dev, home, exec, args, |
95 | dynamic_entry_for_info false (name, ExternalV2 (dev, home, exec, args, |
79 m1, m2, m3)) = |
96 m1, m2, m3)) = |
80 dynamic_entry_for_external name dev home exec args [m1, m2, m3] |
97 dynamic_entry_for_external name dev home exec args [m1, m2, m3] |
81 | dynamic_entry_for_info true (name, Internal (true, ss)) = SOME (name, K ss) |
|
82 | dynamic_entry_for_info true _ = NONE |
98 | dynamic_entry_for_info true _ = NONE |
83 (* bool -> (string * (unit -> string list)) list *) |
99 (* bool -> (string * (unit -> string list)) list *) |
84 fun dynamic_list incremental = |
100 fun dynamic_list incremental = |
85 map_filter (dynamic_entry_for_info incremental) static_list |
101 map_filter (dynamic_entry_for_info incremental) static_list |
86 |
102 |