diff options
-rw-r--r-- | src/expr/node.h | 35 | ||||
-rw-r--r-- | src/expr/node_value.h | 2 | ||||
-rw-r--r-- | test/unit/node/node_black.cpp | 18 |
3 files changed, 51 insertions, 4 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index 5f5d3a976..a406b3d13 100644 --- 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,12 +747,33 @@ 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 * pointing to the node itself. This is useful if you want to diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 5f5ac7d86..c86651648 100644 --- 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 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(); |