From bfa08932b23b391fafbfc18eb8033a87e802f0e1 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 21 Sep 2010 21:36:22 +0000
Subject: [PATCH] some code cleanup, documentation, review of "kinded-iterator"
 code, and addition of a unit test

---
 src/expr/node.h             | 22 ++++++++++++++----
 src/expr/node_value.h       |  8 +++++--
 test/unit/expr/node_black.h | 46 ++++++++++++++++++++++++++++++-------
 3 files changed, 61 insertions(+), 15 deletions(-)

diff --git a/src/expr/node.h b/src/expr/node.h
index 1fc583118..91c5bb21b 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -456,7 +456,7 @@ public:
 
   /**
    * Returns the iterator pointing to the end of the children (one beyond the
-   * last one.
+   * last one).
    * @return the end of the children iterator.
    */
   inline iterator end() {
@@ -468,7 +468,13 @@ public:
   }
 
   /**
-   * Returns the iterator pointing to the first child.
+   * Returns the iterator pointing to the first child, if the node's
+   * kind is the same as the template parameter, otherwise returns the
+   * iterator pointing to the node itself.  This is useful if you want
+   * to pretend to iterate over a "unary" PLUS, for instance, since
+   * unary PLUSes don't exist---begin<PLUS>() will give an iterator
+   * over the children if the node's a PLUS node, otherwise give an
+   * iterator over the node itself, as if it were a unary PLUS.
    * @return the iterator
    */
   template <Kind kind>
@@ -481,9 +487,15 @@ public:
   }
 
   /**
-   * Returns the iterator pointing to the end of the children (one beyond the
-   * last one.
-   * @return the end of the children iterator.
+   * Returns the iterator pointing to the end of the children (one
+   * beyond the last one), if the node's kind is the same as the
+   * template parameter, otherwise returns the iterator pointing to
+   * the one-of-the-node-itself.  This is useful if you want to
+   * pretend to iterate over a "unary" PLUS, for instance, since unary
+   * PLUSes don't exist---begin<PLUS>() will give an iterator over the
+   * children if the node's a PLUS node, otherwise give an iterator
+   * over the node itself, as if it were a unary PLUS.  @return the
+   * end of the children iterator.
    */
   template <Kind kind>
   inline iterator end() {
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 63121b981..2b26b273d 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -364,7 +364,9 @@ inline NodeValue::iterator<T> NodeValue::end() const {
 
 template <typename T, Kind kind>
 inline NodeValue::iterator<T> NodeValue::begin() const {
-  if (d_kind != kind) return iterator<T>(this);
+  if(d_kind != kind) {
+    return iterator<T>(this);
+  }
   NodeValue* const* firstChild = d_children;
   if(getMetaKind() == kind::metakind::PARAMETERIZED) {
     ++firstChild;
@@ -374,7 +376,9 @@ inline NodeValue::iterator<T> NodeValue::begin() const {
 
 template <typename T, Kind kind>
 inline NodeValue::iterator<T> NodeValue::end() const {
-  if (d_kind != kind) return iterator<T>(this + 1);
+  if(d_kind != kind) {
+    return iterator<T>(this + 1);
+  }
   return iterator<T>(d_children + d_nchildren);
 }
 
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index f1bb7c251..fbc308597 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -473,6 +473,7 @@ public:
 #endif /* CVC4_ASSERTIONS */
   }
 
+  // test iterators
   void testIterator() {
     NodeBuilder<> b;
     Node x = d_nodeManager->mkVar(*d_booleanType);
@@ -498,13 +499,42 @@ public:
     }
   }
 
+  // test the special "kinded-iterator"
+  void testKindedIterator() {
+    TypeNode integerType = d_nodeManager->integerType();
+
+    Node x = d_nodeManager->mkVar("x", integerType);
+    Node y = d_nodeManager->mkVar("y", integerType);
+    Node z = d_nodeManager->mkVar("z", integerType);
+    Node plus_x_y_z = d_nodeManager->mkNode(kind::PLUS, x, y, z);
+    Node x_minus_y = d_nodeManager->mkNode(kind::MINUS, x, y);
+
+    { // iterator
+      /* FAILING TEST:
+      Node::iterator i = plus_x_y_z.begin<PLUS>();
+      TS_ASSERT(*i++ == x);
+      TS_ASSERT(*i++ == y);
+      TS_ASSERT(*i++ == z);
+      TS_ASSERT(i == plus_x_y_z.end<PLUS>());
+
+      i = x.begin<PLUS>();
+      TS_ASSERT(*i++ == x);
+      TS_ASSERT(i == x.end<PLUS>());
+      */
+    }
+
+    { // same for const iterator
+      //const Node& c = plus_x_y_z;
+    }
+  }
+
   void testToString() {
     TypeNode booleanType = d_nodeManager->booleanType();
 
-    Node w = d_nodeManager->mkVar("w",booleanType);
-    Node x = d_nodeManager->mkVar("x",booleanType);
-    Node y = d_nodeManager->mkVar("y",booleanType);
-    Node z = d_nodeManager->mkVar("z",booleanType);
+    Node w = d_nodeManager->mkVar("w", booleanType);
+    Node x = d_nodeManager->mkVar("x", booleanType);
+    Node y = d_nodeManager->mkVar("y", booleanType);
+    Node z = d_nodeManager->mkVar("z", booleanType);
     Node m = NodeBuilder<>() << w << x << kind::OR;
     Node n = NodeBuilder<>() << m << y << z << kind::AND;
 
@@ -514,10 +544,10 @@ public:
   void testToStream() {
     TypeNode booleanType = d_nodeManager->booleanType();
 
-    Node w = d_nodeManager->mkVar("w",booleanType);
-    Node x = d_nodeManager->mkVar("x",booleanType);
-    Node y = d_nodeManager->mkVar("y",booleanType);
-    Node z = d_nodeManager->mkVar("z",booleanType);
+    Node w = d_nodeManager->mkVar("w", booleanType);
+    Node x = d_nodeManager->mkVar("x", booleanType);
+    Node y = d_nodeManager->mkVar("y", booleanType);
+    Node z = d_nodeManager->mkVar("z", booleanType);
     Node m = NodeBuilder<>() << x << y << kind::OR;
     Node n = NodeBuilder<>() << w << m << z << kind::AND;
     Node o = NodeBuilder<>() << n << n << kind::XOR;
-- 
2.30.2