diff options
Diffstat (limited to 'src/expr/node_builder.h')
-rw-r--r-- | src/expr/node_builder.h | 44 |
1 files changed, 40 insertions, 4 deletions
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 09e72660e..cefeb2fe2 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -173,6 +173,7 @@ /* strong dependency; make sure node is included first */ #include "node.h" +#include "type_node.h" #ifndef __CVC4__NODE_BUILDER_H #define __CVC4__NODE_BUILDER_H @@ -410,21 +411,21 @@ public: // override this in a derived class. inline ~NodeBuilderBase(); - typedef expr::NodeValue::iterator<true> iterator; - typedef expr::NodeValue::iterator<true> const_iterator; + typedef expr::NodeValue::iterator< NodeTemplate<true> > iterator; + typedef expr::NodeValue::iterator< NodeTemplate<true> > const_iterator; /** Get the begin-const-iterator of this Node-under-construction. */ inline const_iterator begin() const { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); - return d_nv->begin<true>(); + return d_nv->begin< NodeTemplate<true> >(); } /** Get the end-const-iterator of this Node-under-construction. */ inline const_iterator end() const { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); - return d_nv->end<true>(); + return d_nv->end< NodeTemplate<true> >(); } /** Get the kind of this Node-under-construction. */ @@ -505,6 +506,14 @@ public: return append(n); } + /** Append a sequence of children to this TypeNode-under-construction. */ + inline Builder& + append(const std::vector<TypeNode>& children) { + Assert(!isUsed(), "NodeBuilder is one-shot only; " + "attempt to access it after conversion"); + return append(children.begin(), children.end()); + } + /** Append a sequence of children to this Node-under-construction. */ template <bool ref_count> inline Builder& @@ -537,6 +546,18 @@ public: return static_cast<Builder&>(*this); } + /** Append a child to this Node-under-construction. */ + Builder& append(const TypeNode& typeNode) { + Assert(!isUsed(), "NodeBuilder is one-shot only; " + "attempt to access it after conversion"); + Assert(!typeNode.isNull(), "Cannot use NULL Node as a child of a Node"); + allocateNvIfNecessaryForAppend(); + expr::NodeValue* nv = typeNode.d_nv; + nv->inc(); + d_nv->d_children[d_nv->d_nchildren++] = nv; + return static_cast<Builder&>(*this); + } + private: /** Construct the node value out of the node builder */ @@ -553,6 +574,10 @@ public: Node* constructNodePtr(); Node* constructNodePtr() const; + /** Construction of the TypeNode out of the node builder */ + TypeNode constructTypeNode(); + TypeNode constructTypeNode() const; + // two versions, so we can support extraction from (const) // NodeBuilders which are temporaries appearing as rvalues operator Node(); @@ -1245,6 +1270,17 @@ void NodeBuilderBase<Builder>::decrRefCounts() { d_inlineNv.d_nchildren = 0; } + +template <class Builder> +TypeNode NodeBuilderBase<Builder>::constructTypeNode() { + return TypeNode(constructNV()); +} + +template <class Builder> +TypeNode NodeBuilderBase<Builder>::constructTypeNode() const { + return TypeNode(constructNV()); +} + template <class Builder> Node NodeBuilderBase<Builder>::constructNode() { return Node(constructNV()); |