From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 13 Sep 2010 23:35:30 +0000 (+0000)
Subject: make Node iterators more STL-friendly, resolves bug #196
X-Git-Tag: cvc5-1.0.0~8868
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bd9eb727cd4897a8dbb80ea730082886ce1c18e4;p=cvc5.git

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

diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 9f8a8f45b..3c21777ed 100644
--- 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 9ffd2d094..74413796a 100644
--- 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);
+  }
 };