From: Morgan Deters Date: Tue, 28 Sep 2010 20:57:25 +0000 (+0000) Subject: node iterator work X-Git-Tag: cvc5-1.0.0~8842 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=665704ba3ec1201c536c2ffa27a4d667eab3e12c;p=cvc5.git node iterator work --- diff --git a/src/expr/node.h b/src/expr/node.h index 4f306bcff..8b64dc781 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -455,6 +455,70 @@ public: /** Constant iterator allowing for scanning through the children. */ typedef typename expr::NodeValue::iterator< NodeTemplate > const_iterator; + class kinded_iterator { + friend class NodeTemplate; + + NodeTemplate d_node; + ssize_t d_child; + + kinded_iterator(TNode node, ssize_t child) : + d_node(node), + d_child(child) { + } + + // These are factories to serve as clients to Node::begin() and + // Node::end(). + static kinded_iterator begin(TNode n, Kind k) { + return kinded_iterator(n, n.getKind() == k ? 0 : -2); + } + static kinded_iterator end(TNode n, Kind k) { + return kinded_iterator(n, n.getKind() == k ? n.getNumChildren() : -1); + } + + public: + typedef NodeTemplate value_type; + typedef ptrdiff_t difference_type; + typedef NodeTemplate* pointer; + typedef NodeTemplate& reference; + + kinded_iterator() : + d_node(NodeTemplate::null()), + d_child(-2) { + } + + kinded_iterator(const kinded_iterator& i) : + d_node(i.d_node), + d_child(i.d_child) { + } + + NodeTemplate operator*() { + return d_child < 0 ? d_node : d_node[d_child]; + } + + bool operator==(const kinded_iterator& i) { + return d_node == i.d_node && d_child == i.d_child; + } + + bool operator!=(const kinded_iterator& i) { + return !(*this == i); + } + + kinded_iterator& operator++() { + if(d_child != -1) { + ++d_child; + } + return *this; + } + + kinded_iterator operator++(int) { + kinded_iterator i = *this; + ++*this; + return i; + } + };/* class NodeTemplate::kinded_iterator */ + + typedef kinded_iterator const_kinded_iterator; + /** * Returns the iterator pointing to the first child. * @return the iterator @@ -476,38 +540,39 @@ public: /** * 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() 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 + * kind is the same as the 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. + * @param the kind to match + * @return the kinded_iterator iterating over this Node (if its kind + * is not the passed kind) or its children */ - template - inline iterator begin() { + inline kinded_iterator begin(Kind kind) { assertTNodeNotExpired(); - return d_nv->begin< NodeTemplate, kind >(); + return kinded_iterator::begin(*this, kind); } /** * 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() 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. + * 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. + * @param the kind to match + * @return the kinded_iterator pointing off-the-end of this Node (if + * its kind is not the passed kind) or off-the-end of its children */ - template - inline iterator end() { + inline kinded_iterator end(Kind kind) { assertTNodeNotExpired(); - return d_nv->end< NodeTemplate, kind >(); + return kinded_iterator::end(*this, kind); } - /** * Returns the const_iterator pointing to the first child. * @return the const_iterator @@ -528,24 +593,38 @@ public: } /** - * Returns the const_iterator pointing to the first child. - * @return the const_iterator + * 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 + * 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. + * @param the kind to match + * @return the kinded_iterator iterating over this Node (if its kind + * is not the passed kind) or its children */ - template - inline const_iterator begin() const { + inline const_kinded_iterator begin(Kind kind) const { assertTNodeNotExpired(); - return d_nv->begin< NodeTemplate, kind >(); + return const_kinded_iterator::begin(*this, kind); } /** - * Returns the const_iterator pointing to the end of the children (one - * beyond the last one. - * @return the end of the children const_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 + * 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. + * @param the kind to match + * @return the kinded_iterator pointing off-the-end of this Node (if + * its kind is not the passed kind) or off-the-end of its children */ - template - inline const_iterator end() const { + inline const_kinded_iterator end(Kind kind) const { assertTNodeNotExpired(); - return d_nv->end< NodeTemplate, kind >(); + return const_kinded_iterator::end(*this, kind); } /** diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 2b26b273d..e4fc479b7 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -162,7 +162,7 @@ private: return d_i != i.d_i; } - iterator operator++() { + iterator& operator++() { ++d_i; return *this; } @@ -187,12 +187,6 @@ public: template inline iterator end() const; - template - inline iterator begin() const; - - template - inline iterator end() const; - /** * Hash this NodeValue. For hash_maps, hash_sets, etc.. but this is * for expr package internal use only at present! This is likely to @@ -362,26 +356,6 @@ inline NodeValue::iterator NodeValue::end() const { return iterator(d_children + d_nchildren); } -template -inline NodeValue::iterator NodeValue::begin() const { - if(d_kind != kind) { - return iterator(this); - } - NodeValue* const* firstChild = d_children; - if(getMetaKind() == kind::metakind::PARAMETERIZED) { - ++firstChild; - } - return iterator(firstChild); -} - -template -inline NodeValue::iterator NodeValue::end() const { - if(d_kind != kind) { - return iterator(this + 1); - } - return iterator(d_children + d_nchildren); -} - inline bool NodeValue::isBeingDeleted() const { return NodeManager::currentNM() != NULL && NodeManager::currentNM()->isCurrentlyDeleting(this);