diff options
| -rw-r--r-- | src/expr/node.h | 22 | ||||
| -rw-r--r-- | src/expr/node_value.h | 8 | ||||
| -rw-r--r-- | test/unit/expr/node_black.h | 46 |
3 files changed, 61 insertions, 15 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index 1fc583118..91c5bb21b 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -456,7 +456,7 @@ public: /** * Returns the iterator pointing to the end of the children (one beyond the - * last one. + * last one). * @return the end of the children iterator. */ inline iterator end() { @@ -468,7 +468,13 @@ public: } /** - * Returns the iterator pointing to the first child. + * Returns the iterator pointing to the first child, if the node's + * kind is the same as the template parameter, otherwise returns the + * iterator pointing to the node itself. This is useful if you want + * to pretend to iterate over a "unary" PLUS, for instance, since + * unary PLUSes don't exist---begin<PLUS>() will give an iterator + * over the children if the node's a PLUS node, otherwise give an + * iterator over the node itself, as if it were a unary PLUS. * @return the iterator */ template <Kind kind> @@ -481,9 +487,15 @@ public: } /** - * Returns the iterator pointing to the end of the children (one beyond the - * last one. - * @return the end of the children iterator. + * Returns the iterator pointing to the end of the children (one + * beyond the last one), if the node's kind is the same as the + * template parameter, otherwise returns the iterator pointing to + * the one-of-the-node-itself. This is useful if you want to + * pretend to iterate over a "unary" PLUS, for instance, since unary + * PLUSes don't exist---begin<PLUS>() will give an iterator over the + * children if the node's a PLUS node, otherwise give an iterator + * over the node itself, as if it were a unary PLUS. @return the + * end of the children iterator. */ template <Kind kind> inline iterator end() { diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 63121b981..2b26b273d 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -364,7 +364,9 @@ inline NodeValue::iterator<T> NodeValue::end() const { template <typename T, Kind kind> inline NodeValue::iterator<T> NodeValue::begin() const { - if (d_kind != kind) return iterator<T>(this); + if(d_kind != kind) { + return iterator<T>(this); + } NodeValue* const* firstChild = d_children; if(getMetaKind() == kind::metakind::PARAMETERIZED) { ++firstChild; @@ -374,7 +376,9 @@ inline NodeValue::iterator<T> NodeValue::begin() const { template <typename T, Kind kind> inline NodeValue::iterator<T> NodeValue::end() const { - if (d_kind != kind) return iterator<T>(this + 1); + if(d_kind != kind) { + return iterator<T>(this + 1); + } return iterator<T>(d_children + d_nchildren); } diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index f1bb7c251..fbc308597 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -473,6 +473,7 @@ public: #endif /* CVC4_ASSERTIONS */ } + // test iterators void testIterator() { NodeBuilder<> b; Node x = d_nodeManager->mkVar(*d_booleanType); @@ -498,13 +499,42 @@ public: } } + // test the special "kinded-iterator" + void testKindedIterator() { + TypeNode integerType = d_nodeManager->integerType(); + + Node x = d_nodeManager->mkVar("x", integerType); + Node y = d_nodeManager->mkVar("y", integerType); + Node z = d_nodeManager->mkVar("z", integerType); + Node plus_x_y_z = d_nodeManager->mkNode(kind::PLUS, x, y, z); + Node x_minus_y = d_nodeManager->mkNode(kind::MINUS, x, y); + + { // iterator + /* FAILING TEST: + Node::iterator i = plus_x_y_z.begin<PLUS>(); + TS_ASSERT(*i++ == x); + TS_ASSERT(*i++ == y); + TS_ASSERT(*i++ == z); + TS_ASSERT(i == plus_x_y_z.end<PLUS>()); + + i = x.begin<PLUS>(); + TS_ASSERT(*i++ == x); + TS_ASSERT(i == x.end<PLUS>()); + */ + } + + { // same for const iterator + //const Node& c = plus_x_y_z; + } + } + void testToString() { TypeNode booleanType = d_nodeManager->booleanType(); - Node w = d_nodeManager->mkVar("w",booleanType); - Node x = d_nodeManager->mkVar("x",booleanType); - Node y = d_nodeManager->mkVar("y",booleanType); - Node z = d_nodeManager->mkVar("z",booleanType); + Node w = d_nodeManager->mkVar("w", booleanType); + Node x = d_nodeManager->mkVar("x", booleanType); + Node y = d_nodeManager->mkVar("y", booleanType); + Node z = d_nodeManager->mkVar("z", booleanType); Node m = NodeBuilder<>() << w << x << kind::OR; Node n = NodeBuilder<>() << m << y << z << kind::AND; @@ -514,10 +544,10 @@ public: void testToStream() { TypeNode booleanType = d_nodeManager->booleanType(); - Node w = d_nodeManager->mkVar("w",booleanType); - Node x = d_nodeManager->mkVar("x",booleanType); - Node y = d_nodeManager->mkVar("y",booleanType); - Node z = d_nodeManager->mkVar("z",booleanType); + Node w = d_nodeManager->mkVar("w", booleanType); + Node x = d_nodeManager->mkVar("x", booleanType); + Node y = d_nodeManager->mkVar("y", booleanType); + Node z = d_nodeManager->mkVar("z", booleanType); Node m = NodeBuilder<>() << x << y << kind::OR; Node n = NodeBuilder<>() << w << m << z << kind::AND; Node o = NodeBuilder<>() << n << n << kind::XOR; |