From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 9 Feb 2010 19:20:32 +0000 (+0000)
Subject: moving built-in kinds out of the kind.h prologue/middle for uniformity; added TUPLE... 
X-Git-Tag: cvc5-1.0.0~9267
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=05fd8c08ecbe4b9056833d10b4a15061dba00a57;p=cvc5.git

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

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 90ec89968..dd5b2a2f6 100644
--- 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
index 000000000..806f4f402
--- /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 c34697cac..49e43ba68 100644
--- 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 53df4a590..7f4a0a3a2 100644
--- 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,