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