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