make Node iterators more STL-friendly, resolves bug #196

diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 9f8a8f45b3df2625fbd9f02928fa6d36b8be2c3a..3c21777ed55dc2f7a96699f33c5faf2a4fa3838c 100644 (file)
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -144,6 +144,12 @@ private:
   class iterator {
     const_nv_iterator d_i;
   public:
+    typedef T value_type;
+    typedef ptrdiff_t difference_type;
+    typedef T* pointer;
+    typedef T& reference;
+
+    iterator() : d_i(NULL) {}
     explicit iterator(const_nv_iterator i) : d_i(i) {}
 
     inline T operator*();

diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index 9ffd2d09407d8ea45ebdc9535bf7a3507ee62ff2..74413796a6a7d9edc1345ffa508a92f43ef7e781 100644 (file)
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -68,4 +68,39 @@ public:
     TS_ASSERT_EQUALS(b.d_nv->d_nchildren, 0u);
     /* etc. */
   }
+
+  void testIterators() {
+    Node x = d_nm->mkVar("x", d_nm->integerType());
+    Node y = d_nm->mkVar("y", d_nm->integerType());
+    Node x_plus_y = d_nm->mkNode(PLUS, x, y);
+    Node two = d_nm->mkConst(Integer(2));
+    Node x_times_2 = d_nm->mkNode(MULT, x, two);
+
+    Node n = d_nm->mkNode(PLUS, x_times_2, x_plus_y, y);
+
+    Node::iterator i;
+
+    i = find(n.begin(), n.end(), x_plus_y);
+    TS_ASSERT(i != n.end());
+    TS_ASSERT(*i == x_plus_y);
+
+    i = find(n.begin(), n.end(), x);
+    TS_ASSERT(i == n.end());
+
+    i = find(x_times_2.begin(), x_times_2.end(), two);
+    TS_ASSERT(i != x_times_2.end());
+    TS_ASSERT(*i == two);
+
+    i = find(n.begin(), n.end(), y);
+    TS_ASSERT(i != n.end());
+    TS_ASSERT(*i == y);
+
+    vector<Node> v;
+    copy(n.begin(), n.end(), back_inserter(v));
+    TS_ASSERT(n.getNumChildren() == v.size());
+    TS_ASSERT(3 == v.size());
+    TS_ASSERT(v[0] == x_times_2);
+    TS_ASSERT(v[1] == x_plus_y);
+    TS_ASSERT(v[2] == y);
+  }
 };