* 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.

4 files changed, 18 insertions, 8 deletions

diff --git a/test/regress/regress0/distinct.smt b/test/regress/regress0/distinct.smt
index 3c3578edc..8c36a9acb 100644
--- a/test/regress/regress0/distinct.smt
+++ b/test/regress/regress0/distinct.smt
@@ -2,4 +2,4 @@
   :logic QF_UF
   :status unsat
   :extrafuns ((x U) (y U) (z U))
-  :formula (not (iff (distinct x y z) (and (not (= x y)) (not (= x z)) (not (= y z))))))
\ No newline at end of file
+  :formula (not (iff (distinct x y z) (and (not (= x y)) (not (= x z)) (not (= y z))))))
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index 8afc012ff..c07fb1b09 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -26,7 +26,7 @@
 #include "expr/node_manager.h"
 #include "expr/attribute.h"
 #include "expr/node.h"
-#include "theory/theory.h"
+#include "theory/theory_engine.h"
 #include "theory/uf/theory_uf.h"
 #include "util/Assert.h"
 
@@ -138,8 +138,17 @@ public:
     TS_ASSERT_DIFFERS(theory::Theory::RegisteredAttr::s_id, TestFlag2cd::s_id);
     TS_ASSERT_DIFFERS(TestFlag1cd::s_id, TestFlag2cd::s_id);
 
-    lastId = attr::LastAttributeId<TNode, false>::s_id;
-    TS_ASSERT_LESS_THAN(theory::RewriteCache::s_id, lastId);
+    lastId = attr::LastAttributeId<Node, false>::s_id;
+    TS_ASSERT_LESS_THAN(theory::PreRewriteCache::s_id, lastId);
+    TS_ASSERT_LESS_THAN(theory::PostRewriteCache::s_id, lastId);
+    TS_ASSERT_LESS_THAN(theory::PreRewriteCacheTop::s_id, lastId);
+    TS_ASSERT_LESS_THAN(theory::PostRewriteCacheTop::s_id, lastId);
+    TS_ASSERT_DIFFERS(theory::PreRewriteCache::s_id, theory::PostRewriteCache::s_id);
+    TS_ASSERT_DIFFERS(theory::PreRewriteCache::s_id, theory::PreRewriteCacheTop::s_id);
+    TS_ASSERT_DIFFERS(theory::PreRewriteCache::s_id, theory::PostRewriteCacheTop::s_id);
+    TS_ASSERT_DIFFERS(theory::PostRewriteCache::s_id, theory::PreRewriteCacheTop::s_id);
+    TS_ASSERT_DIFFERS(theory::PostRewriteCache::s_id, theory::PostRewriteCacheTop::s_id);
+    TS_ASSERT_DIFFERS(theory::PreRewriteCacheTop::s_id, theory::PostRewriteCacheTop::s_id);
 
     lastId = attr::LastAttributeId<TypeNode, false>::s_id;
     TS_ASSERT_LESS_THAN(NodeManager::TypeAttr::s_id, lastId);
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index fe9cbb388..d6614b87e 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -206,7 +206,7 @@ public:
 
 
     Node expectedProp = d_nm->mkNode(GEQ, x, c);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPOGATE);
+    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPAGATE);
     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), expectedProp);
 
   }
@@ -236,7 +236,7 @@ public:
     d_arith->explain(rLeq1, d_level);
 
     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), PROPOGATE);
+    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), PROPAGATE);
     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), EXPLANATION);
     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq1);
     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), rLt1);
@@ -270,8 +270,8 @@ public:
     d_arith->explain(rLeq1, d_level);
 
     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 4u);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), PROPOGATE);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPOGATE);
+    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), PROPAGATE);
+    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPAGATE);
     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), EXPLANATION);
     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(3), EXPLANATION);
 
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 9c056d368..106d01b13 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -129,6 +129,7 @@ public:
   void preRegisterTerm(TNode n) {}
   void propagate(Effort level) {}
   void explain(TNode n, Effort level) {}
+  string identify() const { return "DummyTheory"; }
 };
 
 class TheoryBlack : public CxxTest::TestSuite {