/********************* */ /*! \file node_builder.h ** \verbatim ** Top contributors (to current version): ** Morgan Deters, Mathias Preiner, Dejan Jovanovic ** This file is part of the CVC4 project. ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** ** \brief A builder interface for Nodes. ** ** A builder interface for Nodes. ** ** The idea is to permit a flexible and efficient (in the common ** case) interface for building Nodes. The general pattern of use is ** to create a NodeBuilder, set its kind, append children to it, then ** "extract" the resulting Node. This resulting Node may be one that ** already exists (the NodeManager keeps a table of all Nodes in the ** system), or may be entirely new. ** ** This implementation gets a bit hairy for a handful of reasons. We ** want a user-supplied "in-line" buffer (probably on the stack, see ** below) to hold the children, but then the number of children must ** be known ahead of time. Therefore, if this buffer is overrun, we ** need to heap-allocate a new buffer to hold the children. ** ** Note that as children are added to a NodeBuilder, they are stored ** as raw pointers-to-NodeValue. However, their reference counts are ** carefully maintained. ** ** When the "in-line" buffer "d_inlineNv" is superceded by a ** heap-allocated buffer, we allocate the new buffer (a NodeValue ** large enough to hold more children), copy the elements to it, and ** mark d_inlineNv as having zero children. We do this last bit so ** that we don't have to modify any child reference counts. The new ** heap-allocated buffer "takes over" the reference counts of the old ** "in-line" buffer. (If we didn't mark it as having zero children, ** the destructor may improperly decrement the children's reference ** counts.) ** ** There are then four normal cases at the end of a NodeBuilder's ** life cycle: ** ** 0. We have a VARIABLE-kinded Node. These are special (they have ** no children and are all distinct by definition). They are ** really a subcase of 1(b), below. ** 1. d_nv points to d_inlineNv: it is the backing store supplied ** by the user (or derived class). ** (a) The Node under construction already exists in the ** NodeManager's pool. ** (b) The Node under construction is NOT already in the ** NodeManager's pool. ** 2. d_nv does NOT point to d_inlineNv: it is a new, larger buffer ** that was heap-allocated by this NodeBuilder. ** (a) The Node under construction already exists in the ** NodeManager's pool. ** (b) The Node under construction is NOT already in the ** NodeManager's pool. ** ** When a Node is extracted, we convert the NodeBuilder to a Node and ** make sure the reference counts are properly maintained. That ** means we must ensure there are no reference-counting errors among ** the node's children, that the children aren't re-decremented on ** clear() or NodeBuilder destruction, and that the returned Node ** wraps a NodeValue with a reference count of 1. ** ** 0. If a VARIABLE, treat similarly to 1(b), except that we ** know there are no children (no reference counts to reason ** about) and we don't keep VARIABLE-kinded Nodes in the ** NodeManager pool. ** ** 1(a). Reference-counts for all children in d_inlineNv must be ** decremented, and the NodeBuilder must be marked as "used" ** and the number of children set to zero so that we don't ** decrement them again on destruction. The existing ** NodeManager pool entry is returned. ** ** 1(b). A new heap-allocated NodeValue must be constructed and all ** settings and children from d_inlineNv copied into it. ** This new NodeValue is put into the NodeManager's pool. ** The NodeBuilder is marked as "used" and the number of ** children in d_inlineNv set to zero so that we don't ** decrement child reference counts on destruction (the child ** reference counts have been "taken over" by the new ** NodeValue). We return a Node wrapper for this new ** NodeValue, which increments its reference count. ** ** 2(a). Reference counts for all children in d_nv must be ** decremented. The NodeBuilder is marked as "used" and the ** heap-allocated d_nv deleted. d_nv is repointed to ** d_inlineNv so that destruction of the NodeBuilder doesn't ** cause any problems. The existing NodeManager pool entry ** is returned. ** ** 2(b). The heap-allocated d_nv is "cropped" to the correct size ** (based on the number of children it _actually_ has). d_nv ** is repointed to d_inlineNv so that destruction of the ** NodeBuilder doesn't cause any problems, and the (old) ** value it had is placed into the NodeManager's pool and ** returned in a Node wrapper. ** ** NOTE IN 1(b) AND 2(b) THAT we can NOT create Node wrapper ** temporary for the NodeValue in the NodeBuilder::operator Node() ** member function. If we create a temporary (for example by writing ** Debug("builder") << Node(nv) << endl), the NodeValue will have its ** reference count incremented from zero to one, then decremented, ** which makes it eligible for collection before the builder has even ** returned it! So this is a no-no. ** ** There are also two cases when the NodeBuilder is clear()'ed: ** ** 1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied ** backing store): all d_inlineNv children have their reference ** counts decremented, d_inlineNv.d_nchildren is set to zero, ** and its kind is set to UNDEFINED_KIND. ** ** 2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all ** d_nv children have their reference counts decremented, d_nv ** is deallocated, and d_nv is set to &d_inlineNv. d_inlineNv's ** kind is set to UNDEFINED_KIND. ** ** ... destruction is similar: ** ** 1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied ** backing store): all d_inlineNv children have their reference ** counts decremented. ** ** 2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all ** d_nv children have their reference counts decremented, and ** d_nv is deallocated. **/ #include "cvc4_private.h" /* strong dependency; make sure node is included first */ #include "expr/node.h" #ifndef CVC5__NODE_BUILDER_H #define CVC5__NODE_BUILDER_H #include #include #include "base/check.h" #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node_value.h" #include "expr/type_node.h" namespace cvc5 { class NodeManager; /** * The NodeBuilder. */ class NodeBuilder { friend std::ostream& operator<<(std::ostream& out, const NodeBuilder& nb); constexpr static size_t default_nchild_thresh = 10; public: NodeBuilder(); NodeBuilder(Kind k); NodeBuilder(NodeManager* nm); NodeBuilder(NodeManager* nm, Kind k); NodeBuilder(const NodeBuilder& nb); ~NodeBuilder(); /** Get the kind of this Node-under-construction. */ Kind getKind() const; /** Get the kind of this Node-under-construction. */ kind::MetaKind getMetaKind() const; /** Get the current number of children of this Node-under-construction. */ unsigned getNumChildren() const; /** * Access to the operator of this Node-under-construction. Only * allowed if this NodeBuilder is unused, and has a defined kind * that is of PARAMETERIZED metakind. */ Node getOperator() const; /** * Access to children of this Node-under-construction. Only allowed * if this NodeBuilder is unused and has a defined kind. */ Node getChild(int i) const; /** Access to children of this Node-under-construction. */ Node operator[](int i) const; /** * "Reset" this node builder (optionally setting a new kind for it), * using the same "inline" memory as at construction time. This * deallocates NodeBuilder-allocated heap memory, if it was * allocated, and decrements the reference counts of any currently * children in the NodeBuilder. * * This should leave the NodeBuilder in the state it was after * initial construction, except for Kind, which is set to the * argument, if provided, or UNDEFINED_KIND. In particular, the * associated NodeManager is not affected by clear(). */ void clear(Kind k = kind::UNDEFINED_KIND); // "Stream" expression constructor syntax /** Set the Kind of this Node-under-construction. */ NodeBuilder& operator<<(const Kind& k); /** * If this Node-under-construction has a Kind set, collapse it and * append the given Node as a child. Otherwise, simply append. */ NodeBuilder& operator<<(TNode n); /** * If this Node-under-construction has a Kind set, collapse it and * append the given Node as a child. Otherwise, simply append. */ NodeBuilder& operator<<(TypeNode n); /** Append a sequence of children to this TypeNode-under-construction. */ NodeBuilder& append(const std::vector& children); /** Append a sequence of children to this Node-under-construction. */ template inline NodeBuilder& append( const std::vector >& 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 NodeBuilder& append(const Iterator& begin, const Iterator& end) { Assert(!isUsed()) << "NodeBuilder is one-shot only; " "attempt to access it after conversion"; for(Iterator i = begin; i != end; ++i) { append(*i); } return *this; } /** Append a child to this Node-under-construction. */ NodeBuilder& append(TNode n); /** Append a child to this Node-under-construction. */ NodeBuilder& append(const TypeNode& typeNode); /** Construct the Node out of the node builder */ Node constructNode(); /** Construct a Node on the heap out of the node builder */ Node* constructNodePtr(); /** Construction of the TypeNode out of the node builder */ TypeNode constructTypeNode(); // two versions, so we can support extraction from (const) // NodeBuilders which are temporaries appearing as rvalues operator Node(); // similarly for TypeNode operator TypeNode(); private: void internalCopy(const NodeBuilder& nb); /** * Returns whether or not this NodeBuilder has been "used"---i.e., * whether a Node has been extracted with operator Node(). * Internally, this state is represented by d_nv pointing to NULL. */ bool isUsed() const; /** * Set this NodeBuilder to the `used' state. */ void setUsed(); /** * Set this NodeBuilder to the `unused' state. Should only be done * from clear(). */ void setUnused(); /** * Returns true if d_nv is *not* the "in-line" one (it was * heap-allocated by this class). */ bool nvIsAllocated() const; /** * Returns true if adding a child requires (re)allocation of d_nv * first. */ bool nvNeedsToBeAllocated() const; /** * (Re)allocate d_nv using a default grow factor. Ensure that child * pointers are copied into the new buffer, and if the "inline" * NodeValue is evacuated, make sure its children won't be * double-decremented later (on destruction/clear). */ void realloc(); /** * (Re)allocate d_nv to a specific size. Specify "copy" if the * children should be copied; if they are, and if the "inline" * NodeValue is evacuated, make sure its children won't be * double-decremented later (on destruction/clear). */ void realloc(size_t toSize); /** * If d_nv needs to be (re)allocated to add an additional child, do * so using realloc(), which ensures child pointers are copied and * that the reference counts of the "inline" NodeValue won't be * double-decremented on destruction/clear. Otherwise, do nothing. */ void allocateNvIfNecessaryForAppend(); /** * Deallocate a d_nv that was heap-allocated by this class during * grow operations. (Marks this NodeValue no longer allocated so * that double-deallocations don't occur.) * * PRECONDITION: only call this when nvIsAllocated() == true. * POSTCONDITION: !nvIsAllocated() */ void dealloc(); /** * "Purge" the "inline" children. Decrement all their reference * counts and set the number of children to zero. * * PRECONDITION: only call this when nvIsAllocated() == false. * POSTCONDITION: d_inlineNv.d_nchildren == 0. */ void decrRefCounts(); /** * Trim d_nv down to the size it needs to be for the number of * children it has. Used when a Node is extracted from a * NodeBuilder and we want the returned memory not to suffer from * internal fragmentation. If d_nv was not heap-allocated by this * class, or is already the right size, this function does nothing. * * @throws bad_alloc if the reallocation fails */ void crop(); /** Construct the node value out of the node builder */ expr::NodeValue* constructNV(); #ifdef CVC5_DEBUG // Throws a TypeCheckingExceptionPrivate on a failure. void maybeCheckType(const TNode n) const; #else /* CVC5_DEBUG */ // Do nothing if not in debug mode. inline void maybeCheckType(const TNode n) const {} #endif /* CVC5_DEBUG */ // used by convenience node builders NodeBuilder& collapseTo(Kind k); /** * An "in-line" stack-allocated buffer for use by the * NodeBuilder. */ expr::NodeValue d_inlineNv; /** * Space for the children of the node being constructed. This is * never accessed directly, but rather through * d_inlineNv.d_children[i]. */ expr::NodeValue* d_inlineNvChildSpace[default_nchild_thresh]; /** * A pointer to the "current" NodeValue buffer; either &d_inlineNv * or a heap-allocated one if d_inlineNv wasn't big enough. */ expr::NodeValue* d_nv; /** The NodeManager at play */ NodeManager* d_nm; /** * The number of children allocated in d_nv. */ uint32_t d_nvMaxChildren; }; /* class NodeBuilder */ // Sometimes it's useful for debugging to output a NodeBuilder that // isn't yet a Node.. std::ostream& operator<<(std::ostream& out, const NodeBuilder& nb); } // namespace cvc5 #endif /* CVC5__NODE_BUILDER_H */