datatypes work

2 files changed, 99 insertions, 2 deletions

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 286ddf611..7c2d02809 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -208,6 +208,62 @@ Type Expr::getType(bool check) const throw (TypeCheckingException) {
   return d_exprManager->getType(*this, check);
 }
 
+Expr::const_iterator::const_iterator() :
+  d_iterator(NULL) {
+}
+Expr::const_iterator::const_iterator(void* v) :
+  d_iterator(v) {
+}
+Expr::const_iterator::const_iterator(const const_iterator& it) {
+  if(it.d_iterator == NULL) {
+    d_iterator = NULL;
+  } else {
+    d_iterator = new Node::iterator(*reinterpret_cast<Node::iterator*>(it.d_iterator));
+  }
+}
+Expr::const_iterator& Expr::const_iterator::operator=(const const_iterator& it) {
+  if(d_iterator != NULL) {
+    delete reinterpret_cast<Node::iterator*>(d_iterator);
+  }
+  d_iterator = new Node::iterator(*reinterpret_cast<Node::iterator*>(it.d_iterator));
+  return *this;
+}
+Expr::const_iterator::~const_iterator() {
+  if(d_iterator != NULL) {
+    delete reinterpret_cast<Node::iterator*>(d_iterator);
+  }
+}
+bool Expr::const_iterator::operator==(const const_iterator& it) const {
+  if(d_iterator == NULL || it.d_iterator == NULL) {
+    return false;
+  }
+  return *reinterpret_cast<Node::iterator*>(d_iterator) ==
+    *reinterpret_cast<Node::iterator*>(it.d_iterator);
+}
+Expr::const_iterator& Expr::const_iterator::operator++() {
+  Assert(d_iterator != NULL);
+  ++*reinterpret_cast<Node::iterator*>(d_iterator);
+  return *this;
+}
+Expr::const_iterator Expr::const_iterator::operator++(int) {
+  Assert(d_iterator != NULL);
+  const_iterator it = *this;
+  ++*reinterpret_cast<Node::iterator*>(d_iterator);
+  return it;
+}
+Expr Expr::const_iterator::operator*() const {
+  Assert(d_iterator != NULL);
+  return (**reinterpret_cast<Node::iterator*>(d_iterator)).toExpr();
+}
+
+Expr::const_iterator Expr::begin() const {
+  return Expr::const_iterator(new Node::iterator(d_node->begin()));
+}
+
+Expr::const_iterator Expr::end() const {
+  return Expr::const_iterator(new Node::iterator(d_node->end()));
+}
+
 std::string Expr::toString() const {
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index b0157adbf..bffb37ddb 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -30,6 +30,7 @@ ${includes}
 
 #include <string>
 #include <iostream>
+#include <iterator>
 #include <stdint.h>
 
 #include "util/exception.h"
@@ -39,7 +40,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 43 "${template}"
+#line 44 "${template}"
 
 namespace CVC4 {
 
@@ -262,6 +263,46 @@ public:
   Expr operator[](unsigned i) const;
 
   /**
+   * Returns the children of this Expr.
+   */
+  std::vector<Expr> getChildren() const {
+    return std::vector<Expr>(begin(), end());
+  }
+
+  /**
+   * Iterator type for the children of an Expr.
+   */
+  class const_iterator : public std::iterator<std::input_iterator_tag, Expr> {
+    void* d_iterator;
+    explicit const_iterator(void*);
+
+    friend class Expr;// to access void* constructor
+
+  public:
+    const_iterator();
+    const_iterator(const const_iterator& it);
+    const_iterator& operator=(const const_iterator& it);
+    ~const_iterator();
+    bool operator==(const const_iterator& it) const;
+    bool operator!=(const const_iterator& it) const {
+      return !(*this == it);
+    }
+    const_iterator& operator++();
+    const_iterator operator++(int);
+    Expr operator*() const;
+  };/* class Expr::const_iterator */
+
+  /**
+   * Returns an iterator to the first child of this Expr.
+   */
+  const_iterator begin() const;
+
+  /**
+   * Returns an iterator to one-off-the-last child of this Expr.
+   */
+  const_iterator end() const;
+
+  /**
    * Check if this is an expression that has an operator.
    *
    * @return true if this expression has an operator
@@ -750,7 +791,7 @@ public:
 
 ${getConst_instantiations}
 
-#line 754 "${template}"
+#line 795 "${template}"
 
 namespace expr {