src/HOL/Nunchaku.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 66637 809d40cfa4de
child 69605 a96320074298
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      HOL/Nunchaku.thy
     2     Author:     Jasmin Blanchette, VU Amsterdam
     3     Copyright   2015, 2016, 2017
     4 
     5 Nunchaku: Yet another counterexample generator for Isabelle/HOL.
     6 
     7 Nunchaku relies on an external program of the same name. The sources are
     8 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, Kodkodi, and SMBC are necessary to use these backend solvers.
    15 *)
    16 
    17 theory Nunchaku
    18 imports Nitpick
    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/nunchaku_util.ML"
    33 ML_file "Tools/Nunchaku/nunchaku_collect.ML"
    34 ML_file "Tools/Nunchaku/nunchaku_problem.ML"
    35 ML_file "Tools/Nunchaku/nunchaku_translate.ML"
    36 ML_file "Tools/Nunchaku/nunchaku_model.ML"
    37 ML_file "Tools/Nunchaku/nunchaku_reconstruct.ML"
    38 ML_file "Tools/Nunchaku/nunchaku_display.ML"
    39 ML_file "Tools/Nunchaku/nunchaku_tool.ML"
    40 ML_file "Tools/Nunchaku/nunchaku.ML"
    41 ML_file "Tools/Nunchaku/nunchaku_commands.ML"
    42 
    43 hide_const (open) unreachable The_unsafe rmember
    44 
    45 end