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

1 files changed, 36 insertions, 36 deletions

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);