author | wenzelm |
Fri, 05 Mar 2021 17:02:32 +0100 | |
changeset 73386 | 3fb201ca8fb5 |
parent 69597 | ff784d5a5bfb |
child 74383 | 107941e8fa01 |
permissions | -rw-r--r-- |
66646 | 1 |
(* Title: HOL/Tools/Nunchaku/nunchaku.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 |
The core of the Nunchaku integration in Isabelle. |
|
6 |
*) |
|
7 |
||
8 |
signature NUNCHAKU = |
|
9 |
sig |
|
10 |
type isa_model = Nunchaku_Reconstruct.isa_model |
|
11 |
||
12 |
datatype mode = Auto_Try | Try | Normal |
|
13 |
||
14 |
type mode_of_operation_params = |
|
66163 | 15 |
{solvers: string list, |
16 |
falsify: bool, |
|
64389 | 17 |
assms: bool, |
18 |
spy: bool, |
|
19 |
overlord: bool, |
|
20 |
expect: string} |
|
21 |
||
22 |
type scope_of_search_params = |
|
23 |
{wfs: ((string * typ) option * bool option) list, |
|
24 |
whacks: (term option * bool) list, |
|
66627 | 25 |
min_bound: int, |
26 |
max_bound: int option, |
|
66625 | 27 |
bound_increment: int, |
64389 | 28 |
cards: (typ option * (int option * int option)) list, |
29 |
monos: (typ option * bool option) list} |
|
30 |
||
31 |
type output_format_params = |
|
32 |
{verbose: bool, |
|
33 |
debug: bool, |
|
34 |
max_potential: int, |
|
35 |
max_genuine: int, |
|
36 |
evals: term list, |
|
37 |
atomss: (typ option * string list) list} |
|
38 |
||
39 |
type optimization_params = |
|
40 |
{specialize: bool, |
|
41 |
multithread: bool} |
|
42 |
||
43 |
type timeout_params = |
|
44 |
{timeout: Time.time, |
|
45 |
wf_timeout: Time.time} |
|
46 |
||
47 |
type params = |
|
48 |
{mode_of_operation_params: mode_of_operation_params, |
|
49 |
scope_of_search_params: scope_of_search_params, |
|
50 |
output_format_params: output_format_params, |
|
51 |
optimization_params: optimization_params, |
|
52 |
timeout_params: timeout_params} |
|
53 |
||
54 |
val genuineN: string |
|
55 |
val quasi_genuineN: string |
|
56 |
val potentialN: string |
|
57 |
val noneN: string |
|
58 |
val unknownN: string |
|
59 |
val no_nunchakuN: string |
|
60 |
||
61 |
val run_chaku_on_prop: Proof.state -> params -> mode -> int -> term list -> term -> |
|
62 |
string * isa_model option |
|
63 |
val run_chaku_on_subgoal: Proof.state -> params -> mode -> int -> string * isa_model option |
|
64 |
end; |
|
65 |
||
66 |
structure Nunchaku : NUNCHAKU = |
|
67 |
struct |
|
68 |
||
69 |
open Nunchaku_Util; |
|
70 |
open Nunchaku_Collect; |
|
71 |
open Nunchaku_Problem; |
|
72 |
open Nunchaku_Translate; |
|
73 |
open Nunchaku_Model; |
|
74 |
open Nunchaku_Reconstruct; |
|
75 |
open Nunchaku_Display; |
|
76 |
open Nunchaku_Tool; |
|
77 |
||
78 |
datatype mode = Auto_Try | Try | Normal; |
|
79 |
||
80 |
type mode_of_operation_params = |
|
66163 | 81 |
{solvers: string list, |
82 |
falsify: bool, |
|
64389 | 83 |
assms: bool, |
84 |
spy: bool, |
|
85 |
overlord: bool, |
|
86 |
expect: string}; |
|
87 |
||
88 |
type scope_of_search_params = |
|
89 |
{wfs: ((string * typ) option * bool option) list, |
|
90 |
whacks: (term option * bool) list, |
|
66627 | 91 |
min_bound: int, |
92 |
max_bound: int option, |
|
66625 | 93 |
bound_increment: int, |
64389 | 94 |
cards: (typ option * (int option * int option)) list, |
95 |
monos: (typ option * bool option) list}; |
|
96 |
||
97 |
type output_format_params = |
|
98 |
{verbose: bool, |
|
99 |
debug: bool, |
|
100 |
max_potential: int, |
|
101 |
max_genuine: int, |
|
102 |
evals: term list, |
|
103 |
atomss: (typ option * string list) list}; |
|
104 |
||
105 |
type optimization_params = |
|
106 |
{specialize: bool, |
|
107 |
multithread: bool}; |
|
108 |
||
109 |
type timeout_params = |
|
110 |
{timeout: Time.time, |
|
111 |
wf_timeout: Time.time}; |
|
112 |
||
113 |
type params = |
|
114 |
{mode_of_operation_params: mode_of_operation_params, |
|
115 |
scope_of_search_params: scope_of_search_params, |
|
116 |
output_format_params: output_format_params, |
|
117 |
optimization_params: optimization_params, |
|
118 |
timeout_params: timeout_params}; |
|
119 |
||
120 |
val genuineN = "genuine"; |
|
121 |
val quasi_genuineN = "quasi_genuine"; |
|
122 |
val potentialN = "potential"; |
|
123 |
val noneN = "none"; |
|
124 |
val unknownN = "unknown"; |
|
125 |
||
126 |
val no_nunchakuN = "no_nunchaku"; |
|
127 |
||
128 |
fun str_of_mode Auto_Try = "Auto_Try" |
|
129 |
| str_of_mode Try = "Try" |
|
130 |
| str_of_mode Normal = "Normal"; |
|
131 |
||
132 |
fun none_true assigns = forall (curry (op <>) (SOME true) o snd) assigns; |
|
133 |
||
69597 | 134 |
fun has_lonely_bool_var (\<^const>\<open>Pure.conjunction\<close> $ (\<^const>\<open>Trueprop\<close> $ Free _) $ _) = true |
64389 | 135 |
| has_lonely_bool_var _ = false; |
136 |
||
137 |
val syntactic_sorts = |
|
69593 | 138 |
\<^sort>\<open>{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}\<close> @ \<^sort>\<open>numeral\<close>; |
64389 | 139 |
|
140 |
fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) = subset (op =) (S, syntactic_sorts) |
|
141 |
| has_tfree_syntactic_sort _ = false; |
|
142 |
||
143 |
val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort); |
|
144 |
||
66617 | 145 |
val unprefix_error = |
66620 | 146 |
perhaps (try (unprefix "failure: ")) |
147 |
#> perhaps (try (unprefix "Error: ")); |
|
66617 | 148 |
|
64389 | 149 |
(* Give the soft timeout a chance. *) |
150 |
val timeout_slack = seconds 1.0; |
|
151 |
||
152 |
fun run_chaku_on_prop state |
|
66163 | 153 |
({mode_of_operation_params = {solvers, falsify, assms, spy, overlord, expect}, |
66627 | 154 |
scope_of_search_params = {wfs, whacks, min_bound, max_bound, bound_increment, cards, monos}, |
64389 | 155 |
output_format_params = {verbose, debug, evals, atomss, ...}, |
156 |
optimization_params = {specialize, ...}, |
|
157 |
timeout_params = {timeout, wf_timeout}}) |
|
158 |
mode i all_assms subgoal = |
|
159 |
let |
|
160 |
val ctxt = Proof.context_of state; |
|
161 |
||
73386 | 162 |
val time_start = Time.now () |
64389 | 163 |
|
164 |
val print = writeln; |
|
165 |
val print_n = if mode = Normal then writeln else K (); |
|
166 |
fun print_v f = if verbose then writeln (f ()) else (); |
|
167 |
fun print_d f = if debug then writeln (f ()) else (); |
|
168 |
||
169 |
val das_wort_Model = if falsify then "Countermodel" else "Model"; |
|
170 |
val das_wort_model = if falsify then "countermodel" else "model"; |
|
171 |
||
66163 | 172 |
val tool_params = |
66627 | 173 |
{solvers = solvers, overlord = overlord, min_bound = min_bound, max_bound = max_bound, |
66625 | 174 |
bound_increment = bound_increment, debug = debug, specialize = specialize, |
66163 | 175 |
timeout = timeout}; |
64389 | 176 |
|
177 |
fun run () = |
|
178 |
let |
|
179 |
val outcome as (outcome_code, _) = |
|
180 |
let |
|
181 |
val (poly_axioms, isa_problem as {sound, complete, ...}) = |
|
182 |
isa_problem_of_subgoal ctxt falsify wfs whacks cards debug wf_timeout evals |
|
183 |
(if assms then all_assms else []) subgoal; |
|
184 |
val _ = print_d (fn () => "*** Isabelle problem ***\n" ^ |
|
185 |
str_of_isa_problem ctxt isa_problem); |
|
186 |
val ugly_nun_problem = nun_problem_of_isa ctxt isa_problem; |
|
187 |
val _ = print_d (fn () => "*** Ugly Nunchaku problem ***\n" ^ |
|
188 |
str_of_nun_problem ugly_nun_problem); |
|
189 |
val (nice_nun_problem, pool) = nice_nun_problem ugly_nun_problem; |
|
190 |
val _ = print_d (fn () => "*** Nice Nunchaku problem ***\n" ^ |
|
191 |
str_of_nun_problem nice_nun_problem); |
|
192 |
||
193 |
fun print_any_hints () = |
|
194 |
if has_lonely_bool_var subgoal then |
|
195 |
print "Hint: Maybe you forgot a colon after the lemma's name?" |
|
196 |
else if has_syntactic_sorts subgoal then |
|
197 |
print "Hint: Maybe you forgot a type constraint?" |
|
198 |
else |
|
199 |
(); |
|
200 |
||
201 |
fun get_isa_model_opt output = |
|
202 |
let |
|
203 |
val nice_nun_model = nun_model_of_str output; |
|
204 |
val _ = print_d (fn () => "*** Nice Nunchaku model ***\n" ^ |
|
205 |
str_of_nun_model nice_nun_model); |
|
206 |
val ugly_nun_model = ugly_nun_model pool nice_nun_model; |
|
207 |
val _ = print_d (fn () => "*** Ugly Nunchaku model ***\n" ^ |
|
208 |
str_of_nun_model ugly_nun_model); |
|
209 |
||
210 |
val pat_completes = pat_completes_of_isa_problem isa_problem; |
|
66623 | 211 |
val raw_isa_model = isa_model_of_nun ctxt pat_completes atomss ugly_nun_model; |
212 |
val _ = print_d (fn () => "*** Raw Isabelle model ***\n" ^ |
|
213 |
str_of_isa_model ctxt raw_isa_model); |
|
214 |
||
215 |
val cleaned_isa_model = clean_up_isa_model ctxt raw_isa_model; |
|
216 |
val _ = print_d (fn () => "*** Cleaned-up Isabelle model ***\n" ^ |
|
217 |
str_of_isa_model ctxt cleaned_isa_model); |
|
64389 | 218 |
in |
66623 | 219 |
cleaned_isa_model |
64389 | 220 |
end; |
221 |
||
222 |
fun isa_model_opt output = |
|
223 |
if debug then SOME (get_isa_model_opt output) else try get_isa_model_opt output; |
|
224 |
||
225 |
val model_str = isa_model_opt #> pretty_of_isa_model_opt ctxt #> Pretty.string_of; |
|
226 |
||
227 |
fun unsat_means_theorem () = |
|
228 |
null whacks andalso null cards andalso null monos; |
|
229 |
||
230 |
fun unknown () = |
|
66617 | 231 |
(print_n ("No " ^ das_wort_model ^ " found"); (unknownN, NONE)); |
64389 | 232 |
|
66620 | 233 |
fun unsat_or_unknown solver complete = |
64389 | 234 |
if complete then |
66620 | 235 |
(print_n ("No " ^ das_wort_model ^ " exists (according to " ^ solver ^ ")" ^ |
64407 | 236 |
(if falsify andalso unsat_means_theorem () then "\nThe goal is a theorem" |
237 |
else "")); |
|
64389 | 238 |
(noneN, NONE)) |
239 |
else |
|
240 |
unknown (); |
|
241 |
||
66620 | 242 |
fun sat_or_maybe_sat solver sound output = |
64389 | 243 |
let val header = if sound then das_wort_Model else "Potential " ^ das_wort_model in |
244 |
(case (null poly_axioms, none_true wfs) of |
|
245 |
(true, true) => |
|
66620 | 246 |
(print (header ^ " (according to " ^ solver ^ "):\n" ^ |
64389 | 247 |
model_str output); print_any_hints (); |
248 |
(genuineN, isa_model_opt output)) |
|
249 |
| (no_poly, no_wf) => |
|
250 |
let |
|
251 |
val ignorings = [] |
|
252 |
|> not no_poly ? cons "polymorphic axioms" |
|
253 |
|> not no_wf ? cons "unchecked well-foundedness"; |
|
254 |
in |
|
66620 | 255 |
(print (header ^ " (according to " ^ solver ^ |
256 |
", ignoring " ^ space_implode " and " ignorings ^ "):\n" ^ |
|
64389 | 257 |
model_str output ^ |
258 |
(if no_poly then |
|
259 |
"" |
|
260 |
else |
|
261 |
"\nIgnored axioms:\n" ^ |
|
262 |
cat_lines (map (prefix " " o Syntax.string_of_term ctxt) poly_axioms))); |
|
263 |
print_any_hints (); |
|
264 |
(quasi_genuineN, isa_model_opt output)) |
|
265 |
end) |
|
266 |
end; |
|
267 |
in |
|
268 |
(case solve_nun_problem tool_params nice_nun_problem of |
|
66620 | 269 |
Unsat solver => unsat_or_unknown solver complete |
270 |
| Sat (solver, output, _) => sat_or_maybe_sat solver sound output |
|
64389 | 271 |
| Unknown NONE => unknown () |
66620 | 272 |
| Unknown (SOME (solver, output, _)) => sat_or_maybe_sat solver false output |
64389 | 273 |
| Timeout => (print_n "Time out"; (unknownN, NONE)) |
274 |
| Nunchaku_Var_Not_Set => |
|
64469
488d4e627238
added Nunchaku component and tuned Nunchaku integration accordingly
blanchet
parents:
64407
diff
changeset
|
275 |
(print_n ("Variable $" ^ nunchaku_home_env_var ^ " not set"); (unknownN, NONE)) |
64389 | 276 |
| Nunchaku_Cannot_Execute => |
277 |
(print_n "External tool \"nunchaku\" cannot execute"; (unknownN, NONE)) |
|
278 |
| Nunchaku_Not_Found => |
|
279 |
(print_n "External tool \"nunchaku\" not found"; (unknownN, NONE)) |
|
280 |
| CVC4_Cannot_Execute => |
|
281 |
(print_n "External tool \"cvc4\" cannot execute"; (unknownN, NONE)) |
|
282 |
| CVC4_Not_Found => (print_n "External tool \"cvc4\" not found"; (unknownN, NONE)) |
|
283 |
| Unknown_Error (code, msg) => |
|
66632 | 284 |
(print_n ("Error: " ^ unprefix_error msg ^ |
64389 | 285 |
(if code = 0 then "" else " (code " ^ string_of_int code ^ ")")); |
286 |
(unknownN, NONE))) |
|
287 |
end |
|
288 |
handle |
|
289 |
CYCLIC_DEPS () => |
|
290 |
(print_n "Cyclic dependencies (or bug in Nunchaku)"; (unknownN, NONE)) |
|
291 |
| TOO_DEEP_DEPS () => |
|
292 |
(print_n "Too deep dependencies (or bug in Nunchaku)"; (unknownN, NONE)) |
|
293 |
| TOO_META t => |
|
294 |
(print_n ("Formula too meta for Nunchaku:\n" ^ Syntax.string_of_term ctxt t); |
|
295 |
(unknownN, NONE)) |
|
296 |
| UNEXPECTED_POLYMORPHISM t => |
|
297 |
(print_n ("Unexpected polymorphism in term\n" ^ Syntax.string_of_term ctxt t); |
|
298 |
(unknownN, NONE)) |
|
299 |
| UNEXPECTED_VAR t => |
|
300 |
(print_n ("Unexpected schematic variables in term\n" ^ Syntax.string_of_term ctxt t); |
|
301 |
(unknownN, NONE)) |
|
302 |
| UNSUPPORTED_FUNC t => |
|
303 |
(print_n ("Unsupported low-level constant in problem: " ^ Syntax.string_of_term ctxt t); |
|
304 |
(unknownN, NONE)); |
|
305 |
in |
|
306 |
if expect = "" orelse outcome_code = expect then outcome |
|
307 |
else error ("Unexpected outcome: " ^ quote outcome_code) |
|
308 |
end; |
|
309 |
||
310 |
val _ = spying spy (fn () => (state, i, "starting " ^ str_of_mode mode ^ " mode")); |
|
311 |
||
312 |
val outcome as (outcome_code, _) = |
|
73386 | 313 |
Timeout.apply (timeout + timeout_slack) run () |
64389 | 314 |
handle Timeout.TIMEOUT _ => (print_n "Time out"; (unknownN, NONE)); |
315 |
||
73386 | 316 |
val _ = print_v (fn () => "Total time: " ^ string_of_time (Time.now () - time_start)); |
64389 | 317 |
|
318 |
val _ = spying spy (fn () => (state, i, "outcome: " ^ outcome_code)); |
|
319 |
in |
|
320 |
if expect = "" orelse outcome_code = expect then outcome |
|
321 |
else error ("Unexpected outcome: " ^ quote outcome_code) |
|
322 |
end; |
|
323 |
||
324 |
fun run_chaku_on_subgoal state params mode i = |
|
325 |
let |
|
326 |
val ctxt = Proof.context_of state; |
|
327 |
val goal = Thm.prop_of (#goal (Proof.raw_goal state)); |
|
328 |
in |
|
329 |
if Logic.count_prems goal = 0 then |
|
330 |
(writeln "No subgoal!"; (noneN, NONE)) |
|
331 |
else |
|
332 |
let |
|
333 |
val subgoal = fst (Logic.goal_params goal i); |
|
334 |
val all_assms = map Thm.term_of (Assumption.all_assms_of ctxt); |
|
335 |
in |
|
336 |
run_chaku_on_prop state params mode i all_assms subgoal |
|
337 |
end |
|
338 |
end; |
|
339 |
||
340 |
end; |