* theory "tree" rewriting implemented and works

* added TheoryArith::preRewrite() to test and demonstrate
  the use of pre-rewriting.

* array types and type checking now supported

* array type checking now supported

* theoryOf() dispatching properly to arrays now

* theories now required to implement a (simple) identify()
  function that returns a string identifying them for
  debugging/user output purposes

* added "builtin" theory to hold all built-in kinds and their
  type rules and rewriting (currently only exploding distinct)

* fixed production build failure (regarding NodeSetDepth)

* removed an errant "using namespace std" in util/bitvector.h
  (and made associated trivial fixes elsewhere)

* fixes to make unexpected exceptions more verbose in debug builds

* fixes to make multiple, cascading assertion fails simpler

* minor other fixes to comments etc.

1 files changed, 13 insertions, 0 deletions

diff --git a/src/theory/builtin/Makefile.am b/src/theory/builtin/Makefile.am
new file mode 100644
index 000000000..5694dea84
--- /dev/null
+++ b/src/theory/builtin/Makefile.am
@@ -0,0 +1,13 @@
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../../include -I@srcdir@/../..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libbuiltin.la
+
+libbuiltin_la_SOURCES = \
+	theory_builtin_type_rules.h \
+	theory_builtin.h \
+	theory_builtin.cpp
+
+EXTRA_DIST = kinds