src/HOL/Nunchaku.thy
author blanchet
Fri Sep 08 01:14:33 2017 +0200 (2017-09-08)
changeset 66637 809d40cfa4de
parent 66614 1f1c5d85d232
child 69605 a96320074298
permissions -rw-r--r--
correctly locate SMBC from Nunchaku
blanchet@66614
     1
(*  Title:      HOL/Nunchaku.thy
blanchet@66614
     2
    Author:     Jasmin Blanchette, VU Amsterdam
blanchet@66614
     3
    Copyright   2015, 2016, 2017
blanchet@64389
     4
blanchet@64389
     5
Nunchaku: Yet another counterexample generator for Isabelle/HOL.
blanchet@64389
     6
blanchet@66614
     7
Nunchaku relies on an external program of the same name. The sources are
blanchet@66614
     8
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@66637
    14
for CVC4, Kodkodi, and SMBC are necessary to use these backend solvers.
blanchet@64389
    15
*)
blanchet@64389
    16
blanchet@64389
    17
theory Nunchaku
blanchet@66614
    18
imports Nitpick
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@66614
    32
ML_file "Tools/Nunchaku/nunchaku_util.ML"
blanchet@66614
    33
ML_file "Tools/Nunchaku/nunchaku_collect.ML"
blanchet@66614
    34
ML_file "Tools/Nunchaku/nunchaku_problem.ML"
blanchet@66614
    35
ML_file "Tools/Nunchaku/nunchaku_translate.ML"
blanchet@66614
    36
ML_file "Tools/Nunchaku/nunchaku_model.ML"
blanchet@66614
    37
ML_file "Tools/Nunchaku/nunchaku_reconstruct.ML"
blanchet@66614
    38
ML_file "Tools/Nunchaku/nunchaku_display.ML"
blanchet@66614
    39
ML_file "Tools/Nunchaku/nunchaku_tool.ML"
blanchet@66614
    40
ML_file "Tools/Nunchaku/nunchaku.ML"
blanchet@66614
    41
ML_file "Tools/Nunchaku/nunchaku_commands.ML"
blanchet@64389
    42
blanchet@64389
    43
hide_const (open) unreachable The_unsafe rmember
blanchet@64389
    44
blanchet@64389
    45
end