diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-04-26 21:37:34 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-04-26 21:37:34 +0000 |
commit | 3ee48833fd8cffe897a05a986c08a30d9de57213 (patch) | |
tree | db56dd28b96b12414a763ee9104adc8389225ca5 /test/unit/expr | |
parent | 96733823eadf9ff566a177cf74e19d1712c48e4b (diff) |
Adding the intermediary TypeNode to represent (and separate) the Types at the Node level.
Diffstat (limited to 'test/unit/expr')
-rw-r--r-- | test/unit/expr/attribute_black.h | 14 | ||||
-rw-r--r-- | test/unit/expr/attribute_white.h | 6 | ||||
-rw-r--r-- | test/unit/expr/node_black.h | 14 | ||||
-rw-r--r-- | test/unit/expr/node_builder_black.h | 4 | ||||
-rw-r--r-- | test/unit/expr/node_manager_black.h | 72 |
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); |