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*`.

1 files changed, 18 insertions, 0 deletions

diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index 98fabc727..522270de4 100644
--- 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();