1 (* Title: HOL/Nunchaku/Nunchaku.thy |
|
2 Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII |
|
3 Copyright 2015, 2016 |
|
4 |
|
5 Nunchaku: Yet another counterexample generator for Isabelle/HOL. |
|
6 |
|
7 Nunchaku relies on an external program of the same name. The program is still |
|
8 being actively developed. The sources are available at |
|
9 |
|
10 https://github.com/nunchaku-inria |
|
11 |
|
12 The "$NUNCHAKU_HOME" environment variable must be set to the absolute path to |
|
13 the directory containing the "nunchaku" executable. The Isabelle components |
|
14 for CVC4 and Kodkodi are necessary to use these backend solvers. |
|
15 *) |
|
16 |
|
17 theory Nunchaku |
|
18 imports Main |
|
19 keywords |
|
20 "nunchaku" :: diag and |
|
21 "nunchaku_params" :: thy_decl |
|
22 begin |
|
23 |
|
24 consts unreachable :: 'a |
|
25 |
|
26 definition The_unsafe :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" where |
|
27 "The_unsafe = The" |
|
28 |
|
29 definition rmember :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" where |
|
30 "rmember A x \<longleftrightarrow> x \<in> A" |
|
31 |
|
32 ML_file "Tools/nunchaku_util.ML" |
|
33 ML_file "Tools/nunchaku_collect.ML" |
|
34 ML_file "Tools/nunchaku_problem.ML" |
|
35 ML_file "Tools/nunchaku_translate.ML" |
|
36 ML_file "Tools/nunchaku_model.ML" |
|
37 ML_file "Tools/nunchaku_reconstruct.ML" |
|
38 ML_file "Tools/nunchaku_display.ML" |
|
39 ML_file "Tools/nunchaku_tool.ML" |
|
40 ML_file "Tools/nunchaku.ML" |
|
41 ML_file "Tools/nunchaku_commands.ML" |
|
42 |
|
43 hide_const (open) unreachable The_unsafe rmember |
|
44 |
|
45 end |
|