diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-12-03 14:59:30 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-12-03 14:59:30 +0000 |
commit | 7fb54afe126e5045fc6c5553c1aff3c3f73509aa (patch) | |
tree | 37f4f23af0eccd6c9615a5af9b2d219e305d1f78 /src/expr/expr.h | |
parent | bde1a14afc211c8f0f0521bb91feb562eaa9f9ea (diff) |
parsing/expr/command/result/various other fixes
Diffstat (limited to 'src/expr/expr.h')
-rw-r--r-- | src/expr/expr.h | 57 |
1 files changed, 54 insertions, 3 deletions
diff --git a/src/expr/expr.h b/src/expr/expr.h index 19f02650e..5a11e0fbd 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -14,12 +14,23 @@ #define __CVC4__EXPR_H #include <vector> +#include <iostream> #include <stdint.h> #include "cvc4_config.h" #include "expr/kind.h" namespace CVC4 { + class Expr; +}/* CVC4 namespace */ + +namespace std { +inline std::ostream& operator<<(std::ostream&, CVC4::Expr) CVC4_PUBLIC; +} + +namespace CVC4 { + +class ExprManager; namespace expr { class ExprValue; @@ -45,10 +56,8 @@ class CVC4_PUBLIC Expr { * Increments the reference count. */ explicit Expr(ExprValue*); - typedef Expr* iterator; - typedef Expr const* const_iterator; - friend class ExprBuilder; + friend class ExprManager; public: CVC4_PUBLIC Expr(const Expr&); @@ -81,20 +90,62 @@ public: inline Kind getKind() const; + inline size_t numChildren() const; + static Expr null() { return s_null; } + typedef Expr* iterator; + typedef Expr const* const_iterator; + + inline iterator begin(); + inline iterator end(); + inline iterator begin() const; + inline iterator end() const; + + void toString(std::ostream&) const; };/* class Expr */ }/* CVC4 namespace */ #include "expr/expr_value.h" +inline std::ostream& std::operator<<(std::ostream& out, CVC4::Expr e) { + e.toString(out); + return out; +} + namespace CVC4 { inline Kind Expr::getKind() const { return Kind(d_ev->d_kind); } +inline void Expr::toString(std::ostream& out) const { + if(d_ev) + d_ev->toString(out); + else out << "null"; +} + +inline Expr::iterator Expr::begin() { + return d_ev->begin(); +} + +inline Expr::iterator Expr::end() { + return d_ev->end(); +} + +inline Expr::iterator Expr::begin() const { + return d_ev->begin(); +} + +inline Expr::iterator Expr::end() const { + return d_ev->end(); +} + +inline size_t Expr::numChildren() const { + return d_ev->d_nchildren; +} + }/* CVC4 namespace */ #endif /* __CVC4__EXPR_H */ |