src/HOL/Nunchaku.thy
author blanchet
Fri Sep 08 01:14:33 2017 +0200 (23 months ago)
changeset 66637 809d40cfa4de
parent 66614 1f1c5d85d232
child 69605 a96320074298
permissions -rw-r--r--
correctly locate SMBC from Nunchaku
     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