1 (* Title: HOL/Nunchaku/Tools/nunchaku_tool.ML |
|
2 Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII |
|
3 Copyright 2015, 2016 |
|
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 = |
|
15 {solvers: string list, |
|
16 overlord: bool, |
|
17 debug: bool, |
|
18 specialize: bool, |
|
19 timeout: Time.time} |
|
20 |
|
21 type nun_solution = |
|
22 {tys: (ty * tm list) list, |
|
23 tms: (tm * tm) list} |
|
24 |
|
25 datatype nun_outcome = |
|
26 Unsat |
|
27 | Sat of string * nun_solution |
|
28 | Unknown of (string * nun_solution) option |
|
29 | Timeout |
|
30 | Nunchaku_Var_Not_Set |
|
31 | Nunchaku_Cannot_Execute |
|
32 | Nunchaku_Not_Found |
|
33 | CVC4_Cannot_Execute |
|
34 | CVC4_Not_Found |
|
35 | Unknown_Error of int * string |
|
36 |
|
37 val nunchaku_home_env_var: string |
|
38 |
|
39 val solve_nun_problem: tool_params -> nun_problem -> nun_outcome |
|
40 end; |
|
41 |
|
42 structure Nunchaku_Tool : NUNCHAKU_TOOL = |
|
43 struct |
|
44 |
|
45 open Nunchaku_Util; |
|
46 open Nunchaku_Problem; |
|
47 |
|
48 type tool_params = |
|
49 {solvers: string list, |
|
50 overlord: bool, |
|
51 debug: bool, |
|
52 specialize: bool, |
|
53 timeout: Time.time}; |
|
54 |
|
55 type nun_solution = |
|
56 {tys: (ty * tm list) list, |
|
57 tms: (tm * tm) list}; |
|
58 |
|
59 datatype nun_outcome = |
|
60 Unsat |
|
61 | Sat of string * nun_solution |
|
62 | Unknown of (string * nun_solution) option |
|
63 | Timeout |
|
64 | Nunchaku_Var_Not_Set |
|
65 | Nunchaku_Cannot_Execute |
|
66 | Nunchaku_Not_Found |
|
67 | CVC4_Cannot_Execute |
|
68 | CVC4_Not_Found |
|
69 | Unknown_Error of int * string; |
|
70 |
|
71 fun bash_output_error s = |
|
72 let val {out, err, rc, ...} = Bash.process s in |
|
73 ((out, err), rc) |
|
74 end; |
|
75 |
|
76 val nunchaku_home_env_var = "NUNCHAKU_HOME"; |
|
77 |
|
78 val cached_outcome = Synchronized.var "Nunchaku_Tool.cached_outcome" |
|
79 (NONE : ((string list * nun_problem) * nun_outcome) option); |
|
80 |
|
81 fun uncached_solve_nun_problem ({solvers, overlord, specialize, timeout, ...} : tool_params) |
|
82 (problem as {sound, complete, ...}) = |
|
83 with_tmp_or_overlord_file overlord "nunchaku" "nun" (fn prob_path => |
|
84 if getenv nunchaku_home_env_var = "" then |
|
85 Nunchaku_Var_Not_Set |
|
86 else |
|
87 let |
|
88 val bash_cmd = |
|
89 "PATH=\"$CVC4_HOME:$KODKODI/bin:$PATH\" \"$" ^ |
|
90 nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^ |
|
91 (if specialize then "" else "--no-specialize ") ^ |
|
92 "--solvers \"" ^ Bash_Syntax.string (space_implode " " solvers) ^ "\" " ^ |
|
93 "--timeout " ^ string_of_int (Time.toSeconds timeout) ^ " " ^ |
|
94 File.bash_path prob_path; |
|
95 val comments = |
|
96 [bash_cmd, "This file was generated by Isabelle (most likely Nunchaku)", timestamp ()]; |
|
97 val prob_str = cat_lines (map (prefix "# ") comments) ^ "\n\n" ^ str_of_nun_problem problem; |
|
98 val _ = File.write prob_path prob_str; |
|
99 val ((output, error), code) = bash_output_error bash_cmd; |
|
100 in |
|
101 if String.isPrefix "SAT" output then |
|
102 (if sound then Sat else Unknown o SOME) (output, {tys = [], tms = []}) |
|
103 else if String.isPrefix "UNSAT" output then |
|
104 if complete then Unsat else Unknown NONE |
|
105 else if String.isSubstring "TIMEOUT" output |
|
106 (* FIXME: temporary *) |
|
107 orelse String.isSubstring "kodkod failed (errcode 152)" error then |
|
108 Timeout |
|
109 else if String.isPrefix "UNKNOWN" output then |
|
110 Unknown NONE |
|
111 else if code = 126 then |
|
112 Nunchaku_Cannot_Execute |
|
113 else if code = 127 then |
|
114 Nunchaku_Not_Found |
|
115 else |
|
116 Unknown_Error (code, |
|
117 simplify_spaces (elide_string 1000 (if error <> "" then error else output))) |
|
118 end); |
|
119 |
|
120 fun solve_nun_problem (params as {solvers, overlord, debug, ...}) problem = |
|
121 let val key = (solvers, problem) in |
|
122 (case (overlord orelse debug, |
|
123 AList.lookup (op =) (the_list (Synchronized.value cached_outcome)) key) of |
|
124 (false, SOME outcome) => outcome |
|
125 | _ => |
|
126 let |
|
127 val outcome = uncached_solve_nun_problem params problem; |
|
128 |
|
129 fun update_cache () = |
|
130 Synchronized.change cached_outcome (K (SOME (key, outcome))); |
|
131 in |
|
132 (case outcome of |
|
133 Unsat => update_cache () |
|
134 | Sat _ => update_cache () |
|
135 | Unknown _ => update_cache () |
|
136 | _ => ()); |
|
137 outcome |
|
138 end) |
|
139 end; |
|
140 |
|
141 end; |
|