diff options
Diffstat (limited to 'test/unit/expr/node_black.h')
-rw-r--r-- | test/unit/expr/node_black.h | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index c92ea31f5..0b46b06ce 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -174,8 +174,8 @@ public: #endif /* CVC4_ASSERTIONS */ //Basic access check - Node tb = d_nodeManager->mkNode(TRUE); - Node eb = d_nodeManager->mkNode(FALSE); + Node tb = d_nodeManager->mkConst(true); + Node eb = d_nodeManager->mkConst(false); Node cnd = d_nodeManager->mkNode(XOR, tb, eb); Node ite = cnd.iteNode(tb, eb); @@ -232,7 +232,7 @@ public: */ // simple test of descending descendant property - Node child = d_nodeManager->mkNode(TRUE); + Node child = d_nodeManager->mkConst(true); Node parent = d_nodeManager->mkNode(NOT, child); TS_ASSERT(child < parent); @@ -259,8 +259,8 @@ public: void testEqNode() { /* Node eqNode(const Node& right) const; */ - Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, d_nodeManager->mkNode(FALSE)); + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, d_nodeManager->mkConst(false)); Node eq = left.eqNode(right); TS_ASSERT(EQUAL == eq.getKind()); @@ -273,7 +273,7 @@ public: void testNotNode() { /* Node notNode() const; */ - Node child = d_nodeManager->mkNode(TRUE); + Node child = d_nodeManager->mkConst(true); Node parent = child.notNode(); TS_ASSERT(NOT == parent.getKind()); @@ -285,8 +285,8 @@ public: void testAndNode() { /*Node andNode(const Node& right) const;*/ - Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.andNode(right); @@ -301,8 +301,8 @@ public: void testOrNode() { /*Node orNode(const Node& right) const;*/ - Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.orNode(right); @@ -321,8 +321,8 @@ public: Node b = d_nodeManager->mkVar(); Node cnd = d_nodeManager->mkNode(PLUS, a, b); - Node thenBranch = d_nodeManager->mkNode(TRUE); - Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkNode(FALSE)); + Node thenBranch = d_nodeManager->mkConst(true); + Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkConst(false)); Node ite = cnd.iteNode(thenBranch, elseBranch); TS_ASSERT(ITE == ite.getKind()); @@ -336,8 +336,8 @@ public: void testIffNode() { /* Node iffNode(const Node& right) const; */ - Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.iffNode(right); @@ -351,8 +351,8 @@ public: void testImpNode() { /* Node impNode(const Node& right) const; */ - Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.impNode(right); @@ -365,8 +365,8 @@ public: void testXorNode() { /*Node xorNode(const Node& right) const;*/ - Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.xorNode(right); @@ -422,7 +422,7 @@ public: void testNaryExpForSize(Kind k, int N) { NodeBuilder<> nbz(k); - Node trueNode = d_nodeManager->mkNode(TRUE); + Node trueNode = d_nodeManager->mkConst(true); for(int i = 0; i < N; ++i) { nbz << trueNode; } @@ -433,7 +433,7 @@ public: void testNumChildren() { /*inline size_t getNumChildren() const;*/ - Node trueNode = d_nodeManager->mkNode(TRUE); + Node trueNode = d_nodeManager->mkConst(true); //test 0 TS_ASSERT(0 == (Node::null()).getNumChildren()); |