Marging from types 404:415, changes: Massive

* Types are now represented as nodes in the attribute table and are managed, i.e. you can say
    Type booleanType = d_nodeManager->booleanType();
    Type t = d_nodeManager->mkFunctionType(booleanType, booleanType);
    FunctionType ft = (FunctionType)t;
    Assert(ft.getArgTypes()[0], booleanType);
* The attributes now have a table for Nodes and a table for TNodes (both should be used with caution)
* Changes the way nodes are extracted from NodeBuilder, added several methods to
  extract a Node, NodeValue, or Node*, with corresponding methods for extraction
* Used the above in the construction of Expr and Type objects
* The NodeManager now destroys the attributes in the destructor by pausing the
  garbage collection
* To achive destruction a flag d_inDesctruction has been added to loosen the assertion
  in NodeValue::dec() (there might be -refcount TNodes leftover)
* Beginnings of the Bitvector constants using GMP

Not yet in tiptop phase, needs more documentation, and Types should be pulled out to TypeNodes eventually. Also, the types are currently defined in the builting_kinds, and I need to add these to the theory specific definitions with special 'type' constructs.

I hate branching and merging.

10 files changed, 150 insertions, 149 deletions

diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index 5ae644193..d0be9a351 100644
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -70,7 +70,7 @@ public:
   typedef expr::Attribute<MyDataAttributeId, MyData*, MyDataCleanupFunction> MyDataAttribute;
 
   void testDeallocation() {
-    Type* booleanType = d_nodeManager->booleanType();
+    Type booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkVar(booleanType));
     MyData* data;
     MyData* data1;
@@ -88,7 +88,7 @@ public:
   typedef expr::Attribute<PrimitiveIntAttributeId,uint64_t> PrimitiveIntAttribute;
   typedef expr::CDAttribute<CDPrimitiveIntAttributeId,uint64_t> CDPrimitiveIntAttribute;
   void testInts(){
-    Type* booleanType = d_nodeManager->booleanType();
+    BooleanType booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkVar(booleanType));
     const uint64_t val = 63489;
     uint64_t data0 = 0;
@@ -116,7 +116,7 @@ public:
   typedef expr::Attribute<TNodeAttributeId, TNode> TNodeAttribute;
   typedef expr::CDAttribute<CDTNodeAttributeId, TNode> CDTNodeAttribute;
   void testTNodes(){
-    Type* booleanType = d_nodeManager->booleanType();
+    BooleanType booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkVar(booleanType));
 
     Node val(d_nodeManager->mkVar(booleanType));
@@ -151,7 +151,7 @@ public:
   typedef expr::Attribute<PtrAttributeId, Foo*> PtrAttribute;
   typedef expr::CDAttribute<CDPtrAttributeId, Foo*> CDPtrAttribute;
   void testPtrs(){
-    Type* booleanType = d_nodeManager->booleanType();
+    BooleanType booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkVar(booleanType));
 
     Foo* val = new Foo(63489);
@@ -182,7 +182,7 @@ public:
   typedef expr::Attribute<ConstPtrAttributeId, const Foo*> ConstPtrAttribute;
   typedef expr::CDAttribute<CDConstPtrAttributeId, const Foo*> CDConstPtrAttribute;
   void testConstPtrs(){
-    Type* booleanType = d_nodeManager->booleanType();
+    BooleanType booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkVar(booleanType));
 
     const Foo* val = new Foo(63489);
@@ -212,7 +212,7 @@ public:
   typedef expr::Attribute<StringAttributeId, std::string> StringAttribute;
   typedef expr::CDAttribute<CDStringAttributeId, std::string> CDStringAttribute;
   void testStrings(){
-    Type* booleanType = d_nodeManager->booleanType();
+    BooleanType booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkVar(booleanType));
 
     std::string val("63489");
@@ -241,7 +241,7 @@ public:
   typedef expr::Attribute<BoolAttributeId, bool> BoolAttribute;
   typedef expr::CDAttribute<CDBoolAttributeId, bool> CDBoolAttribute;
   void testBools(){
-    Type* booleanType = d_nodeManager->booleanType();
+    BooleanType booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkVar(booleanType));
 
     bool val = true;
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index e3b7811a4..bfe0ef3cf 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -69,10 +69,11 @@ public:
     d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
 
-    d_booleanType = d_nm->booleanType();
+    d_booleanType = new Type(d_nm->booleanType());
   }
 
   void tearDown() {
+    delete d_booleanType;
     delete d_scope;
     delete d_nm;
     delete d_ctxt;
@@ -101,9 +102,7 @@ public:
     TS_ASSERT_DIFFERS(TestStringAttr1::s_id, TestStringAttr2::s_id);
 
     lastId = attr::LastAttributeId<void*, false>::s_id;
-    TS_ASSERT_LESS_THAN(NodeManager::TypeAttr::s_id, lastId);
     TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId);
-    TS_ASSERT_DIFFERS(NodeManager::TypeAttr::s_id, theory::uf::ECAttr::s_id);
 
     lastId = attr::LastAttributeId<bool, false>::s_id;
     TS_ASSERT_LESS_THAN(NodeManager::AtomicAttr::s_id, lastId);
@@ -146,14 +145,18 @@ public:
 
     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(NodeManager::TypeAttr::s_id, lastId);
+
   }
 
   void testCDAttributes() {
     //Debug.on("boolattr");
 
-    Node a = d_nm->mkVar(d_booleanType);
-    Node b = d_nm->mkVar(d_booleanType);
-    Node c = d_nm->mkVar(d_booleanType);
+    Node a = d_nm->mkVar(*d_booleanType);
+    Node b = d_nm->mkVar(*d_booleanType);
+    Node c = d_nm->mkVar(*d_booleanType);
 
     Debug("boolattr", "get flag 1 on a (should be F)\n");
     TS_ASSERT(! a.getAttribute(TestFlag1cd()));
@@ -279,10 +282,10 @@ public:
   void testAttributes() {
     //Debug.on("boolattr");
 
-    Node a = d_nm->mkVar(d_booleanType);
-    Node b = d_nm->mkVar(d_booleanType);
-    Node c = d_nm->mkVar(d_booleanType);
-    Node unnamed = d_nm->mkVar(d_booleanType);
+    Node a = d_nm->mkVar(*d_booleanType);
+    Node b = d_nm->mkVar(*d_booleanType);
+    Node c = d_nm->mkVar(*d_booleanType);
+    Node unnamed = d_nm->mkVar(*d_booleanType);
 
     a.setAttribute(VarNameAttr(), "a");
     b.setAttribute(VarNameAttr(), "b");
diff --git a/test/unit/expr/declaration_scope_black.h b/test/unit/expr/declaration_scope_black.h
index f93a3fcc8..67e6d3e98 100644
--- a/test/unit/expr/declaration_scope_black.h
+++ b/test/unit/expr/declaration_scope_black.h
@@ -56,7 +56,7 @@ public:
 
   void testBind() {
     DeclarationScope declScope;
-    Type *booleanType = d_exprManager->booleanType();
+    Type booleanType = d_exprManager->booleanType();
     Expr x = d_exprManager->mkVar(booleanType);
     declScope.bind("x",x);
     TS_ASSERT( declScope.isBound("x") );
@@ -65,7 +65,7 @@ public:
 
   void testBind2() {
     DeclarationScope declScope;
-    Type *booleanType = d_exprManager->booleanType();
+    Type booleanType = d_exprManager->booleanType();
     // var name attribute shouldn't matter
     Expr y = d_exprManager->mkVar("y", booleanType);
     declScope.bind("x",y);
@@ -75,7 +75,7 @@ public:
 
   void testBind3() {
     DeclarationScope declScope;
-    Type *booleanType = d_exprManager->booleanType();
+    Type booleanType = d_exprManager->booleanType();
     Expr x = d_exprManager->mkVar(booleanType);
     declScope.bind("x",x);
     Expr y = d_exprManager->mkVar(booleanType);
@@ -87,11 +87,11 @@ public:
 
   void testBind4() {
     DeclarationScope declScope;
-    Type *booleanType = d_exprManager->booleanType();
+    Type booleanType = d_exprManager->booleanType();
     Expr x = d_exprManager->mkVar(booleanType);
     declScope.bind("x",x);
 
-    Type *t = d_exprManager->mkSort("T");
+    Type t = d_exprManager->mkSort("T");
     // duplicate binding for type is OK
     declScope.bindType("x",t);
 
@@ -103,7 +103,7 @@ public:
 
   void testBindType() {
     DeclarationScope declScope;
-    Type *s = d_exprManager->mkSort("S");
+    Type s = d_exprManager->mkSort("S");
     declScope.bindType("S",s);
     TS_ASSERT( declScope.isBoundType("S") );
     TS_ASSERT_EQUALS( declScope.lookupType("S"), s );
@@ -112,7 +112,7 @@ public:
   void testBindType2() {
     DeclarationScope declScope;
     // type name attribute shouldn't matter
-    Type *s = d_exprManager->mkSort("S");
+    Type s = d_exprManager->mkSort("S");
     declScope.bindType("T",s);
     TS_ASSERT( declScope.isBoundType("T") );
     TS_ASSERT_EQUALS( declScope.lookupType("T"), s );
@@ -120,9 +120,9 @@ public:
 
   void testBindType3() {
     DeclarationScope declScope;
-    Type *s = d_exprManager->mkSort("S");
+    Type s = d_exprManager->mkSort("S");
     declScope.bindType("S",s);
-    Type *t = d_exprManager->mkSort("T");
+    Type t = d_exprManager->mkSort("T");
     // new binding covers old
     declScope.bindType("S",t);
     TS_ASSERT( declScope.isBoundType("S") );
@@ -131,7 +131,7 @@ public:
 
   void testPushScope() {
     DeclarationScope declScope;
-    Type *booleanType = d_exprManager->booleanType();
+    Type booleanType = d_exprManager->booleanType();
     Expr x = d_exprManager->mkVar(booleanType);
     declScope.bind("x",x);
     declScope.pushScope();
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index fd36a7cfa..f40e32ef9 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -254,22 +254,18 @@ public:
   }
 
   void testGetType() {
-    /* Type* getType() const; */
+    /* Type getType(); */
 
     TS_ASSERT(a->getType() == d_em->booleanType());
     TS_ASSERT(b->getType() == d_em->booleanType());
-    TS_ASSERT(c->getType() == NULL);
-    TS_ASSERT(mult->getType() == NULL);
-    TS_ASSERT(plus->getType() == NULL);
-    TS_ASSERT(d->getType() == NULL);
-#ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(null->getType(), AssertionException);
-#endif /* CVC4_ASSERTIONS */
-
-    TS_ASSERT(i1->getType() == NULL);
-    TS_ASSERT(i2->getType() == NULL);
-    TS_ASSERT(r1->getType() == NULL);
-    TS_ASSERT(r2->getType() == NULL);
+    TS_ASSERT(c->getType().isNull());
+    TS_ASSERT(mult->getType().isNull());
+    TS_ASSERT(plus->getType().isNull());
+    TS_ASSERT(d->getType().isNull());
+    TS_ASSERT(i1->getType().isNull());
+    TS_ASSERT(i2->getType().isNull());
+    TS_ASSERT(r1->getType().isNull());
+    TS_ASSERT(r2->getType().isNull());
   }
 
   void testToString() {
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 23d1daf4e..6469806d6 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -36,7 +36,7 @@ private:
   Context* d_ctxt;
   NodeManager* d_nodeManager;
   NodeManagerScope* d_scope;
-  Type* d_booleanType;
+  Type *d_booleanType;
 
 public:
 
@@ -44,11 +44,11 @@ public:
     d_ctxt = new Context;
     d_nodeManager = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nodeManager);
-
-    d_booleanType = d_nodeManager->booleanType();
+    d_booleanType = new Type(d_nodeManager->booleanType());
   }
 
   void tearDown() {
+    delete d_booleanType;
     delete d_scope;
     delete d_nodeManager;
     delete d_ctxt;
@@ -97,12 +97,12 @@ public:
   void testOperatorEquals() {
     Node a, b, c;
 
-    b = d_nodeManager->mkVar(d_booleanType);
+    b = d_nodeManager->mkVar(*d_booleanType);
 
     a = b;
     c = a;
 
-    Node d = d_nodeManager->mkVar(d_booleanType);
+    Node d = d_nodeManager->mkVar(*d_booleanType);
 
     TS_ASSERT(a==a);
     TS_ASSERT(a==b);
@@ -137,12 +137,12 @@ public:
 
     Node a, b, c;
 
-    b = d_nodeManager->mkVar(d_booleanType);
+    b = d_nodeManager->mkVar(*d_booleanType);
 
     a = b;
     c = a;
 
-    Node d = d_nodeManager->mkVar(d_booleanType);
+    Node d = d_nodeManager->mkVar(*d_booleanType);
 
     /*structed assuming operator == works */
     TS_ASSERT(iff(a!=a, !(a==a)));
@@ -199,7 +199,7 @@ public:
   /*tests:   Node& operator=(const Node&); */
   void testOperatorAssign() {
     Node a, b;
-    Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkVar(d_booleanType));
+    Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkVar(*d_booleanType));
 
     b = c;
     TS_ASSERT(b==c);
@@ -320,8 +320,8 @@ public:
   void testIteNode() {
     /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/
 
-    Node a = d_nodeManager->mkVar(d_booleanType);
-    Node b = d_nodeManager->mkVar(d_booleanType);
+    Node a = d_nodeManager->mkVar(*d_booleanType);
+    Node b = d_nodeManager->mkVar(*d_booleanType);
 
     Node cnd = d_nodeManager->mkNode(PLUS, a, b);
     Node thenBranch = d_nodeManager->mkConst(true);
@@ -383,8 +383,8 @@ public:
   void testGetKind() {
     /*inline Kind getKind() const; */
 
-    Node a = d_nodeManager->mkVar(d_booleanType);
-    Node b = d_nodeManager->mkVar(d_booleanType);
+    Node a = d_nodeManager->mkVar(*d_booleanType);
+    Node b = d_nodeManager->mkVar(*d_booleanType);
 
     Node n = d_nodeManager->mkNode(NOT, a);
     TS_ASSERT(NOT == n.getKind());
@@ -400,9 +400,9 @@ public:
   }
 
   void testGetOperator() {
-    Type* sort = d_nodeManager->mkSort("T");
-    Type* booleanType = d_nodeManager->booleanType();
-    Type* predType = d_nodeManager->mkFunctionType(sort, booleanType);
+    Type sort = d_nodeManager->mkSort("T");
+    Type booleanType = d_nodeManager->booleanType();
+    Type predType = d_nodeManager->mkFunctionType(sort, booleanType);
 
     Node f = d_nodeManager->mkVar(predType);
     Node a = d_nodeManager->mkVar(booleanType);
@@ -466,9 +466,9 @@ public:
 
   void testIterator() {
     NodeBuilder<> b;
-    Node x = d_nodeManager->mkVar(d_booleanType);
-    Node y = d_nodeManager->mkVar(d_booleanType);
-    Node z = d_nodeManager->mkVar(d_booleanType);
+    Node x = d_nodeManager->mkVar(*d_booleanType);
+    Node y = d_nodeManager->mkVar(*d_booleanType);
+    Node z = d_nodeManager->mkVar(*d_booleanType);
     Node n = b << x << y << z << kind::AND;
 
     { // iterator
@@ -490,7 +490,7 @@ public:
   }
 
   void testToString() {
-    Type* booleanType = d_nodeManager->booleanType();
+    Type booleanType = d_nodeManager->booleanType();
 
     Node w = d_nodeManager->mkVar("w",booleanType);
     Node x = d_nodeManager->mkVar("x",booleanType);
@@ -503,7 +503,7 @@ public:
   }
 
   void testToStream() {
-    Type* booleanType = d_nodeManager->booleanType();
+    Type booleanType = d_nodeManager->booleanType();
 
     Node w = d_nodeManager->mkVar("w",booleanType);
     Node x = d_nodeManager->mkVar("x",booleanType);
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 4521f3bf6..17e1d6f18 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -47,10 +47,11 @@ public:
     d_scope = new NodeManagerScope(d_nm);
 
     specKind = PLUS;
-    d_booleanType = d_nm->booleanType();
+    d_booleanType = new Type(d_nm->booleanType());
   }
 
   void tearDown() {
+    delete d_booleanType;
     delete d_scope;
     delete d_nm;
     delete d_ctxt;
@@ -212,9 +213,9 @@ public:
 
   void testIterator() {
     NodeBuilder<> b;
-    Node x = d_nm->mkVar(d_booleanType);
-    Node y = d_nm->mkVar(d_booleanType);
-    Node z = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
+    Node y = d_nm->mkVar(*d_booleanType);
+    Node z = d_nm->mkVar(*d_booleanType);
     b << x << y << z << AND;
 
     {
@@ -463,9 +464,9 @@ public:
   }
 
   void testAppend() {
-    Node x = d_nm->mkVar(d_booleanType);
-    Node y = d_nm->mkVar(d_booleanType);
-    Node z = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
+    Node y = d_nm->mkVar(*d_booleanType);
+    Node z = d_nm->mkVar(*d_booleanType);
     Node m = d_nm->mkNode(AND, y, z, x);
     Node n = d_nm->mkNode(OR, d_nm->mkNode(NOT, x), y, z);
     Node o = d_nm->mkNode(XOR, y, x);
@@ -590,12 +591,12 @@ public:
   }
 
   void testConvenienceBuilders() {
-    Node a = d_nm->mkVar(d_booleanType);
-    Node b = d_nm->mkVar(d_booleanType);
-    Node c = d_nm->mkVar(d_booleanType);
-    Node d = d_nm->mkVar(d_booleanType);
-    Node e = d_nm->mkVar(d_booleanType);
-    Node f = d_nm->mkVar(d_booleanType);
+    Node a = d_nm->mkVar(*d_booleanType);
+    Node b = d_nm->mkVar(*d_booleanType);
+    Node c = d_nm->mkVar(*d_booleanType);
+    Node d = d_nm->mkVar(*d_booleanType);
+    Node e = d_nm->mkVar(*d_booleanType);
+    Node f = d_nm->mkVar(*d_booleanType);
 
     Node m = a && b;
     Node n = (a && b) || c;
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index e059fa509..873e28bb3 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -142,7 +142,7 @@ public:
   }
 
   void testMkVar1() {
-    Type* booleanType = d_nodeManager->booleanType();
+    Type booleanType = d_nodeManager->booleanType();
     Node x = d_nodeManager->mkVar(booleanType);
     TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
     TS_ASSERT_EQUALS(x.getNumChildren(),0u);
@@ -150,7 +150,7 @@ public:
   }
 
   void testMkVar2() {
-    Type* booleanType = d_nodeManager->booleanType();
+    Type booleanType = d_nodeManager->booleanType();
     Node x = d_nodeManager->mkVar("x", booleanType);
     TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
     TS_ASSERT_EQUALS(x.getNumChildren(),0u);
@@ -187,19 +187,19 @@ public:
   }
 
   void testBooleanType() {
-    Type* booleanType1 = d_nodeManager->booleanType();
-    Type* booleanType2 = d_nodeManager->booleanType();
-    Type* otherType = d_nodeManager->mkSort("T");
-    TS_ASSERT( booleanType1->isBoolean() );
+    Type booleanType1 = d_nodeManager->booleanType();
+    Type booleanType2 = d_nodeManager->booleanType();
+    Type otherType = d_nodeManager->mkSort("T");
+    TS_ASSERT( booleanType1.isBoolean() );
     TS_ASSERT_EQUALS(booleanType1, booleanType2);
     TS_ASSERT( booleanType1 != otherType );
   }
 
   void testKindType() {
-    Type* kindType1 = d_nodeManager->kindType();
-    Type* kindType2 = d_nodeManager->kindType();
-    Type* otherType = d_nodeManager->mkSort("T");
-    TS_ASSERT( kindType1->isKind() );
+    Type kindType1 = d_nodeManager->kindType();
+    Type kindType2 = d_nodeManager->kindType();
+    Type otherType = d_nodeManager->mkSort("T");
+    TS_ASSERT( kindType1.isKind() );
     TS_ASSERT_EQUALS(kindType1, kindType2);
     TS_ASSERT( kindType1 != otherType );
     // TODO: Is there a way to get the type of otherType (it should == kindType)
@@ -213,98 +213,98 @@ public:
    * with the current type implementation it's the best we can do. */
 
   void testMkFunctionType2() {
-    Type *booleanType = d_nodeManager->booleanType();
-    Type *t = d_nodeManager->mkFunctionType(booleanType,booleanType);
+    Type booleanType = d_nodeManager->booleanType();
+    Type t = d_nodeManager->mkFunctionType(booleanType,booleanType);
     TS_ASSERT( t != booleanType );
-    TS_ASSERT( t->isFunction() );
+    TS_ASSERT( t.isFunction() );
 
-    FunctionType* ft = (FunctionType*)t;
-    TS_ASSERT_EQUALS(ft->getArgTypes().size(), 1u);
-    TS_ASSERT_EQUALS(ft->getArgTypes()[0], booleanType);
-    TS_ASSERT_EQUALS(ft->getRangeType(), booleanType);
+    FunctionType ft = (FunctionType)t;
+    TS_ASSERT_EQUALS(ft.getArgTypes().size(), 1u);
+    TS_ASSERT_EQUALS(ft.getArgTypes()[0], booleanType);
+    TS_ASSERT_EQUALS(ft.getRangeType(), booleanType);
 
 /*    Type *t2 = d_nodeManager->mkFunctionType(booleanType,booleanType);
     TS_ASSERT_EQUALS( t, t2 );*/
   }
 
   void testMkFunctionTypeVecType() {
-    Type *a = d_nodeManager->mkSort("a");
-    Type *b = d_nodeManager->mkSort("b");
-    Type *c = d_nodeManager->mkSort("c");
+    Type a = d_nodeManager->mkSort("a");
+    Type b = d_nodeManager->mkSort("b");
+    Type c = d_nodeManager->mkSort("c");
 
-    std::vector<Type*> argTypes;
+    std::vector<Type> argTypes;
     argTypes.push_back(a);
     argTypes.push_back(b);
 
-    Type *t = d_nodeManager->mkFunctionType(argTypes,c);
+    Type t = d_nodeManager->mkFunctionType(argTypes,c);
 
     TS_ASSERT( t != a );
     TS_ASSERT( t != b );
     TS_ASSERT( t != c );
-    TS_ASSERT( t->isFunction() );
+    TS_ASSERT( t.isFunction() );
 
-    FunctionType* ft = (FunctionType*)t;
-    TS_ASSERT_EQUALS(ft->getArgTypes().size(), argTypes.size());
-    TS_ASSERT_EQUALS(ft->getArgTypes()[0], a);
-    TS_ASSERT_EQUALS(ft->getArgTypes()[1], b);
-    TS_ASSERT_EQUALS(ft->getRangeType(), c);
+    FunctionType ft = (FunctionType)t;
+    TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size());
+    TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
+    TS_ASSERT_EQUALS(ft.getArgTypes()[1], b);
+    TS_ASSERT_EQUALS(ft.getRangeType(), c);
 
 /*    Type *t2 = d_nodeManager->mkFunctionType(argTypes,c);
     TS_ASSERT_EQUALS( t, t2 );*/
   }
 
   void testMkFunctionTypeVec() {
-    Type *a = d_nodeManager->mkSort("a");
-    Type *b = d_nodeManager->mkSort("b");
-    Type *c = d_nodeManager->mkSort("c");
+    Type a = d_nodeManager->mkSort("a");
+    Type b = d_nodeManager->mkSort("b");
+    Type c = d_nodeManager->mkSort("c");
 
-    std::vector<Type*> types;
+    std::vector<Type> types;
     types.push_back(a);
     types.push_back(b);
     types.push_back(c);
 
-    Type *t = d_nodeManager->mkFunctionType(types);
+    Type t = d_nodeManager->mkFunctionType(types);
 
     TS_ASSERT( t != a );
     TS_ASSERT( t != b );
     TS_ASSERT( t != c );
-    TS_ASSERT( t->isFunction() );
+    TS_ASSERT( t.isFunction() );
 
-    FunctionType* ft = (FunctionType*)t;
-    TS_ASSERT_EQUALS(ft->getArgTypes().size(), types.size()-1);
-    TS_ASSERT_EQUALS(ft->getArgTypes()[0], a);
-    TS_ASSERT_EQUALS(ft->getArgTypes()[1], b);
-    TS_ASSERT_EQUALS(ft->getRangeType(), c);
+    FunctionType ft = (FunctionType)t;
+    TS_ASSERT_EQUALS(ft.getArgTypes().size(), types.size()-1);
+    TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
+    TS_ASSERT_EQUALS(ft.getArgTypes()[1], b);
+    TS_ASSERT_EQUALS(ft.getRangeType(), c);
 
 /*    Type *t2 = d_nodeManager->mkFunctionType(types);
     TS_ASSERT_EQUALS( t, t2 );*/
   }
 
   void testMkPredicateType() {
-    Type *a = d_nodeManager->mkSort("a");
-    Type *b = d_nodeManager->mkSort("b");
-    Type *c = d_nodeManager->mkSort("c");
-    Type *booleanType = d_nodeManager->booleanType();
+    Type a = d_nodeManager->mkSort("a");
+    Type b = d_nodeManager->mkSort("b");
+    Type c = d_nodeManager->mkSort("c");
+    Type booleanType = d_nodeManager->booleanType();
 
-    std::vector<Type*> argTypes;
+    std::vector<Type> argTypes;
     argTypes.push_back(a);
     argTypes.push_back(b);
     argTypes.push_back(c);
 
-    Type *t = d_nodeManager->mkPredicateType(argTypes);
+    Type t = d_nodeManager->mkPredicateType(argTypes);
 
     TS_ASSERT( t != a );
     TS_ASSERT( t != b );
     TS_ASSERT( t != c );
     TS_ASSERT( t != booleanType );
-    TS_ASSERT( t->isFunction() );
-
-    FunctionType* ft = (FunctionType*)t;
-    TS_ASSERT_EQUALS(ft->getArgTypes().size(), argTypes.size());
-    TS_ASSERT_EQUALS(ft->getArgTypes()[0], a);
-    TS_ASSERT_EQUALS(ft->getArgTypes()[1], b);
-    TS_ASSERT_EQUALS(ft->getArgTypes()[2], c);
-    TS_ASSERT_EQUALS(ft->getRangeType(), booleanType);
+    TS_ASSERT( t.isFunction() );
+
+    FunctionType ft = (FunctionType)t;
+    TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size());
+    TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
+    TS_ASSERT_EQUALS(ft.getArgTypes()[1], b);
+    TS_ASSERT_EQUALS(ft.getArgTypes()[2], c);
+    TS_ASSERT_EQUALS(ft.getRangeType(), booleanType);
 
 //    Type *t2 = d_nodeManager->mkPredicateType(argTypes);
 //    TS_ASSERT_EQUALS( t, t2 );
diff --git a/test/unit/parser/parser_white.h b/test/unit/parser/parser_white.h
index 653e3a1d7..317817e15 100644
--- a/test/unit/parser/parser_white.h
+++ b/test/unit/parser/parser_white.h
@@ -146,17 +146,17 @@ class ParserWhite : public CxxTest::TestSuite {
 
   void setupContext(ParserState* parserState) {
     /* a, b, c: BOOLEAN */
-    parserState->mkVar("a",(Type*)d_exprManager->booleanType());
-    parserState->mkVar("b",(Type*)d_exprManager->booleanType());
-    parserState->mkVar("c",(Type*)d_exprManager->booleanType());
+    parserState->mkVar("a",d_exprManager->booleanType());
+    parserState->mkVar("b",d_exprManager->booleanType());
+    parserState->mkVar("c",d_exprManager->booleanType());
     /* t, u, v: TYPE */
-    Type *t = parserState->mkSort("t");
-    Type *u = parserState->mkSort("u");
-    Type *v = parserState->mkSort("v");
+    Type t = parserState->mkSort("t");
+    Type u = parserState->mkSort("u");
+    Type v = parserState->mkSort("v");
     /* f : t->u; g: u->v; h: v->t; */
-    parserState->mkVar("f", (Type*)d_exprManager->mkFunctionType(t,u));
-    parserState->mkVar("g", (Type*)d_exprManager->mkFunctionType(u,v));
-    parserState->mkVar("h", (Type*)d_exprManager->mkFunctionType(v,t));
+    parserState->mkVar("f", d_exprManager->mkFunctionType(t,u));
+    parserState->mkVar("g", d_exprManager->mkFunctionType(u,v));
+    parserState->mkVar("h", d_exprManager->mkFunctionType(v,t));
     /* x:t; y:u; z:v; */
     parserState->mkVar("x",t);
     parserState->mkVar("y",u);
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 097724d48..25c22f196 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -211,8 +211,8 @@ public:
   void testRegisterTerm() {
     TS_ASSERT(d_dummy->doneWrapper());
 
-    Type* typeX = d_nm->booleanType();
-    Type* typeF = d_nm->mkFunctionType(typeX, typeX);
+    Type typeX = d_nm->booleanType();
+    Type typeF = d_nm->mkFunctionType(typeX, typeX);
 
     Node x = d_nm->mkVar("x",typeX);
     Node f = d_nm->mkVar("f",typeF);
diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h
index f5da06a0b..44b13c87c 100644
--- a/test/unit/theory/theory_uf_white.h
+++ b/test/unit/theory/theory_uf_white.h
@@ -107,10 +107,11 @@ public:
     d_outputChannel.clear();
     d_euf = new TheoryUF(d_ctxt, d_outputChannel);
 
-    d_booleanType = d_nm->booleanType();
+    d_booleanType = new Type(d_nm->booleanType());
   }
 
   void tearDown() {
+    delete d_booleanType;
     delete d_euf;
     d_outputChannel.clear();
     delete d_scope;
@@ -119,8 +120,8 @@ public:
   }
 
   void testPushPopChain() {
-    Node x = d_nm->mkVar(d_booleanType);
-    Node f = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
+    Node f = d_nm->mkVar(*d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
     Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
@@ -174,8 +175,8 @@ public:
 
   /* test that {f(f(x)) == x, f(f(f(x))) != f(x)} is inconsistent */
   void testSimpleChain() {
-    Node x = d_nm->mkVar(d_booleanType);
-    Node f = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
+    Node f = d_nm->mkVar(*d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
     Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
@@ -199,7 +200,7 @@ public:
 
   /* test that !(x == x) is inconsistent */
   void testSelfInconsistent() {
-    Node x = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
     Node x_neq_x = (x.eqNode(x)).notNode();
 
     d_euf->assertFact(x_neq_x);
@@ -212,7 +213,7 @@ public:
 
   /* test that (x == x) is consistent */
   void testSelfConsistent() {
-    Node x = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
     Node x_eq_x = x.eqNode(x);
 
     d_euf->assertFact(x_eq_x);
@@ -228,8 +229,8 @@ public:
       f(x) != x
      } is inconsistent */
   void testChain() {
-    Node x = d_nm->mkVar(d_booleanType);
-    Node f = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
+    Node f = d_nm->mkVar(*d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
     Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
@@ -259,7 +260,7 @@ public:
 
 
   void testPushPopA() {
-    Node x = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
     Node x_eq_x = x.eqNode(x);
 
     d_ctxt->push();
@@ -270,8 +271,8 @@ public:
   }
 
   void testPushPopB() {
-    Node x = d_nm->mkVar(d_booleanType);
-    Node f = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
+    Node f = d_nm->mkVar(*d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_x_eq_x = f_x.eqNode(x);