diff options
Diffstat (limited to 'src/expr/node_builder.h')
-rw-r--r-- | src/expr/node_builder.h | 22 |
1 files changed, 20 insertions, 2 deletions
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 13aa0b0ff..7c6405ace 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -36,6 +36,9 @@ namespace CVC4 { namespace CVC4 { +template <unsigned nchild_thresh> +inline std::ostream& operator<<(std::ostream&, const NodeBuilder<nchild_thresh>&); + class AndNodeBuilder; class OrNodeBuilder; class PlusNodeBuilder; @@ -122,6 +125,10 @@ public: return d_ev->ev_end(); } + unsigned getNumChildren() const { + return d_ev->getNumChildren(); + } + // Compound expression constructors /* NodeBuilder& eqExpr(const Node& right); @@ -189,6 +196,10 @@ public: // not const operator Node(); + inline void toStream(std::ostream& out) const { + d_ev->toStream(out); + } + /* AndNodeBuilder operator&&(Node); OrNodeBuilder operator||(Node); @@ -440,7 +451,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) : template <unsigned nchild_thresh> inline NodeBuilder<nchild_thresh>::~NodeBuilder() { Assert(d_used, "NodeBuilder unused at destruction"); - + return; /* for(iterator i = d_ev->ev_begin(); @@ -566,7 +577,7 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const // this inserts into the NodeManager; // return the result of lookup() in case another thread beat us to it - if(ev->numChildren()) { + if(ev->getNumChildren()) { Debug("prop") << "ev first child: " << *ev->ev_begin() << std::endl; } Node n = d_nm->lookup(d_hash, ev); @@ -574,6 +585,13 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const return n; } +template <unsigned nchild_thresh> +inline std::ostream& operator<<(std::ostream& out, + const NodeBuilder<nchild_thresh>& b) { + b.toStream(out); + return out; +} + }/* CVC4 namespace */ #endif /* __CVC4__NODE_BUILDER_H */ |