moving built-in kinds out of the kind.h prologue/middle for uniformity; added TUPLE...

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 90ec89968252074cbb161752fd0ed488ad1122d3..dd5b2a2f65483bf8acaeadaf19df628f3e17d347 100644 (file)
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -35,6 +35,7 @@ EXTRA_DIST = @srcdir@/kind.h kind_prologue.h kind_middle.h kind_epilogue.h
                @srcdir@/kind_prologue.h \
                @srcdir@/kind_middle.h \
                @srcdir@/kind_epilogue.h \
+               @srcdir@/builtin_kinds \
                `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
        > @srcdir@/kind.h) || (rm -f @srcdir@/kind.h && exit 1)
 

diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds
new file mode 100644 (file)
index 0000000..806f4f4
--- /dev/null
+++ b/src/expr/builtin_kinds
@@ -0,0 +1,5 @@
+EQUAL
+ITE
+SKOLEM
+VARIABLE
+TUPLE

diff --git a/src/expr/kind_middle.h b/src/expr/kind_middle.h
index c34697cacd9638caf60351dd24bef2d6f081ac2d..49e43ba6883c6c3e46bf4cd744390c2dfcd333cb 100644 (file)
--- a/src/expr/kind_middle.h
+++ b/src/expr/kind_middle.h
@@ -27,8 +27,3 @@ inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
   /* special cases */
   case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break;
   case NULL_EXPR: out << "NULL"; break;
-
-  case EQUAL: out << "EQUAL"; break;
-  case ITE: out << "ITE"; break;
-  case SKOLEM: out << "SKOLEM"; break;
-  case VARIABLE: out << "VARIABLE"; break;

diff --git a/src/expr/kind_prologue.h b/src/expr/kind_prologue.h
index 53df4a59031ffa37850318aa050c0c21718338b0..7f4a0a3a23543192a782535b6c4dd8f7b1e9b360 100644 (file)
--- a/src/expr/kind_prologue.h
+++ b/src/expr/kind_prologue.h
@@ -26,9 +26,3 @@ enum Kind {
   UNDEFINED_KIND = -1,
   /** Null Kind */
   NULL_EXPR,
-
-  /* built-ins */
-  EQUAL,
-  ITE,
-  SKOLEM,
-  VARIABLE,