From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Tue, 21 Sep 2010 17:33:06 +0000 (+0000)
Subject: iterators for tim, begin<PLUS>() and end<PLUS>() should give him what he wants
X-Git-Tag: cvc5-1.0.0~8860
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ea9346f840046ee20558afb2a17dd5999d45c5c9;p=cvc5.git

iterators for tim, begin<PLUS>() and end<PLUS>() should give him what he wants
---

diff --git a/src/expr/node.h b/src/expr/node.h
index 222185e8c..1fc583118 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -467,6 +467,34 @@ public:
     return d_nv->end< NodeTemplate<ref_count> >();
   }
 
+  /**
+   * Returns the iterator pointing to the first child.
+   * @return the iterator
+   */
+  template <Kind kind>
+  inline iterator begin() {
+    if(!ref_count) {
+      Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
+    }
+
+    return d_nv->begin< NodeTemplate<ref_count>, kind >();
+  }
+
+  /**
+   * Returns the iterator pointing to the end of the children (one beyond the
+   * last one.
+   * @return the end of the children iterator.
+   */
+  template <Kind kind>
+  inline iterator end() {
+    if(!ref_count) {
+      Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
+    }
+
+    return d_nv->end< NodeTemplate<ref_count>, kind >();
+  }
+
+
   /**
    * Returns the const_iterator pointing to the first child.
    * @return the const_iterator
@@ -492,6 +520,33 @@ public:
     return d_nv->end< NodeTemplate<ref_count> >();
   }
 
+  /**
+   * Returns the const_iterator pointing to the first child.
+   * @return the const_iterator
+   */
+  template <Kind kind>
+  inline const_iterator begin() const {
+    if(!ref_count) {
+      Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
+    }
+
+    return d_nv->begin< NodeTemplate<ref_count>, 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.
+   */
+  template <Kind kind>
+  inline const_iterator end() const {
+    if(!ref_count) {
+      Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
+    }
+
+    return d_nv->end< NodeTemplate<ref_count>, kind >();
+  }
+
   /**
    * Converts this node into a string representation.
    * @return the string representation of this node.
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 3c21777ed..63121b981 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -187,6 +187,12 @@ public:
   template <typename T>
   inline iterator<T> end() const;
 
+  template <typename T, Kind kind>
+  inline iterator<T> begin() const;
+
+  template <typename T, Kind kind>
+  inline iterator<T> 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
@@ -356,6 +362,22 @@ inline NodeValue::iterator<T> NodeValue::end() const {
   return iterator<T>(d_children + d_nchildren);
 }
 
+template <typename T, Kind kind>
+inline NodeValue::iterator<T> NodeValue::begin() const {
+  if (d_kind != kind) return iterator<T>(this);
+  NodeValue* const* firstChild = d_children;
+  if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+    ++firstChild;
+  }
+  return iterator<T>(firstChild);
+}
+
+template <typename T, Kind kind>
+inline NodeValue::iterator<T> NodeValue::end() const {
+  if (d_kind != kind) return iterator<T>(this + 1);
+  return iterator<T>(d_children + d_nchildren);
+}
+
 inline bool NodeValue::isBeingDeleted() const {
   return NodeManager::currentNM() != NULL &&
     NodeManager::currentNM()->isCurrentlyDeleting(this);