Adding the intermediary TypeNode to represent (and separate) the Types at the Node level.

5 files changed, 55 insertions, 55 deletions

diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index d0be9a351..7894743d6 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();
+    TypeNode 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(){
-    BooleanType booleanType = d_nodeManager->booleanType();
+    TypeNode 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(){
-    BooleanType booleanType = d_nodeManager->booleanType();
+    TypeNode 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(){
-    BooleanType booleanType = d_nodeManager->booleanType();
+    TypeNode 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(){
-    BooleanType booleanType = d_nodeManager->booleanType();
+    TypeNode 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(){
-    BooleanType booleanType = d_nodeManager->booleanType();
+    TypeNode 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(){
-    BooleanType booleanType = d_nodeManager->booleanType();
+    TypeNode 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 bfe0ef3cf..43bcc7fe3 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -60,7 +60,7 @@ class AttributeWhite : public CxxTest::TestSuite {
   Context* d_ctxt;
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
-  Type* d_booleanType;
+  TypeNode* d_booleanType;
 
 public:
 
@@ -69,7 +69,7 @@ public:
     d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
 
-    d_booleanType = new Type(d_nm->booleanType());
+    d_booleanType = new TypeNode(d_nm->booleanType());
   }
 
   void tearDown() {
@@ -146,7 +146,7 @@ public:
     lastId = attr::LastAttributeId<TNode, false>::s_id;
     TS_ASSERT_LESS_THAN(theory::RewriteCache::s_id, lastId);
 
-    lastId = attr::LastAttributeId<Node, false>::s_id;
+    lastId = attr::LastAttributeId<TypeNode, false>::s_id;
     TS_ASSERT_LESS_THAN(NodeManager::TypeAttr::s_id, lastId);
 
   }
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 6469806d6..7e034036a 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;
+  TypeNode *d_booleanType;
 
 public:
 
@@ -44,7 +44,7 @@ public:
     d_ctxt = new Context;
     d_nodeManager = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nodeManager);
-    d_booleanType = new Type(d_nodeManager->booleanType());
+    d_booleanType = new TypeNode(d_nodeManager->booleanType());
   }
 
   void tearDown() {
@@ -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);
+    TypeNode sort = d_nodeManager->mkSort("T");
+    TypeNode booleanType = d_nodeManager->booleanType();
+    TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType);
 
     Node f = d_nodeManager->mkVar(predType);
     Node a = d_nodeManager->mkVar(booleanType);
@@ -490,7 +490,7 @@ public:
   }
 
   void testToString() {
-    Type booleanType = d_nodeManager->booleanType();
+    TypeNode 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();
+    TypeNode 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 17e1d6f18..a1887118c 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -37,7 +37,7 @@ private:
   Context* d_ctxt;
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
-  Type* d_booleanType;
+  TypeNode* d_booleanType;
 
 public:
 
@@ -47,7 +47,7 @@ public:
     d_scope = new NodeManagerScope(d_nm);
 
     specKind = PLUS;
-    d_booleanType = new Type(d_nm->booleanType());
+    d_booleanType = new TypeNode(d_nm->booleanType());
   }
 
   void tearDown() {
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index 118ba8173..0e1e09178 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -142,7 +142,7 @@ public:
   }
 
   void testMkVarWithNoName() {
-    Type booleanType = d_nodeManager->booleanType();
+    TypeNode 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 testMkVarWithName() {
-    Type booleanType = d_nodeManager->booleanType();
+    TypeNode booleanType = d_nodeManager->booleanType();
     Node x = d_nodeManager->mkVar("x", booleanType);
     TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
     TS_ASSERT_EQUALS(x.getNumChildren(),0u);
@@ -187,9 +187,9 @@ public:
   }
 
   void testBooleanType() {
-    Type t = d_nodeManager->booleanType();
-    Type t2 = d_nodeManager->booleanType();
-    Type t3 = d_nodeManager->mkSort("T");
+    TypeNode t = d_nodeManager->booleanType();
+    TypeNode t2 = d_nodeManager->booleanType();
+    TypeNode t3 = d_nodeManager->mkSort("T");
     TS_ASSERT( t.isBoolean() );
     TS_ASSERT( !t.isFunction() );
     TS_ASSERT( !t.isKind() );
@@ -199,14 +199,14 @@ public:
     TS_ASSERT_EQUALS(t, t2);
     TS_ASSERT( t != t3 );
 
-    BooleanType bt = t;
+    TypeNode bt = t;
     TS_ASSERT_EQUALS( bt, t);
   }
 
   void testKindType() {
-    Type t = d_nodeManager->kindType();
-    Type t2 = d_nodeManager->kindType();
-    Type t3 = d_nodeManager->mkSort("T");
+    TypeNode t = d_nodeManager->kindType();
+    TypeNode t2 = d_nodeManager->kindType();
+    TypeNode t3 = d_nodeManager->mkSort("T");
 
     TS_ASSERT( !t.isBoolean() );
     TS_ASSERT( !t.isFunction() );
@@ -218,15 +218,15 @@ public:
     TS_ASSERT_EQUALS(t, t2);
     TS_ASSERT( t != t3);
 
-    KindType kt = t;
+    TypeNode kt = t;
     TS_ASSERT_EQUALS( kt, t );
     // TODO: Is there a way to get the type of otherType (it should == t)?
   }
 
   void testMkFunctionTypeBoolToBool() {
-    Type booleanType = d_nodeManager->booleanType();
-    Type t = d_nodeManager->mkFunctionType(booleanType,booleanType);
-    Type t2 = d_nodeManager->mkFunctionType(booleanType,booleanType);
+    TypeNode booleanType = d_nodeManager->booleanType();
+    TypeNode t = d_nodeManager->mkFunctionType(booleanType,booleanType);
+    TypeNode t2 = d_nodeManager->mkFunctionType(booleanType,booleanType);
 
     TS_ASSERT( !t.isBoolean() );
     TS_ASSERT( t.isFunction() );
@@ -237,7 +237,7 @@ public:
 
     TS_ASSERT_EQUALS( t, t2 );
 
-    FunctionType ft = t;
+    TypeNode ft = t;
     TS_ASSERT_EQUALS( ft, t );
     TS_ASSERT_EQUALS(ft.getArgTypes().size(), 1u);
     TS_ASSERT_EQUALS(ft.getArgTypes()[0], booleanType);
@@ -246,16 +246,16 @@ public:
   }
 
   void testMkFunctionTypeVectorOfArgsWithReturnType() {
-    Type a = d_nodeManager->mkSort();
-    Type b = d_nodeManager->mkSort();
-    Type c = d_nodeManager->mkSort();
+    TypeNode a = d_nodeManager->mkSort();
+    TypeNode b = d_nodeManager->mkSort();
+    TypeNode c = d_nodeManager->mkSort();
 
-    std::vector<Type> argTypes;
+    std::vector<TypeNode> argTypes;
     argTypes.push_back(a);
     argTypes.push_back(b);
 
-    Type t = d_nodeManager->mkFunctionType(argTypes,c);
-    Type t2 = d_nodeManager->mkFunctionType(argTypes,c);
+    TypeNode t = d_nodeManager->mkFunctionType(argTypes,c);
+    TypeNode t2 = d_nodeManager->mkFunctionType(argTypes,c);
 
     TS_ASSERT( !t.isBoolean() );
     TS_ASSERT( t.isFunction() );
@@ -266,7 +266,7 @@ public:
 
     TS_ASSERT_EQUALS( t, t2 );
 
-    FunctionType ft = t;
+    TypeNode ft = t;
     TS_ASSERT_EQUALS( ft, t );
     TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size());
     TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
@@ -276,17 +276,17 @@ public:
   }
 
   void testMkFunctionTypeVectorOfArguments() {
-    Type a = d_nodeManager->mkSort();
-    Type b = d_nodeManager->mkSort();
-    Type c = d_nodeManager->mkSort();
+    TypeNode a = d_nodeManager->mkSort();
+    TypeNode b = d_nodeManager->mkSort();
+    TypeNode c = d_nodeManager->mkSort();
 
-    std::vector<Type> types;
+    std::vector<TypeNode> types;
     types.push_back(a);
     types.push_back(b);
     types.push_back(c);
 
-    Type t = d_nodeManager->mkFunctionType(types);
-    Type t2 = d_nodeManager->mkFunctionType(types);
+    TypeNode t = d_nodeManager->mkFunctionType(types);
+    TypeNode t2 = d_nodeManager->mkFunctionType(types);
 
     TS_ASSERT( !t.isBoolean() );
     TS_ASSERT( t.isFunction() );
@@ -297,7 +297,7 @@ public:
 
     TS_ASSERT_EQUALS( t, t2 );
 
-    FunctionType ft = t;
+    TypeNode ft = t;
     TS_ASSERT_EQUALS( ft, t );
     TS_ASSERT_EQUALS(ft.getArgTypes().size(), types.size()-1);
     TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
@@ -306,18 +306,18 @@ public:
   }
 
   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();
+    TypeNode a = d_nodeManager->mkSort("a");
+    TypeNode b = d_nodeManager->mkSort("b");
+    TypeNode c = d_nodeManager->mkSort("c");
+    TypeNode booleanType = d_nodeManager->booleanType();
 
-    std::vector<Type> argTypes;
+    std::vector<TypeNode> argTypes;
     argTypes.push_back(a);
     argTypes.push_back(b);
     argTypes.push_back(c);
 
-    Type t = d_nodeManager->mkPredicateType(argTypes);
-    Type t2 = d_nodeManager->mkPredicateType(argTypes);
+    TypeNode t = d_nodeManager->mkPredicateType(argTypes);
+    TypeNode t2 = d_nodeManager->mkPredicateType(argTypes);
 
     TS_ASSERT( !t.isBoolean() );
     TS_ASSERT( t.isFunction() );
@@ -328,7 +328,7 @@ public:
 
     TS_ASSERT_EQUALS( t, t2 );
 
-    FunctionType ft = t;
+    TypeNode ft = t;
     TS_ASSERT_EQUALS( ft, t );
     TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size());
     TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);