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

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 3eb2a8109..f28729b94 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -31,7 +31,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 32 "${template}"
+#line 35 "${template}"
 
 using namespace std;
 using namespace CVC4::context;
@@ -69,11 +69,6 @@ IntegerType ExprManager::integerType() const {
   return Type(d_nodeManager, new TypeNode(d_nodeManager->integerType()));
 }
 
-BitVectorType ExprManager::bitVectorType(unsigned size) const {
-  NodeManagerScope nms(d_nodeManager);
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->bitVectorType(size)));
-}
-
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
   const unsigned n = 1;
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
@@ -216,7 +211,17 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes)));
 }
 
-SortType ExprManager::mkSort(const std::string& name) {
+BitVectorType ExprManager::mkBitVectorType(unsigned size) const {
+  NodeManagerScope nms(d_nodeManager);
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size)));
+}
+
+ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const {
+  NodeManagerScope nms(d_nodeManager);
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode)));
+}
+
+SortType ExprManager::mkSort(const std::string& name) const {
   NodeManagerScope nms(d_nodeManager);
   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name)));
 }