author | wenzelm |
Mon, 22 Feb 2021 14:48:03 +0100 | |
changeset 73275 | f0db1e4c89bc |
parent 73274 | 10d3b49a702a |
child 74142 | 0f051404f487 |
permissions | -rw-r--r-- |
66646 | 1 |
(* Title: HOL/Tools/Nunchaku/nunchaku_tool.ML |
66614
1f1c5d85d232
moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years
blanchet
parents:
66163
diff
changeset
|
2 |
Author: Jasmin Blanchette, VU Amsterdam |
1f1c5d85d232
moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years
blanchet
parents:
66163
diff
changeset
|
3 |
Copyright 2015, 2016, 2017 |
64389 | 4 |
|
5 |
Interface to the external "nunchaku" tool. |
|
6 |
*) |
|
7 |
||
8 |
signature NUNCHAKU_TOOL = |
|
9 |
sig |
|
10 |
type ty = Nunchaku_Problem.ty |
|
11 |
type tm = Nunchaku_Problem.tm |
|
12 |
type nun_problem = Nunchaku_Problem.nun_problem |
|
13 |
||
14 |
type tool_params = |
|
66163 | 15 |
{solvers: string list, |
16 |
overlord: bool, |
|
66627 | 17 |
min_bound: int, |
18 |
max_bound: int option, |
|
66625 | 19 |
bound_increment: int, |
64389 | 20 |
debug: bool, |
21 |
specialize: bool, |
|
22 |
timeout: Time.time} |
|
23 |
||
24 |
type nun_solution = |
|
25 |
{tys: (ty * tm list) list, |
|
26 |
tms: (tm * tm) list} |
|
27 |
||
28 |
datatype nun_outcome = |
|
66620 | 29 |
Unsat of string |
30 |
| Sat of string * string * nun_solution |
|
31 |
| Unknown of (string * string * nun_solution) option |
|
64389 | 32 |
| Timeout |
33 |
| Nunchaku_Var_Not_Set |
|
34 |
| Nunchaku_Cannot_Execute |
|
35 |
| Nunchaku_Not_Found |
|
36 |
| CVC4_Cannot_Execute |
|
37 |
| CVC4_Not_Found |
|
38 |
| Unknown_Error of int * string |
|
39 |
||
64469
488d4e627238
added Nunchaku component and tuned Nunchaku integration accordingly
blanchet
parents:
64407
diff
changeset
|
40 |
val nunchaku_home_env_var: string |
64389 | 41 |
|
42 |
val solve_nun_problem: tool_params -> nun_problem -> nun_outcome |
|
43 |
end; |
|
44 |
||
45 |
structure Nunchaku_Tool : NUNCHAKU_TOOL = |
|
46 |
struct |
|
47 |
||
48 |
open Nunchaku_Util; |
|
49 |
open Nunchaku_Problem; |
|
50 |
||
51 |
type tool_params = |
|
66163 | 52 |
{solvers: string list, |
53 |
overlord: bool, |
|
66627 | 54 |
min_bound: int, |
55 |
max_bound: int option, |
|
66625 | 56 |
bound_increment: int, |
64389 | 57 |
debug: bool, |
58 |
specialize: bool, |
|
59 |
timeout: Time.time}; |
|
60 |
||
61 |
type nun_solution = |
|
62 |
{tys: (ty * tm list) list, |
|
63 |
tms: (tm * tm) list}; |
|
64 |
||
65 |
datatype nun_outcome = |
|
66620 | 66 |
Unsat of string |
67 |
| Sat of string * string * nun_solution |
|
68 |
| Unknown of (string * string * nun_solution) option |
|
64389 | 69 |
| Timeout |
70 |
| Nunchaku_Var_Not_Set |
|
71 |
| Nunchaku_Cannot_Execute |
|
72 |
| Nunchaku_Not_Found |
|
73 |
| CVC4_Cannot_Execute |
|
74 |
| CVC4_Not_Found |
|
75 |
| Unknown_Error of int * string; |
|
76 |
||
64469
488d4e627238
added Nunchaku component and tuned Nunchaku integration accordingly
blanchet
parents:
64407
diff
changeset
|
77 |
val nunchaku_home_env_var = "NUNCHAKU_HOME"; |
64389 | 78 |
|
66620 | 79 |
val unknown_solver = "unknown"; |
80 |
||
66163 | 81 |
val cached_outcome = Synchronized.var "Nunchaku_Tool.cached_outcome" |
66626 | 82 |
(NONE : ((tool_params * nun_problem) * nun_outcome) option); |
64389 | 83 |
|
66627 | 84 |
fun uncached_solve_nun_problem ({solvers, overlord, min_bound, max_bound, bound_increment, |
85 |
specialize, timeout, ...} : tool_params) |
|
64389 | 86 |
(problem as {sound, complete, ...}) = |
87 |
with_tmp_or_overlord_file overlord "nunchaku" "nun" (fn prob_path => |
|
64469
488d4e627238
added Nunchaku component and tuned Nunchaku integration accordingly
blanchet
parents:
64407
diff
changeset
|
88 |
if getenv nunchaku_home_env_var = "" then |
64389 | 89 |
Nunchaku_Var_Not_Set |
90 |
else |
|
91 |
let |
|
92 |
val bash_cmd = |
|
66637 | 93 |
"PATH=\"$CVC4_HOME:$KODKODI/bin:$SMBC_HOME:$PATH\" \"$" ^ |
64469
488d4e627238
added Nunchaku component and tuned Nunchaku integration accordingly
blanchet
parents:
64407
diff
changeset
|
94 |
nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^ |
64389 | 95 |
(if specialize then "" else "--no-specialize ") ^ |
67106 | 96 |
"--solvers \"" ^ space_implode "," (map Bash.string solvers) ^ "\" " ^ |
64389 | 97 |
"--timeout " ^ string_of_int (Time.toSeconds timeout) ^ " " ^ |
66627 | 98 |
"--kodkod-min-bound " ^ string_of_int min_bound ^ " " ^ |
99 |
(case max_bound of NONE => "" | SOME n => "--kodkod-max-bound " ^ string_of_int n ^ " ") ^ |
|
100 |
"--kodkod-bound-increment " ^ string_of_int bound_increment ^ " " ^ |
|
64389 | 101 |
File.bash_path prob_path; |
102 |
val comments = |
|
103 |
[bash_cmd, "This file was generated by Isabelle (most likely Nunchaku)", timestamp ()]; |
|
104 |
val prob_str = cat_lines (map (prefix "# ") comments) ^ "\n\n" ^ str_of_nun_problem problem; |
|
105 |
val _ = File.write prob_path prob_str; |
|
73275 | 106 |
val res = Isabelle_System.bash_process bash_cmd; |
107 |
val rc = Process_Result.rc res; |
|
108 |
val out = Process_Result.out res; |
|
109 |
val err = Process_Result.err res; |
|
66620 | 110 |
|
111 |
val backend = |
|
73274 | 112 |
(case map_filter (try (unprefix "{backend:")) (split_lines out) of |
66638 | 113 |
[s] => hd (space_explode "," s) |
114 |
| _ => unknown_solver); |
|
64389 | 115 |
in |
73274 | 116 |
if String.isPrefix "SAT" out then |
117 |
(if sound then Sat else Unknown o SOME) (backend, out, {tys = [], tms = []}) |
|
118 |
else if String.isPrefix "UNSAT" out then |
|
66620 | 119 |
if complete then Unsat backend else Unknown NONE |
73274 | 120 |
else if String.isSubstring "TIMEOUT" out |
64469
488d4e627238
added Nunchaku component and tuned Nunchaku integration accordingly
blanchet
parents:
64407
diff
changeset
|
121 |
(* FIXME: temporary *) |
73274 | 122 |
orelse String.isSubstring "kodkod failed (errcode 152)" err then |
64469
488d4e627238
added Nunchaku component and tuned Nunchaku integration accordingly
blanchet
parents:
64407
diff
changeset
|
123 |
Timeout |
73274 | 124 |
else if String.isPrefix "UNKNOWN" out then |
64389 | 125 |
Unknown NONE |
73274 | 126 |
else if rc = 126 then |
64389 | 127 |
Nunchaku_Cannot_Execute |
73274 | 128 |
else if rc = 127 then |
64389 | 129 |
Nunchaku_Not_Found |
130 |
else |
|
73274 | 131 |
Unknown_Error (rc, |
132 |
simplify_spaces (elide_string 1000 (if err <> "" then err else out))) |
|
64389 | 133 |
end); |
134 |
||
66163 | 135 |
fun solve_nun_problem (params as {solvers, overlord, debug, ...}) problem = |
66626 | 136 |
let val key = (params, problem) in |
66163 | 137 |
(case (overlord orelse debug, |
138 |
AList.lookup (op =) (the_list (Synchronized.value cached_outcome)) key) of |
|
139 |
(false, SOME outcome) => outcome |
|
140 |
| _ => |
|
141 |
let |
|
142 |
val outcome = uncached_solve_nun_problem params problem; |
|
64389 | 143 |
|
66163 | 144 |
fun update_cache () = |
145 |
Synchronized.change cached_outcome (K (SOME (key, outcome))); |
|
146 |
in |
|
147 |
(case outcome of |
|
66620 | 148 |
Unsat _ => update_cache () |
66163 | 149 |
| Sat _ => update_cache () |
150 |
| Unknown _ => update_cache () |
|
151 |
| _ => ()); |
|
152 |
outcome |
|
153 |
end) |
|
154 |
end; |
|
64389 | 155 |
|
156 |
end; |