From: Christopher L. Conway Date: Thu, 15 Apr 2010 16:56:11 +0000 (+0000) Subject: Enhancements to NodeManager tests, taking advantage of new Type implementation X-Git-Tag: cvc5-1.0.0~9113 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=74eb1c4f0f3932dcb9aeb0d8d9ac24b32fb69cec;p=cvc5.git Enhancements to NodeManager tests, taking advantage of new Type implementation --- diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 3a6b6e15a..138a87493 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -473,6 +473,9 @@ public: */ inline Type mkPredicateType(const std::vector& sorts); + /** Make a new sort. */ + inline Type mkSort(); + /** Make a new sort with the given name. */ inline Type mkSort(const std::string& name); @@ -630,6 +633,10 @@ NodeManager::mkPredicateType(const std::vector& sorts) { return Type(this, mkNodePtr(kind::FUNCTION_TYPE, sortNodes)); } +inline Type NodeManager::mkSort() { + return Type(this, mkVarPtr(kindType())); +} + inline Type NodeManager::mkSort(const std::string& name) { return Type(this, mkVarPtr(name, kindType())); } 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 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 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 ); } };