NodeSelfIterator implementation and unit test (resolves bug #204); also fix ParserBlack unit test initialization

7 files changed, 261 insertions, 18 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 50ce4141e..d2b9197cb 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -27,7 +27,7 @@ libexpr_la_SOURCES = \
 	declaration_scope.h \
 	declaration_scope.cpp \
 	expr_manager_scope.h \
-	sort.h
+	node_self_iterator.h
 nodist_libexpr_la_SOURCES = \
 	kind.h \
 	metakind.h \
diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h
new file mode 100644
index 000000000..c38243b0a
--- /dev/null
+++ b/src/expr/node_self_iterator.h
@@ -0,0 +1,130 @@
+/*********************                                                        */
+/*! \file node_self_iterator.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Iterator supporting Node "self-iteration"
+ **
+ ** Iterator supporting Node "self-iteration."
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__EXPR__NODE_SELF_ITERATOR_H
+#define __CVC4__EXPR__NODE_SELF_ITERATOR_H
+
+#include <iterator>
+
+#include "util/Assert.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace expr {
+
+class NodeSelfIterator : std::iterator<std::input_iterator_tag, Node> {
+  Node d_node;
+  Node::const_iterator d_child;
+
+public:
+  static NodeSelfIterator self(TNode n);
+  static NodeSelfIterator selfEnd(TNode n);
+
+  NodeSelfIterator();
+  NodeSelfIterator(Node n);
+  NodeSelfIterator(TNode n);
+  NodeSelfIterator(const NodeSelfIterator& i);
+
+  NodeSelfIterator(Node::const_iterator i);
+  NodeSelfIterator(TNode::const_iterator i);
+
+  Node operator*() const;
+  NodeSelfIterator& operator++();
+  NodeSelfIterator operator++(int);
+
+  bool operator==(NodeSelfIterator i) const;
+  bool operator!=(NodeSelfIterator i) const;
+
+};/* class NodeSelfIterator */
+
+inline NodeSelfIterator NodeSelfIterator::self(TNode n) {
+  Assert(!n.isNull(), "Self-iteration over null nodes not permitted.");
+  return NodeSelfIterator(n);
+}
+
+inline NodeSelfIterator NodeSelfIterator::selfEnd(TNode n) {
+  Assert(!n.isNull(), "Self-iteration over null nodes not permitted.");
+  return NodeSelfIterator(n.end());
+}
+
+inline NodeSelfIterator::NodeSelfIterator() :
+  d_node(),
+  d_child() {
+}
+
+inline NodeSelfIterator::NodeSelfIterator(Node node) :
+  d_node(node),
+  d_child() {
+  Assert(!node.isNull(), "Self-iteration over null nodes not permitted.");
+}
+
+inline NodeSelfIterator::NodeSelfIterator(TNode node) :
+  d_node(node),
+  d_child() {
+  Assert(!node.isNull(), "Self-iteration over null nodes not permitted.");
+}
+
+inline NodeSelfIterator::NodeSelfIterator(const NodeSelfIterator& i) :
+  d_node(i.d_node),
+  d_child(i.d_child) {
+}
+
+inline NodeSelfIterator::NodeSelfIterator(Node::const_iterator i) :
+  d_node(),
+  d_child(i) {
+}
+
+inline NodeSelfIterator::NodeSelfIterator(TNode::const_iterator i) :
+  d_node(),
+  d_child(i) {
+}
+
+inline Node NodeSelfIterator::operator*() const {
+  return d_node.isNull() ? *d_child : d_node;
+}
+
+inline NodeSelfIterator& NodeSelfIterator::operator++() {
+  if(d_node.isNull()) {
+    ++d_child;
+  } else {
+    d_child = d_node.end();
+    d_node = Node::null();
+  }
+  return *this;
+}
+
+inline NodeSelfIterator NodeSelfIterator::operator++(int) {
+  NodeSelfIterator i = *this;
+  ++*this;
+  return i;
+}
+
+inline bool NodeSelfIterator::operator==(NodeSelfIterator i) const {
+  return d_node == i.d_node && d_child == i.d_child;
+}
+
+inline bool NodeSelfIterator::operator!=(NodeSelfIterator i) const {
+  return !(*this == i);
+}
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR__NODE_SELF_ITERATOR_H */
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 658cb1e2d..b91196559 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -119,11 +119,8 @@ class NodeValue {
 
   static size_t next_id;
 
-public:
   /**
-   * Uninitializing constructor for NodeBuilder's use.  This is
-   * somewhat dangerous, but must also be public for the
-   * makeStackNodeBuilder() macro to work.
+   * Uninitializing constructor for NodeBuilder's use.
    */
   NodeValue() { /* do not initialize! */ }
 
@@ -140,10 +137,11 @@ private:
   const_nv_iterator nv_begin() const;
   const_nv_iterator nv_end() const;
 
-  template <typename T>
+  template <class T>
   class iterator {
     const_nv_iterator d_i;
   public:
+    typedef std::random_access_iterator_tag iterator_category;
     typedef T value_type;
     typedef ptrdiff_t difference_type;
     typedef T* pointer;
@@ -152,13 +150,18 @@ private:
     iterator() : d_i(NULL) {}
     explicit iterator(const_nv_iterator i) : d_i(i) {}
 
-    inline T operator*();
+    // conversion of a TNode iterator to a Node iterator
+    inline operator NodeValue::iterator<NodeTemplate<true> >() {
+      return iterator<NodeTemplate<true> >(d_i);
+    }
+
+    inline T operator*() const;
 
-    bool operator==(const iterator& i) {
+    bool operator==(const iterator& i) const {
       return d_i == i.d_i;
     }
 
-    bool operator!=(const iterator& i) {
+    bool operator!=(const iterator& i) const {
       return d_i != i.d_i;
     }
 
@@ -201,8 +204,6 @@ private:
     difference_type operator-(iterator i) {
       return d_i - i.d_i;
     }
-
-    typedef std::random_access_iterator_tag iterator_category;
   };/* class NodeValue::iterator<T> */
 
   // operator+ (as a function) cannot be a template, so we have to
@@ -440,7 +441,7 @@ namespace CVC4 {
 namespace expr {
 
 template <typename T>
-inline T NodeValue::iterator<T>::operator*() {
+inline T NodeValue::iterator<T>::operator*() const {
   return T(*d_i);
 }
 
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 059d1d163..83dc888d4 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -16,6 +16,7 @@ UNIT_TESTS = \
 	expr/attribute_white \
 	expr/attribute_black \
 	expr/declaration_scope_black \
+	expr/node_self_iterator_black \
 	parser/parser_black \
 	parser/parser_builder_black \
 	prop/cnf_stream_black \
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 6c5d8888f..5389e1308 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -39,8 +39,8 @@ private:
   Context* d_ctxt;
   NodeManager* d_nodeManager;
   NodeManagerScope* d_scope;
-  TypeNode *d_booleanType;
-  TypeNode *d_realType;
+  TypeNode* d_booleanType;
+  TypeNode* d_realType;
 
 public:
 
diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h
new file mode 100644
index 000000000..5627a9db5
--- /dev/null
+++ b/test/unit/expr/node_self_iterator_black.h
@@ -0,0 +1,81 @@
+/*********************                                                        */
+/*! \file node_self_iterator_black.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::expr::NodeSelfIterator
+ **
+ ** Black box testing of CVC4::expr::NodeSelfIterator
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "context/context.h"
+#include "expr/node.h"
+#include "expr/node_self_iterator.h"
+#include "expr/node_builder.h"
+#include "expr/convenience_node_builders.h"
+
+using namespace CVC4;
+using namespace CVC4::context;
+using namespace CVC4::kind;
+using namespace CVC4::expr;
+using namespace std;
+
+class NodeSelfIteratorBlack : public CxxTest::TestSuite {
+private:
+
+  Context* d_ctxt;
+  NodeManager* d_nodeManager;
+  NodeManagerScope* d_scope;
+  TypeNode* d_booleanType;
+  TypeNode* d_realType;
+
+public:
+
+  void setUp() {
+    d_ctxt = new Context;
+    d_nodeManager = new NodeManager(d_ctxt);
+    d_scope = new NodeManagerScope(d_nodeManager);
+    d_booleanType = new TypeNode(d_nodeManager->booleanType());
+    d_realType = new TypeNode(d_nodeManager->realType());
+  }
+
+  void tearDown() {
+    delete d_booleanType;
+    delete d_scope;
+    delete d_nodeManager;
+    delete d_ctxt;
+  }
+
+  void testSelfIteration() {
+    Node x = d_nodeManager->mkVar("x", *d_booleanType);
+    Node y = d_nodeManager->mkVar("y", *d_booleanType);
+    Node x_and_y = x && y;
+    NodeSelfIterator i = x_and_y, j = NodeSelfIterator::self(x_and_y);
+    TS_ASSERT(i != x_and_y.end());
+    TS_ASSERT(j != x_and_y.end());
+    TS_ASSERT(*i == x_and_y);
+    TS_ASSERT(*j == x_and_y);
+    TS_ASSERT(*i++ == x_and_y);
+    TS_ASSERT(*j++ == x_and_y);
+    TS_ASSERT(i == NodeSelfIterator::selfEnd(x_and_y));
+    TS_ASSERT(j == NodeSelfIterator::selfEnd(x_and_y));
+    TS_ASSERT(i == x_and_y.end());
+    TS_ASSERT(j == x_and_y.end());
+    i = x_and_y.begin();
+    TS_ASSERT(i != x_and_y.end());
+    TS_ASSERT(*i == x);
+    TS_ASSERT(*++i == y);
+    TS_ASSERT(++i == x_and_y.end());
+  }
+
+};
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 0e0835327..88a6eaf57 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -169,21 +169,33 @@ protected:
   }
 
   ParserBlack(InputLanguage lang) :
-    d_lang(lang),
-    d_exprManager(new ExprManager()) {
+    d_lang(lang) {
   }
 
-public:
-  virtual ~ParserBlack() {
+  void setUp() {
+cout << "SET UP\n";
+    d_exprManager = new ExprManager;
+  }
+
+  void tearDown() {
     delete d_exprManager;
   }
 };
 
 class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack  {
+  typedef ParserBlack super;
 
 public:
   Cvc4ParserTest() : ParserBlack(LANG_CVC4) { }
 
+  void setUp() {
+    super::setUp();
+  }
+
+  void tearDown() {
+    super::tearDown();
+  }
+
   void testGoodCvc4Inputs() {
     tryGoodInput(""); // empty string is OK
     tryGoodInput("ASSERT TRUE;");
@@ -228,9 +240,19 @@ public:
 };
 
 class SmtParserTest : public CxxTest::TestSuite, public ParserBlack {
+  typedef ParserBlack super;
+
 public:
   SmtParserTest() : ParserBlack(LANG_SMTLIB) { }
 
+  void setUp() {
+    super::setUp();
+  }
+
+  void tearDown() {
+    super::tearDown();
+  }
+
   void testGoodSmtInputs() {
     tryGoodInput(""); // empty string is OK
     tryGoodInput("(benchmark foo :assumption true)");
@@ -286,6 +308,14 @@ class Smt2ParserTest : public CxxTest::TestSuite, public ParserBlack {
 public:
   Smt2ParserTest() : ParserBlack(LANG_SMTLIB_V2) { }
 
+  void setUp() {
+    super::setUp();
+  }
+
+  void tearDown() {
+    super::tearDown();
+  }
+
   void setupContext(Smt2& parser) {
     parser.addTheory(Smt2::THEORY_CORE);
     super::setupContext(parser);