author | blanchet |
Fri, 08 Sep 2017 00:01:52 +0200 | |
changeset 66615 | 7706577cd10e |
parent 66614 | 1f1c5d85d232 |
child 66620 | 984c179a00d3 |
permissions | -rw-r--r-- |
64389 | 1 |
(* Title: HOL/Nunchaku/Tools/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, |
|
64389 | 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 |
||
64469
488d4e627238
added Nunchaku component and tuned Nunchaku integration accordingly
blanchet
parents:
64407
diff
changeset
|
37 |
val nunchaku_home_env_var: string |
64389 | 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 = |
|
66163 | 49 |
{solvers: string list, |
50 |
overlord: bool, |
|
64389 | 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 |
||
64469
488d4e627238
added Nunchaku component and tuned Nunchaku integration accordingly
blanchet
parents:
64407
diff
changeset
|
76 |
val nunchaku_home_env_var = "NUNCHAKU_HOME"; |
64389 | 77 |
|
66163 | 78 |
val cached_outcome = Synchronized.var "Nunchaku_Tool.cached_outcome" |
79 |
(NONE : ((string list * nun_problem) * nun_outcome) option); |
|
64389 | 80 |
|
66163 | 81 |
fun uncached_solve_nun_problem ({solvers, overlord, specialize, timeout, ...} : tool_params) |
64389 | 82 |
(problem as {sound, complete, ...}) = |
83 |
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
|
84 |
if getenv nunchaku_home_env_var = "" then |
64389 | 85 |
Nunchaku_Var_Not_Set |
86 |
else |
|
87 |
let |
|
88 |
val bash_cmd = |
|
64469
488d4e627238
added Nunchaku component and tuned Nunchaku integration accordingly
blanchet
parents:
64407
diff
changeset
|
89 |
"PATH=\"$CVC4_HOME:$KODKODI/bin:$PATH\" \"$" ^ |
488d4e627238
added Nunchaku component and tuned Nunchaku integration accordingly
blanchet
parents:
64407
diff
changeset
|
90 |
nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^ |
64389 | 91 |
(if specialize then "" else "--no-specialize ") ^ |
66615 | 92 |
"--solvers \"" ^ Bash_Syntax.string (space_implode "," solvers) ^ "\" " ^ |
64389 | 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 |
|
64469
488d4e627238
added Nunchaku component and tuned Nunchaku integration accordingly
blanchet
parents:
64407
diff
changeset
|
105 |
else if String.isSubstring "TIMEOUT" output |
488d4e627238
added Nunchaku component and tuned Nunchaku integration accordingly
blanchet
parents:
64407
diff
changeset
|
106 |
(* FIXME: temporary *) |
488d4e627238
added Nunchaku component and tuned Nunchaku integration accordingly
blanchet
parents:
64407
diff
changeset
|
107 |
orelse String.isSubstring "kodkod failed (errcode 152)" error then |
488d4e627238
added Nunchaku component and tuned Nunchaku integration accordingly
blanchet
parents:
64407
diff
changeset
|
108 |
Timeout |
64389 | 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 |
||
66163 | 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; |
|
64389 | 128 |
|
66163 | 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; |
|
64389 | 140 |
|
141 |
end; |