From 05fd8c08ecbe4b9056833d10b4a15061dba00a57 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 9 Feb 2010 19:20:32 +0000 Subject: [PATCH] moving built-in kinds out of the kind.h prologue/middle for uniformity; added TUPLE built-in --- src/expr/Makefile.am | 1 + src/expr/builtin_kinds | 5 +++++ src/expr/kind_middle.h | 5 ----- src/expr/kind_prologue.h | 6 ------ 4 files changed, 6 insertions(+), 11 deletions(-) create mode 100644 src/expr/builtin_kinds 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, -- 2.30.2