diff options
author | Tim King <taking@cs.nyu.edu> | 2010-01-26 17:55:28 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-01-26 17:55:28 +0000 |
commit | aaecc4532bb39f7e5c35f6f11c6eb5962ad4016d (patch) | |
tree | 52a64b831c618a356e4873b99e41771d399f4d90 /test/unit/expr | |
parent | b3d0ea6ed6d92943d9a52abbe30e944e9887516d (diff) |
Added test/regress/boolean.cvc
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); } + }; |