* 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, 33 insertions, 9 deletions

diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index dc08788f3..cd0b4ef66 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -12,8 +12,10 @@
 #include "theory/interrupted.h"
 
 #include <vector>
+#include <utility>
+#include <iostream>
 
-namespace CVC4{
+namespace CVC4 {
 
 namespace theory {
 
@@ -21,12 +23,32 @@ namespace theory {
  * Very basic OutputChannel for testing simple Theory Behaviour.
  * Stores a call sequence for the output channel
  */
-enum OutputChannelCallType { CONFLICT, PROPOGATE, AUG_LEMMA, LEMMA, EXPLANATION };
+enum OutputChannelCallType {
+  CONFLICT,
+  PROPAGATE,
+  AUG_LEMMA,
+  LEMMA,
+  EXPLANATION
+};
+
+}/* CVC4::theory namespace */
+
+inline std::ostream& operator<<(std::ostream& out, theory::OutputChannelCallType type) {
+  switch(type) {
+  case theory::CONFLICT: return out << "CONFLICT";
+  case theory::PROPAGATE: return out << "PROPAGATE";
+  case theory::AUG_LEMMA: return out << "AUG_LEMMA";
+  case theory::LEMMA: return out << "LEMMA";
+  case theory::EXPLANATION: return out << "EXPLANATION";
+  default: return out << "UNDEFINED-OutputChannelCallType!" << int(type);
+  }
+}
 
+namespace theory {
 
 class TestOutputChannel : public theory::OutputChannel {
 public:
-  std::vector< pair<enum OutputChannelCallType, Node> > d_callHistory;
+  std::vector< std::pair<enum OutputChannelCallType, Node> > d_callHistory;
 
   TestOutputChannel() {}
 
@@ -34,12 +56,14 @@ public:
 
   void safePoint()  throw(Interrupted, AssertionException) {}
 
-  void conflict(TNode n, bool safe = false)  throw(Interrupted, AssertionException) {
+  void conflict(TNode n, bool safe = false)
+    throw(Interrupted, AssertionException) {
     push(CONFLICT, n);
   }
 
-  void propagate(TNode n, bool safe = false)  throw(Interrupted, AssertionException) {
-    push(PROPOGATE, n);
+  void propagate(TNode n, bool safe = false)
+    throw(Interrupted, AssertionException) {
+    push(PROPAGATE, n);
   }
 
   void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) {
@@ -71,11 +95,11 @@ public:
 
 private:
   void push(OutputChannelCallType call, TNode n) {
-    d_callHistory.push_back(make_pair(call,n));
+    d_callHistory.push_back(std::make_pair(call,n));
   }
 };/* class TestOutputChannel */
 
-}/* namespace theory */
-}/* namespace CVC4 */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__THEORY_TEST_UTILS_H */