* 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, 17 insertions, 6 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 6e2141351..8f7196e0c 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -20,10 +20,11 @@
 
 #include "node_manager.h"
 
-#include "expr/builtin_type_rules.h"
+#include "theory/builtin/theory_builtin_type_rules.h"
 #include "theory/booleans/theory_bool_type_rules.h"
 #include "theory/uf/theory_uf_type_rules.h"
 #include "theory/arith/theory_arith_type_rules.h"
+#include "theory/arrays/theory_arrays_type_rules.h"
 #include "theory/bv/theory_bv_type_rules.h"
 
 #include <ext/hash_set>
@@ -181,17 +182,19 @@ void NodeManager::reclaimZombies() {
   }
 }/* NodeManager::reclaimZombies() */
 
-TypeNode NodeManager::getType(TNode n) throw (TypeCheckingExceptionPrivate) {
+TypeNode NodeManager::getType(TNode n)
+  throw (TypeCheckingExceptionPrivate, AssertionException) {
   TypeNode typeNode;
   bool hasType = getAttribute(n, TypeAttr(), typeNode);
-  if (!hasType) {
+  Debug("getType") << "getting type for " << n << std::endl;
+  if(!hasType) {
     // Infer the type
-    switch (n.getKind()) {
+    switch(n.getKind()) {
     case kind::EQUAL:
-      typeNode = CVC4::EqualityTypeRule::computeType(this, n);
+      typeNode = CVC4::theory::builtin::EqualityTypeRule::computeType(this, n);
       break;
     case kind::DISTINCT:
-      typeNode = CVC4::DistinctTypeRule::computeType(this, n);
+      typeNode = CVC4::theory::builtin::DistinctTypeRule::computeType(this, n);
       break;
     case kind::CONST_BOOLEAN:
       typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n);
@@ -253,6 +256,12 @@ TypeNode NodeManager::getType(TNode n) throw (TypeCheckingExceptionPrivate) {
     case kind::GEQ:
       typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n);
       break;
+    case kind::SELECT:
+      typeNode = CVC4::theory::arrays::ArraySelectTypeRule::computeType(this, n);
+      break;
+    case kind::STORE:
+      typeNode = CVC4::theory::arrays::ArrayStoreTypeRule::computeType(this, n);
+      break;
     case kind::BITVECTOR_CONST:
       typeNode = CVC4::theory::bv::BitVectorConstantTypeRule::computeType(this, n);
       break;
@@ -362,10 +371,12 @@ TypeNode NodeManager::getType(TNode n) throw (TypeCheckingExceptionPrivate) {
       typeNode = CVC4::theory::bv::BitVectorExtendTypeRule::computeType(this, n);
       break;
     default:
+      Debug("getType") << "FAILURE" << std::endl;
       Unhandled(n.getKind());
     }
     setAttribute(n, TypeAttr(), typeNode);
   }
+  Debug("getType") << "type of " << n << " is " << typeNode << std::endl;
   return typeNode;
 }