Added test/regress/boolean.cvc

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);
   }
+
 };