diff options
Diffstat (limited to 'test/unit/expr')
-rw-r--r-- | test/unit/expr/node_black.h | 32 |
1 files changed, 28 insertions, 4 deletions
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index aa99c70c4..c5a2bb609 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -15,18 +15,42 @@ #include <cxxtest/TestSuite.h> +#include "expr/node_manager.h" #include "expr/node.h" using namespace CVC4; +using namespace std; class NodeBlack : public CxxTest::TestSuite { +private: + + NodeManagerScope *d_scope; + NodeManager *d_nm; + public: - void testNull() { - Node::null(); + void setUp() { + d_nm = new NodeManager(); + d_scope = new NodeManagerScope(d_nm); + } + + void tearDown(){ + delete d_nm; + delete d_scope; } - void testCopyCtor() { - Node e(Node::null()); + void testEqExpr(){ + /*Node eqExpr(const Node& right) const;*/ + Node left = d_nm->mkNode(TRUE); + Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + + Node eq = left.eqExpr(right); + + Node first = *(eq.begin()); + Node second = *(eq.begin()++); + + TS_ASSERT(first.getKind() == NULL); + TS_ASSERT(second.getKind() == NULL); } + }; |