diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/expr/attribute_black.h | 14 | ||||
-rw-r--r-- | test/unit/expr/attribute_white.h | 23 | ||||
-rw-r--r-- | test/unit/expr/declaration_scope_black.h | 20 | ||||
-rw-r--r-- | test/unit/expr/expr_public.h | 22 | ||||
-rw-r--r-- | test/unit/expr/node_black.h | 40 | ||||
-rw-r--r-- | test/unit/expr/node_builder_black.h | 27 | ||||
-rw-r--r-- | test/unit/expr/node_manager_black.h | 106 | ||||
-rw-r--r-- | test/unit/parser/parser_white.h | 18 | ||||
-rw-r--r-- | test/unit/theory/theory_black.h | 4 | ||||
-rw-r--r-- | test/unit/theory/theory_uf_white.h | 25 |
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); |