diff options
Diffstat (limited to 'src/expr/mkkind')
| -rwxr-xr-x | src/expr/mkkind | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/src/expr/mkkind b/src/expr/mkkind index 6d75164d1..294dc5d7e 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -4,12 +4,12 @@ # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 # Copyright (c) 2010 The CVC4 Project # -# The purpose of this script is to create kind.h from a prologue, -# middle section, epilogue, and a list of theory kinds. +# The purpose of this script is to create kind.h from a template and a +# list of theory kinds. # # Invocation: # -# mkkind prologue-file middle-file epilogue-file theory-kind-files... +# mkkind template-file theory-kind-files... # # Output is to standard out. # @@ -17,7 +17,7 @@ copyright=2010 cat <<EOF -/********************* -*- C++ -*- */ +/********************* */ /** kind.h ** ** Copyright $copyright The AcSys Group, New York University, and as below. @@ -83,6 +83,15 @@ function operator { register_kind "$1" "$2" "$3" } +function nonatomic_operator { + # nonatomic_operator K #children ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + register_kind "$1" "$2" "$3" +} + function parameterized { # parameterized K #children ["comment"] |