src/HOL/Nunchaku/Nunchaku.thy
author blanchet
Mon Nov 07 14:55:39 2016 +0100 (2016-11-07)
changeset 64469 488d4e627238
parent 64407 5c5b9d945625
child 66163 45d3d43abee7
permissions -rw-r--r--
added Nunchaku component and tuned Nunchaku integration accordingly
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@64469
    12
The "$NUNCHAKU_HOME" environment variable must be set to the absolute path to
blanchet@64469
    13
the directory containing the "nunchaku" executable. The Isabelle components
blanchet@64469
    14
for CVC4 and Kodkodi are 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