Add reverse iterators to `Node`/`TNode` (#6825)

This feature is useful for example for succinctly inserting children of
a node in the reverse order. To make this work, the commit fixes the
declaration of `reference` in the `NodeValue::iterator`. The
`std::reverse_iterator` adapter expects the `reference` type to match
the return type of `operator*` in the corresponding iterator (as
mandated by the standard). Despite its name, `reference` does not have
to be a C++ reference. Note that we cannot actually make it a C++
reference because `NodeValue::iterator` wraps the `NodeValue*` in a
`Node`/`TNode` in `operator*`.

diff --git a/src/expr/node.h b/src/expr/node.h
index 5f5d3a976e2d4b55cfcd0e1ba7e1449b068ebec0..a406b3d13df5ef9173500af14620fdd95373b3f7 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -605,7 +605,14 @@ public:
   /** Iterator allowing for scanning through the children. */
   typedef typename expr::NodeValue::iterator< NodeTemplate<ref_count> > iterator;
   /** Constant iterator allowing for scanning through the children. */
-  typedef typename expr::NodeValue::iterator< NodeTemplate<ref_count> > const_iterator;
+  using const_iterator =
+      typename expr::NodeValue::iterator<NodeTemplate<ref_count>>;
+  /**
+   * Reverse constant iterator allowing for scanning through the children in
+   * reverse order.
+   */
+  using const_reverse_iterator = std::reverse_iterator<
+      typename expr::NodeValue::iterator<NodeTemplate<ref_count>>>;
 
   class kinded_iterator {
     friend class NodeTemplate<ref_count>;
@@ -729,7 +736,8 @@ public:
    * Returns the const_iterator pointing to the first child.
    * @return the const_iterator
    */
-  inline const_iterator begin() const {
+  const_iterator begin() const
+  {
     assertTNodeNotExpired();
     return d_nv->begin< NodeTemplate<ref_count> >();
   }
@@ -739,11 +747,32 @@ public:
    * beyond the last one.
    * @return the end of the children const_iterator.
    */
-  inline const_iterator end() const {
+  const_iterator end() const
+  {
     assertTNodeNotExpired();
     return d_nv->end< NodeTemplate<ref_count> >();
   }
 
+  /**
+   * Returns the const_reverse_iterator pointing to the last child.
+   * @return the const_reverse_iterator
+   */
+  const_reverse_iterator rbegin() const
+  {
+    assertTNodeNotExpired();
+    return std::make_reverse_iterator(d_nv->end<NodeTemplate<ref_count>>());
+  }
+
+  /**
+   * Returns the const_reverse_iterator pointing to one before the first child.
+   * @return the end of the const_reverse_iterator.
+   */
+  const_reverse_iterator rend() const
+  {
+    assertTNodeNotExpired();
+    return std::make_reverse_iterator(d_nv->begin<NodeTemplate<ref_count>>());
+  }
+
   /**
    * Returns the iterator pointing to the first child, if the node's
    * kind is the same as the parameter, otherwise returns the iterator

diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 5f5ac7d861f9d8a4d0ed75da3301765abc2a551b..c866516489d3489cc602034316ba70054ebe8c8d 100644 (file)
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -93,7 +93,7 @@ class NodeValue
     using value_type = T;
     using difference_type = std::ptrdiff_t;
     using pointer = T*;
-    using reference = T&;
+    using reference = T;
 
     iterator() : d_i(NULL) {}
     explicit iterator(const_nv_iterator i) : d_i(i) {}

diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index 98fabc727f680153550c6c05072fd67b28482a07..522270de42efebd911dfe5c1d6e1568476184abb 100644 (file)
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -488,6 +488,24 @@ TEST_F(TestNodeBlackNode, iterator)
   }
 }
 
+TEST_F(TestNodeBlackNode, const_reverse_iterator)
+{
+  NodeBuilder b;
+  Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
+  Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType());
+  Node z = d_skolemManager->mkDummySkolem("z", d_nodeManager->booleanType());
+  Node n = b << x << y << z << kind::AND;
+
+  {  // same for const iterator
+    const Node& c = n;
+    Node::const_reverse_iterator i = c.rbegin();
+    ASSERT_EQ(*i++, z);
+    ASSERT_EQ(*i++, y);
+    ASSERT_EQ(*i++, x);
+    ASSERT_EQ(i, n.rend());
+  }
+}
+
 TEST_F(TestNodeBlackNode, kinded_iterator)
 {
   TypeNode integerType = d_nodeManager->integerType();