diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-02-09 19:20:32 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-02-09 19:20:32 +0000 |
| commit | 05fd8c08ecbe4b9056833d10b4a15061dba00a57 (patch) | |
| tree | 780b10f3b96a3c848766d4f7dbda590e352a3b30 /src | |
| parent | cbd51a7c0219f7ced9d48ef3810c440dda1fe8e5 (diff) | |
moving built-in kinds out of the kind.h prologue/middle for uniformity; added TUPLE built-in
Diffstat (limited to 'src')
| -rw-r--r-- | src/expr/Makefile.am | 1 | ||||
| -rw-r--r-- | src/expr/builtin_kinds | 5 | ||||
| -rw-r--r-- | src/expr/kind_middle.h | 5 | ||||
| -rw-r--r-- | src/expr/kind_prologue.h | 6 |
4 files changed, 6 insertions, 11 deletions
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, |