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