diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-06-03 05:30:54 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-06-03 05:30:54 +0000 |
commit | 4a696409769044ad155a56eeb00c9d85246ca0b4 (patch) | |
tree | 27a131cb40138049508150fc5aa2c0330b52f704 /src/expr | |
parent | d935021323ca343da5359fa54bc62184d47ccd1b (diff) |
datatypes work
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_template.cpp | 56 | ||||
-rw-r--r-- | src/expr/expr_template.h | 45 |
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 { |