summaryrefslogtreecommitdiff
path: root/test/unit/expr/node_manager_black.h
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/expr/node_manager_black.h')
-rw-r--r--test/unit/expr/node_manager_black.h152
1 files changed, 90 insertions, 62 deletions
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index 873e28bb3..118ba8173 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -49,7 +49,7 @@ public:
delete d_context;
}
- void testMkNode1() {
+ void testMkNodeNot() {
Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(NOT, x);
TS_ASSERT_EQUALS( n.getNumChildren(), 1u );
@@ -57,7 +57,7 @@ public:
TS_ASSERT_EQUALS( n[0], x);
}
- void testMkNode2() {
+ void testMkNodeBinary() {
Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType());
Node y = d_nodeManager->mkVar("y",d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(IMPLIES, x, y);
@@ -67,7 +67,7 @@ public:
TS_ASSERT_EQUALS( n[1], y);
}
- void testMkNode3() {
+ void testMkNodeThreeChildren() {
Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType());
Node y = d_nodeManager->mkVar("y",d_nodeManager->booleanType());
Node z = d_nodeManager->mkVar("z",d_nodeManager->booleanType());
@@ -79,7 +79,7 @@ public:
TS_ASSERT_EQUALS( n[2], z);
}
- void testMkNode4() {
+ void testMkNodeFourChildren() {
Node x1 = d_nodeManager->mkVar("x1",d_nodeManager->booleanType());
Node x2 = d_nodeManager->mkVar("x2",d_nodeManager->booleanType());
Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType());
@@ -93,7 +93,7 @@ public:
TS_ASSERT_EQUALS( n[3], x4 );
}
- void testMkNode5() {
+ void testMkNodeFiveChildren() {
Node x1 = d_nodeManager->mkVar("x1",d_nodeManager->booleanType());
Node x2 = d_nodeManager->mkVar("x2",d_nodeManager->booleanType());
Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType());
@@ -109,7 +109,7 @@ public:
TS_ASSERT_EQUALS( n[4], x5);
}
- void testMkNodeVecOfNode() {
+ void testMkNodeVectorOfNodeChildren() {
Node x1 = d_nodeManager->mkVar("x1",d_nodeManager->booleanType());
Node x2 = d_nodeManager->mkVar("x2",d_nodeManager->booleanType());
Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType());
@@ -125,7 +125,7 @@ public:
}
}
- void testMkNodeVecOfTNode() {
+ void testMkNodeVectorOfTNodeChildren() {
Node x1 = d_nodeManager->mkVar("x1",d_nodeManager->booleanType());
Node x2 = d_nodeManager->mkVar("x2",d_nodeManager->booleanType());
Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType());
@@ -141,7 +141,7 @@ public:
}
}
- void testMkVar1() {
+ void testMkVarWithNoName() {
Type booleanType = d_nodeManager->booleanType();
Node x = d_nodeManager->mkVar(booleanType);
TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
@@ -149,7 +149,7 @@ public:
TS_ASSERT_EQUALS(x.getType(),booleanType);
}
- void testMkVar2() {
+ void testMkVarWithName() {
Type booleanType = d_nodeManager->booleanType();
Node x = d_nodeManager->mkVar("x", booleanType);
TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
@@ -187,76 +187,98 @@ public:
}
void testBooleanType() {
- 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 );
+ Type t = d_nodeManager->booleanType();
+ Type t2 = d_nodeManager->booleanType();
+ Type t3 = d_nodeManager->mkSort("T");
+ TS_ASSERT( t.isBoolean() );
+ TS_ASSERT( !t.isFunction() );
+ TS_ASSERT( !t.isKind() );
+ TS_ASSERT( !t.isNull() );
+ TS_ASSERT( !t.isPredicate() );
+ TS_ASSERT( !t.isSort() );
+ TS_ASSERT_EQUALS(t, t2);
+ TS_ASSERT( t != t3 );
+
+ BooleanType bt = t;
+ TS_ASSERT_EQUALS( bt, t);
}
void testKindType() {
- 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)
+ Type t = d_nodeManager->kindType();
+ Type t2 = d_nodeManager->kindType();
+ Type t3 = d_nodeManager->mkSort("T");
+
+ TS_ASSERT( !t.isBoolean() );
+ TS_ASSERT( !t.isFunction() );
+ TS_ASSERT( t.isKind() );
+ TS_ASSERT( !t.isNull() );
+ TS_ASSERT( !t.isPredicate() );
+ TS_ASSERT( !t.isSort() );
+
+ TS_ASSERT_EQUALS(t, t2);
+ TS_ASSERT( t != t3);
+
+ KindType kt = t;
+ TS_ASSERT_EQUALS( kt, t );
+ // TODO: Is there a way to get the type of otherType (it should == t)?
}
- /* TODO: All of the type comparisons in all of the following tests are
- * strictly for pointer equality. This is too weak for disequalities and
- * too strong for equalities! Also, it means we can't really check for
- * structural equality between two identical calls to mkFunctionType (see
- * the commented out assertions at the bottom of each test). Unfortunately,
- * with the current type implementation it's the best we can do. */
-
- void testMkFunctionType2() {
+ void testMkFunctionTypeBoolToBool() {
Type booleanType = d_nodeManager->booleanType();
Type t = d_nodeManager->mkFunctionType(booleanType,booleanType);
- TS_ASSERT( t != booleanType );
+ Type t2 = d_nodeManager->mkFunctionType(booleanType,booleanType);
+
+ TS_ASSERT( !t.isBoolean() );
TS_ASSERT( t.isFunction() );
+ TS_ASSERT( !t.isKind() );
+ TS_ASSERT( !t.isNull() );
+ TS_ASSERT( t.isPredicate() );
+ TS_ASSERT( !t.isSort() );
- FunctionType ft = (FunctionType)t;
+ TS_ASSERT_EQUALS( t, t2 );
+
+ FunctionType ft = t;
+ TS_ASSERT_EQUALS( ft, 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");
+ void testMkFunctionTypeVectorOfArgsWithReturnType() {
+ Type a = d_nodeManager->mkSort();
+ Type b = d_nodeManager->mkSort();
+ Type c = d_nodeManager->mkSort();
std::vector<Type> argTypes;
argTypes.push_back(a);
argTypes.push_back(b);
Type t = d_nodeManager->mkFunctionType(argTypes,c);
+ Type t2 = d_nodeManager->mkFunctionType(argTypes,c);
- TS_ASSERT( t != a );
- TS_ASSERT( t != b );
- TS_ASSERT( t != c );
+ TS_ASSERT( !t.isBoolean() );
TS_ASSERT( t.isFunction() );
+ TS_ASSERT( !t.isKind() );
+ TS_ASSERT( !t.isNull() );
+ TS_ASSERT( !t.isPredicate() );
+ TS_ASSERT( !t.isSort() );
+
+ TS_ASSERT_EQUALS( t, t2 );
- FunctionType ft = (FunctionType)t;
+ FunctionType ft = t;
+ TS_ASSERT_EQUALS( ft, 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");
+ void testMkFunctionTypeVectorOfArguments() {
+ Type a = d_nodeManager->mkSort();
+ Type b = d_nodeManager->mkSort();
+ Type c = d_nodeManager->mkSort();
std::vector<Type> types;
types.push_back(a);
@@ -264,20 +286,23 @@ public:
types.push_back(c);
Type t = d_nodeManager->mkFunctionType(types);
+ Type t2 = d_nodeManager->mkFunctionType(types);
- TS_ASSERT( t != a );
- TS_ASSERT( t != b );
- TS_ASSERT( t != c );
+ TS_ASSERT( !t.isBoolean() );
TS_ASSERT( t.isFunction() );
+ TS_ASSERT( !t.isKind() );
+ TS_ASSERT( !t.isNull() );
+ TS_ASSERT( !t.isPredicate() );
+ TS_ASSERT( !t.isSort() );
- FunctionType ft = (FunctionType)t;
+ TS_ASSERT_EQUALS( t, t2 );
+
+ FunctionType ft = t;
+ TS_ASSERT_EQUALS( ft, 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() {
@@ -292,21 +317,24 @@ public:
argTypes.push_back(c);
Type t = d_nodeManager->mkPredicateType(argTypes);
+ Type t2 = d_nodeManager->mkPredicateType(argTypes);
- TS_ASSERT( t != a );
- TS_ASSERT( t != b );
- TS_ASSERT( t != c );
- TS_ASSERT( t != booleanType );
+ TS_ASSERT( !t.isBoolean() );
TS_ASSERT( t.isFunction() );
+ TS_ASSERT( !t.isKind() );
+ TS_ASSERT( !t.isNull() );
+ TS_ASSERT( t.isPredicate() );
+ TS_ASSERT( !t.isSort() );
+
+ TS_ASSERT_EQUALS( t, t2 );
- FunctionType ft = (FunctionType)t;
+ FunctionType ft = t;
+ TS_ASSERT_EQUALS( ft, 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