From bfab2bde219a0cda230fb2f26d89d123918a219f Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Thu, 25 Feb 2010 22:32:03 +0000 Subject: Adding Node::getOperator() Removing references to ExprManager from Type, moving Type creation into NodeManager --- test/unit/expr/node_black.h | 98 +++++++++++++++++++++++++++------------------ 1 file changed, 59 insertions(+), 39 deletions(-) (limited to 'test/unit/expr/node_black.h') diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 4731810ea..90358a622 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -18,6 +18,7 @@ //Used in some of the tests #include +#include "expr/expr_manager.h" #include "expr/node_value.h" #include "expr/node_builder.h" #include "expr/node_manager.h" @@ -30,19 +31,19 @@ using namespace std; class NodeBlack : public CxxTest::TestSuite { private: + NodeManager *d_nodeManager; NodeManagerScope *d_scope; - NodeManager *d_nm; public: void setUp() { - d_nm = new NodeManager(); - d_scope = new NodeManagerScope(d_nm); + d_nodeManager = new NodeManager(); + d_scope = new NodeManagerScope(d_nodeManager); } void tearDown() { delete d_scope; - delete d_nm; + delete d_nodeManager; } bool imp(bool a, bool b) const { @@ -88,12 +89,12 @@ public: void testOperatorEquals() { Node a, b, c; - b = d_nm->mkVar(); + b = d_nodeManager->mkVar(); a = b; c = a; - Node d = d_nm->mkVar(); + Node d = d_nodeManager->mkVar(); TS_ASSERT(a==a); TS_ASSERT(a==b); @@ -128,12 +129,12 @@ public: Node a, b, c; - b = d_nm->mkVar(); + b = d_nodeManager->mkVar(); a = b; c = a; - Node d = d_nm->mkVar(); + Node d = d_nodeManager->mkVar(); /*structed assuming operator == works */ TS_ASSERT(iff(a!=a,!(a==a))); @@ -168,9 +169,9 @@ public: #endif /* CVC4_ASSERTIONS */ //Basic access check - Node tb = d_nm->mkNode(TRUE); - Node eb = d_nm->mkNode(FALSE); - Node cnd = d_nm->mkNode(XOR, tb, eb); + Node tb = d_nodeManager->mkNode(TRUE); + Node eb = d_nodeManager->mkNode(FALSE); + Node cnd = d_nodeManager->mkNode(XOR, tb, eb); Node ite = cnd.iteNode(tb,eb); TS_ASSERT(tb == cnd[0]); @@ -190,7 +191,7 @@ public: /*tests: Node& operator=(const Node&); */ void testOperatorAssign() { Node a, b; - Node c = d_nm->mkNode(NOT); + Node c = d_nodeManager->mkNode(NOT); b = c; TS_ASSERT(b==c); @@ -208,14 +209,14 @@ public: */ - Node a = d_nm->mkVar(); - Node b = d_nm->mkVar(); + Node a = d_nodeManager->mkVar(); + Node b = d_nodeManager->mkVar(); TS_ASSERT(amkNode(NULL_EXPR); - Node d = d_nm->mkNode(NULL_EXPR); + Node c = d_nodeManager->mkNode(NULL_EXPR); + Node d = d_nodeManager->mkNode(NULL_EXPR); TS_ASSERT(!(cmkNode(TRUE); - Node parent = d_nm->mkNode(NOT, child); + Node child = d_nodeManager->mkNode(TRUE); + Node parent = d_nodeManager->mkNode(NOT, child); TS_ASSERT(child < parent); //Slightly less simple test of DD property. std::vector chain; int N = 500; - Node curr = d_nm->mkNode(NULL_EXPR); + Node curr = d_nodeManager->mkNode(NULL_EXPR); for(int i=0;imkNode(AND,curr); + curr = d_nodeManager->mkNode(AND,curr); } for(int i=0;imkNode(ITE); - Node b = d_nm->mkNode(ITE); + Node a = d_nodeManager->mkNode(ITE); + Node b = d_nodeManager->mkNode(ITE); TS_ASSERT(b.hash() == a.hash()); } @@ -265,8 +266,8 @@ public: void testEqNode() { /*Node eqNode(const Node& right) const;*/ - Node left = d_nm->mkNode(TRUE); - Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node left = d_nodeManager->mkNode(TRUE); + Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); Node eq = left.eqNode(right); @@ -280,7 +281,7 @@ public: void testNotNode() { /* Node notNode() const;*/ - Node child = d_nm->mkNode(TRUE); + Node child = d_nodeManager->mkNode(TRUE); Node parent = child.notNode(); TS_ASSERT(NOT == parent.getKind()); @@ -292,8 +293,8 @@ public: void testAndNode() { /*Node andNode(const Node& right) const;*/ - Node left = d_nm->mkNode(TRUE); - Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node left = d_nodeManager->mkNode(TRUE); + Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); Node eq = left.andNode(right); @@ -308,8 +309,8 @@ public: void testOrNode() { /*Node orNode(const Node& right) const;*/ - Node left = d_nm->mkNode(TRUE); - Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node left = d_nodeManager->mkNode(TRUE); + Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); Node eq = left.orNode(right); @@ -324,9 +325,9 @@ public: void testIteNode() { /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/ - Node cnd = d_nm->mkNode(PLUS); - Node thenBranch = d_nm->mkNode(TRUE); - Node elseBranch = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node cnd = d_nodeManager->mkNode(PLUS); + Node thenBranch = d_nodeManager->mkNode(TRUE); + Node elseBranch = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); Node ite = cnd.iteNode(thenBranch,elseBranch); @@ -341,8 +342,8 @@ public: void testIffNode() { /* Node iffNode(const Node& right) const; */ - Node left = d_nm->mkNode(TRUE); - Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node left = d_nodeManager->mkNode(TRUE); + Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); Node eq = left.iffNode(right); @@ -356,8 +357,8 @@ public: void testImpNode() { /* Node impNode(const Node& right) const; */ - Node left = d_nm->mkNode(TRUE); - Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node left = d_nodeManager->mkNode(TRUE); + Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); Node eq = left.impNode(right); @@ -370,8 +371,8 @@ public: void testXorNode() { /*Node xorNode(const Node& right) const;*/ - Node left = d_nm->mkNode(TRUE); - Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node left = d_nodeManager->mkNode(TRUE); + Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); Node eq = left.xorNode(right); @@ -383,7 +384,7 @@ public: } void testKindSingleton(Kind k) { - Node n = d_nm->mkNode(k); + Node n = d_nodeManager->mkNode(k); TS_ASSERT(k == n.getKind()); } @@ -395,6 +396,25 @@ public: testKindSingleton(ITE); testKindSingleton(SKOLEM); } + + + void testGetOperator() { + const Type* sort = d_nodeManager->mkSort("T"); + const Type* booleanType = d_nodeManager->booleanType(); + const Type* predType = d_nodeManager->mkFunctionType(sort,booleanType); + + Node f = d_nodeManager->mkVar(predType); + Node a = d_nodeManager->mkVar(booleanType); + Node fa = d_nodeManager->mkNode(kind::APPLY,f,a); + + TS_ASSERT( fa.hasOperator() ); + TS_ASSERT( !f.hasOperator() ); + TS_ASSERT( !a.hasOperator() ); + + TS_ASSERT( f == fa.getOperator() ); + TS_ASSERT_THROWS( f.getOperator(), AssertionException ); + TS_ASSERT_THROWS( a.getOperator(), AssertionException ); + } void testNaryExpForSize(Kind k, int N){ NodeBuilder<> nbz(k); -- cgit v1.2.3