summaryrefslogtreecommitdiff
path: root/test/unit/expr
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/expr')
-rw-r--r--test/unit/expr/attribute_black.h14
-rw-r--r--test/unit/expr/attribute_white.h23
-rw-r--r--test/unit/expr/declaration_scope_black.h20
-rw-r--r--test/unit/expr/expr_public.h22
-rw-r--r--test/unit/expr/node_black.h40
-rw-r--r--test/unit/expr/node_builder_black.h27
-rw-r--r--test/unit/expr/node_manager_black.h106
7 files changed, 126 insertions, 126 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 );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback