** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** 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 (see the non-const version of
+ ** NodeBuilderBase<>::operator Node()), 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 NodeBuilderBase<>::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.
+ **
+ ** For the _const_ version of NodeBuilderBase<>::operator Node(), no
+ ** reference-count modifications or anything else can take place!
+ ** Therefore, we have a slightly more expensive version:
+ **
+ ** 0. If a VARIABLE, treat similarly to 1(b), except that we
+ ** know there are no children, and we don't keep
+ ** VARIABLE-kinded Nodes in the NodeManager pool.
+ **
+ ** 1(a). The existing NodeManager pool entry is returned; we leave
+ ** child reference counts alone and get them at NodeBuilder
+ ** destruction time.
+ **
+ ** 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 cannot be marked as "used", so we
+ ** increment all child reference counts (which will be
+ ** decremented to match on destruction of the NodeBuilder).
+ ** We return a Node wrapper for this new NodeValue, which
+ ** increments its reference count.
+ **
+ ** 2(a). The existing NodeManager pool entry is returned; we leave
+ ** child reference counts alone and get them at NodeBuilder
+ ** destruction time.
+ **
+ ** 2(b). The heap-allocated d_nv cannot be "cropped" to the correct
+ ** size; we create a copy, increment child reference counts,
+ ** place this copy into the NodeManager pool, and return a
+ ** Node wrapper around it. The child reference counts will
+ ** be decremented to match at NodeBuilder destruction time.
+ **
+ ** 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.
+ **
+ ** Regarding the backing store (typically on the stack): the file
+ ** below provides three classes (two of them are templates):
+ **
+ ** template <class Builder> class NodeBuilderBase;
+ **
+ ** This is the base class for node builders. It can not be used
+ ** directly. It contains a shared implementation but is intended
+ ** to be subclassed. Derived classes supply its "in-line" buffer.
+ **
+ ** class BackedNodeBuilder;
+ **
+ ** This is the usable form for a user-supplied-backing-store node
+ ** builder. A user can allocate a buffer large enough for a
+ ** NodeValue with N children (say, on the stack), then pass a
+ ** pointer to this buffer, and the parameter N, to a
+ ** BackedNodeBuilder. It will use this buffer to build its
+ ** NodeValue until the number of children exceeds N; then it will
+ ** allocate d_nv on the heap.
+ **
+ ** To ensure that the buffer is properly-sized, it is recommended
+ ** to use the makeStackNodeBuilder(b, N) macro to make a
+ ** BackedNodeBuilder "b" with a stack-allocated buffer large
+ ** enough to hold N children.
+ **
+ ** template <unsigned nchild_thresh> class NodeBuilder;
+ **
+ ** This is the conceptually easiest form of NodeBuilder to use.
+ ** The default:
+ **
+ ** NodeBuilder<> b;
+ **
+ ** gives you a backing buffer with capacity for 10 children in
+ ** the same place as the NodeBuilder<> itself is allocated. You
+ ** can specify another size as a template parameter, but it must
+ ** be a compile-time constant (which is why the BackedNodeBuilder
+ ** creator-macro "makeStackNodeBuilder(b, N)" is sometimes
+ ** preferred).
**/
#include "cvc4_private.h"
namespace CVC4 {
static const unsigned default_nchild_thresh = 10;
- template <unsigned nchild_thresh = default_nchild_thresh>
- class NodeBuilder;
+ template <class Builder>
+ class NodeBuilderBase;
class NodeManager;
}/* CVC4 namespace */
namespace CVC4 {
-template <unsigned nchild_thresh>
-inline std::ostream& operator<<(std::ostream&, const NodeBuilder<nchild_thresh>&);
+template <class Builder>
+inline std::ostream& operator<<(std::ostream&, const NodeBuilderBase<Builder>&);
class AndNodeBuilder;
class OrNodeBuilder;
class PlusNodeBuilder;
class MultNodeBuilder;
-template <unsigned nchild_thresh>
-class NodeBuilder {
+/**
+ * A base class for NodeBuilders. When extending this class, use:
+ *
+ * class MyExtendedNodeBuilder : public NodeBuilderBase<MyExtendedNodeBuilder> { ... };
+ *
+ * This ensures that certain member functions return the right
+ * (derived) class type.
+ *
+ * There are no virtual functions here, and that should remain the
+ * case! This class is just used for sharing of implementation. Two
+ * types derive from it: BackedNodeBuilder (which allows for an
+ * external buffer), and the NodeBuilder<> template, which requires
+ * that you give it a compile-time constant backing-store size.
+ */
+template <class Builder>
+class NodeBuilderBase {
+protected:
- unsigned d_size;
+ /**
+ * A reference to an "in-line" stack-allocated buffer for use by the
+ * NodeBuilder.
+ */
+ expr::NodeValue& d_inlineNv;
- uint64_t d_hash;
+ /**
+ * 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;
- // initially false, when you extract the Node this is set and you can't
- // extract another
- bool d_used;
+ /**
+ * The maximum number of children that can be held in this "in-line"
+ * buffer.
+ */
+ const uint16_t d_inlineNvMaxChildren;
- expr::NodeValue* d_nv;
- expr::NodeValue d_inlineNv;
- expr::NodeValue *d_childrenStorage[nchild_thresh];
+ /**
+ * The number of children allocated in d_nv.
+ */
+ uint16_t d_nvMaxChildren;
- bool nvIsAllocated() const {
- return d_nv->d_nchildren > nchild_thresh;
+ /**
+ * Returns whether or not this NodeBuilder has been "used"---i.e.,
+ * whether a Node has been extracted with [the non-const version of]
+ * operator Node(). Internally, this state is represented by d_nv
+ * pointing to NULL.
+ */
+ inline bool isUsed() const {
+ return EXPECT_FALSE( d_nv == NULL );
}
- template <unsigned N>
- bool nvIsAllocated(const NodeBuilder<N>& nb) const {
- return nb.d_nv->d_nchildren > N;
+ /**
+ * Set this NodeBuilder to the `used' state.
+ */
+ inline void setUsed() {
+ Assert(!isUsed(), "Internal error: bad `used' state in NodeBuilder!");
+ Assert(d_inlineNv.d_nchildren == 0 &&
+ d_nvMaxChildren == d_inlineNvMaxChildren,
+ "Internal error: bad `inline' state in NodeBuilder!");
+ d_nv = NULL;
}
- bool evNeedsToBeAllocated() const {
- return d_nv->d_nchildren == d_size;
+ /**
+ * Set this NodeBuilder to the `unused' state. Should only be done
+ * from clear().
+ */
+ inline void setUnused() {
+ Assert(isUsed(), "Internal error: bad `used' state in NodeBuilder!");
+ Assert(d_inlineNv.d_nchildren == 0 &&
+ d_nvMaxChildren == d_inlineNvMaxChildren,
+ "Internal error: bad `inline' state in NodeBuilder!");
+ d_nv = &d_inlineNv;
}
- // realloc in the default way
- void realloc();
+ /**
+ * Returns true if d_nv is *not* the "in-line" one (it was
+ * heap-allocated by this class).
+ */
+ inline bool nvIsAllocated() const {
+ return EXPECT_FALSE( d_nv != &d_inlineNv ) && EXPECT_TRUE( d_nv != NULL );
+ }
- // realloc to a specific size
- void realloc(size_t toSize, bool copy = true);
+ /**
+ * Returns true if adding a child requires (re)allocation of d_nv
+ * first.
+ */
+ inline bool nvNeedsToBeAllocated() const {
+ return EXPECT_FALSE( d_nv->d_nchildren == d_nvMaxChildren );
+ }
- void allocateEvIfNecessaryForAppend() {
- if(EXPECT_FALSE( evNeedsToBeAllocated() )) {
+ /**
+ * (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).
+ */
+ inline void realloc() {
+ realloc(d_nvMaxChildren * 2);
+ }
+
+ /**
+ * (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.
+ */
+ inline void allocateNvIfNecessaryForAppend() {
+ if(EXPECT_FALSE( nvNeedsToBeAllocated() )) {
realloc();
}
}
- // dealloc: only call this with d_used == false and nvIsAllocated()
- inline void dealloc();
+ /**
+ * 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() {
- Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
- if(EXPECT_FALSE( nvIsAllocated() ) && EXPECT_TRUE( d_size > d_nv->d_nchildren )) {
- d_nv = (expr::NodeValue*)
- std::realloc(d_nv, sizeof(expr::NodeValue) +
- ( sizeof(expr::NodeValue*) * (d_size = d_nv->d_nchildren) ));
- if(d_nv == NULL) {
+ if(EXPECT_FALSE( nvIsAllocated() ) &&
+ EXPECT_TRUE( d_nvMaxChildren > d_nv->d_nchildren )) {
+ // Ensure d_nv is not modified on allocation failure
+ expr::NodeValue* newBlock = (expr::NodeValue*)
+ std::realloc(d_nv,
+ sizeof(expr::NodeValue) +
+ ( sizeof(expr::NodeValue*) * (d_nvMaxChildren = d_nv->d_nchildren) ));
+ if(newBlock == NULL) {
+ // In this case, d_nv was NOT freed. If we throw, the
+ // deallocation should occur on destruction of the
+ // NodeBuilder.
throw std::bad_alloc();
}
+ d_nv = newBlock;
}
}
- NodeBuilder& collapseTo(Kind k) {
- Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+ Builder& collapseTo(Kind k) {
AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR,
k, "illegal collapsing kind");
if(getKind() != k) {
- Node n = *this;
+ Node n = operator Node();
clear();
- d_nv->d_kind = k;
- append(n);
+ d_nv->d_kind = expr::NodeValue::kindToDKind(k);
+ return append(n);
}
- return *this;
+ return static_cast<Builder&>(*this);
}
+protected:
+
+ inline NodeBuilderBase(char* buf, unsigned maxChildren,
+ Kind k = kind::UNDEFINED_KIND);
+ inline NodeBuilderBase(char* buf, unsigned maxChildren,
+ NodeManager* nm, Kind k = kind::UNDEFINED_KIND);
+
+private:
+ // disallow copy or assignment of these base classes directly (there
+ // would be no backing store!)
+ NodeBuilderBase(const NodeBuilderBase& nb);
+ NodeBuilderBase& operator=(const NodeBuilderBase& nb);
+
public:
- inline NodeBuilder();
- inline NodeBuilder(Kind k);
- inline NodeBuilder(const NodeBuilder<nchild_thresh>& nb);
- template <unsigned N> inline NodeBuilder(const NodeBuilder<N>& nb);
- inline NodeBuilder(NodeManager* nm);
- inline NodeBuilder(NodeManager* nm, Kind k);
- inline ~NodeBuilder();
+ // Intentionally not virtual; we don't want a vtable. Don't
+ // override this in a derived class.
+ inline ~NodeBuilderBase();
typedef expr::NodeValue::iterator<true> iterator;
typedef expr::NodeValue::iterator<true> const_iterator;
- const_iterator begin() const {
- Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+ /** 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>();
}
- const_iterator end() const {
- Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+ /** 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>();
}
- Kind getKind() const {
- Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+ /** Get the kind of this Node-under-construction. */
+ inline Kind getKind() const {
+ Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
return d_nv->getKind();
}
- unsigned getNumChildren() const {
- Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+ /** Get the current number of children of this Node-under-construction. */
+ inline unsigned getNumChildren() const {
+ Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
return d_nv->getNumChildren();
}
- Node operator[](int i) const {
- Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
- Assert(i >= 0 && i < d_nv->getNumChildren());
+ /** Access to children of this Node-under-construction. */
+ inline Node operator[](int i) const {
+ Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+ Assert(i >= 0 && i < d_nv->getNumChildren(), "index out of range for NodeBuilder[]");
return Node(d_nv->d_children[i]);
}
/**
* "Reset" this node builder (optionally setting a new kind for it),
- * using the same memory as before. This should leave the
- * NodeBuilder<> in the state it was after initial construction.
+ * 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 BackedNodeBuilder 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
- NodeBuilder& operator<<(const Kind& k) {
- Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
- Assert(d_nv->getKind() == kind::UNDEFINED_KIND);
- d_nv->d_kind = k;
- return *this;
+ /** Set the Kind of this Node-under-construction. */
+ inline Builder& operator<<(const Kind& k) {
+ Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+ Assert(getKind() == kind::UNDEFINED_KIND,
+ "can't redefine the Kind of a NodeBuilder");
+ Assert(k != kind::UNDEFINED_KIND,
+ "can't define the Kind of a NodeBuilder to be UNDEFINED_KIND");
+ d_nv->d_kind = expr::NodeValue::kindToDKind(k);
+ return static_cast<Builder&>(*this);
}
- NodeBuilder& operator<<(TNode n) {
- // FIXME: collapse if ! UNDEFINED_KIND
- Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+ /**
+ * If this Node-under-construction has a Kind set, collapse it and
+ * append the given Node as a child. Otherwise, simply append.
+ * FIXME: do we really want that collapse behavior? We had agreed
+ * on it but then never wrote code like that.
+ */
+ Builder& operator<<(TNode n) {
+ Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+ /* FIXME: disable this "collapsing" for now..
+ if(EXPECT_FALSE( getKind() != kind::UNDEFINED_KIND )) {
+ Node n2 = operator Node();
+ clear();
+ append(n2);
+ }*/
return append(n);
}
- // For pushing sequences of children
- NodeBuilder& append(const std::vector<Node>& children) {
- Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+ /** Append a sequence of children to this Node-under-construction. */
+ inline Builder& append(const std::vector<Node>& children) {
+ Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
return append(children.begin(), children.end());
}
- NodeBuilder& append(TNode n) {
- Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
- Debug("node") << "append: " << this << " " << n << "[" << n.d_nv << "]" << std::endl;
- allocateEvIfNecessaryForAppend();
- expr::NodeValue* ev = n.d_nv;
- ev->inc();
- d_nv->d_children[d_nv->d_nchildren++] = ev;
- return *this;
- }
-
+ /** Append a sequence of children to this Node-under-construction. */
template <class Iterator>
- NodeBuilder& append(const Iterator& begin, const Iterator& end) {
- Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+ Builder& 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;
+ return static_cast<Builder&>(*this);
+ }
+
+ /** Append a child to this Node-under-construction. */
+ Builder& append(TNode n) {
+ Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+ allocateNvIfNecessaryForAppend();
+ expr::NodeValue* nv = n.d_nv;
+ nv->inc();
+ d_nv->d_children[d_nv->d_nchildren++] = nv;
+ return static_cast<Builder&>(*this);
}
+ // two versions, so we can support extraction from (const)
+ // NodeBuilders which are temporaries appearing as rvalues
operator Node();
operator Node() const;
inline void toStream(std::ostream& out) const {
- Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+ Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
d_nv->toStream(out);
}
- NodeBuilder& operator&=(TNode);
- NodeBuilder& operator|=(TNode);
- NodeBuilder& operator+=(TNode);
- NodeBuilder& operator-=(TNode);
- NodeBuilder& operator*=(TNode);
+ Builder& operator&=(TNode);
+ Builder& operator|=(TNode);
+ Builder& operator+=(TNode);
+ Builder& operator-=(TNode);
+ Builder& operator*=(TNode);
friend class AndNodeBuilder;
friend class OrNodeBuilder;
friend class PlusNodeBuilder;
friend class MultNodeBuilder;
- // Yet 1 more example of how terrifying C++ is as a language
+};/* class NodeBuilderBase */
+
+/**
+ * Backing-store interface version for NodeBuilders. To construct one
+ * of these, you need to create a backing store (preferably on the
+ * stack) for it to hold its "inline" NodeValue. There's a
+ * convenience macro defined below, makeStackNodeBuilder(b, N),
+ * defined below to define a stack-allocated BackedNodeBuilder "b"
+ * with room for N children on the stack.
+ */
+class BackedNodeBuilder : public NodeBuilderBase<BackedNodeBuilder> {
+public:
+ inline BackedNodeBuilder(char* buf, unsigned maxChildren) :
+ NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
+ }
+
+ inline BackedNodeBuilder(char* buf, unsigned maxChildren, Kind k) :
+ NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
+ }
+
+ inline BackedNodeBuilder(char* buf, unsigned maxChildren, NodeManager* nm) :
+ NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
+ }
+
+ inline BackedNodeBuilder(char* buf, unsigned maxChildren, NodeManager* nm, Kind k) :
+ NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
+ }
+
+ // we don't want a vtable, so do not declare a dtor!
+ //inline ~NodeBuilder();
+
+private:
+ // disallow copy or assignment (there would be no backing store!)
+ BackedNodeBuilder(const BackedNodeBuilder& nb);
+ BackedNodeBuilder& operator=(const BackedNodeBuilder& nb);
+
+};/* class BackedNodeBuilder */
+
+/**
+ * Stack-allocate a BackedNodeBuilder with a stack-allocated backing
+ * store of size __n. The BackedNodeBuilder will be named __v.
+ *
+ * __v must be a simple name. __n must be convertible to size_t, and
+ * will be evaluated only once. This macro may only be used where
+ * declarations are permitted.
+ */
+#define makeStackNodeBuilder(__v, __n) \
+ size_t __cvc4_backednodebuilder_nchildren__ ## __v = (__n); \
+ char __cvc4_backednodebuilder_buf__ ## __v \
+ [ sizeof(NodeValue) + \
+ sizeof(NodeValue*) * __cvc4_backednodebuilder_nchildren__ ## __v ] \
+ __attribute__((aligned(__WORDSIZE / 8))); \
+ BackedNodeBuilder __v(__cvc4_backednodebuilder_buf__ ## __v, \
+ __cvc4_backednodebuilder_nchildren__ ## __v)
+
+/**
+ * Simple NodeBuilder interface. This is a template that requires
+ * that the number of children of the "inline"-allocated NodeValue be
+ * specified as a template parameter (which means it must be a
+ * compile-time constant).
+ */
+template <unsigned nchild_thresh = default_nchild_thresh>
+class NodeBuilder : public NodeBuilderBase<NodeBuilder<nchild_thresh> > {
+ char d_backingStore[ sizeof(expr::NodeValue)
+ + (sizeof(expr::NodeValue*) * nchild_thresh) ]
+ __attribute__((aligned(__WORDSIZE / 8)));
+
+ typedef NodeBuilderBase<NodeBuilder<nchild_thresh> > super;
+
+ template <unsigned N>
+ void internalCopy(const NodeBuilder<N>& nb);
+
+public:
+ inline NodeBuilder() :
+ NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore, nchild_thresh) {
+ }
+
+ inline NodeBuilder(Kind k) :
+ NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore, nchild_thresh, k) {
+ }
+
+ inline NodeBuilder(NodeManager* nm) :
+ NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore, nchild_thresh, nm) {
+ }
+
+ inline NodeBuilder(NodeManager* nm, Kind k) :
+ NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore, nchild_thresh, nm, k) {
+ }
+
+ // These implementations are identical, but we need to have both of
+ // these because the templatized version isn't recognized as a
+ // generalization of a copy constructor (and a default copy
+ // constructor will be generated [?])
+ inline NodeBuilder(const NodeBuilder& nb) :
+ NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore,
+ nchild_thresh,
+ nb.d_nm,
+ nb.getKind()) {
+ internalCopy(nb);
+ }
+
+ // technically this is a conversion, not a copy
+ template <unsigned N>
+ inline NodeBuilder(const NodeBuilder<N>& nb) :
+ NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore,
+ nchild_thresh,
+ nb.d_nm,
+ nb.getKind()) {
+ internalCopy(nb);
+ }
+
+ // we don't want a vtable, so do not declare a dtor!
+ //inline ~NodeBuilder();
+
// This is needed for copy constructors of different sizes to access private fields
template <unsigned N>
friend class NodeBuilder;
-};/* class NodeBuilder */
+};/* class NodeBuilder<> */
// TODO: add templatized NodeTemplate<ref_count> to all above and
// below inlines for 'const [T]Node&' arguments? Technically a lot of
};/* class MultNodeBuilder */
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator&=(TNode e) {
+template <class Builder>
+inline Builder& NodeBuilderBase<Builder>::operator&=(TNode e) {
return collapseTo(kind::AND).append(e);
}
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator|=(TNode e) {
+template <class Builder>
+inline Builder& NodeBuilderBase<Builder>::operator|=(TNode e) {
return collapseTo(kind::OR).append(e);
}
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator+=(TNode e) {
+template <class Builder>
+inline Builder& NodeBuilderBase<Builder>::operator+=(TNode e) {
return collapseTo(kind::PLUS).append(e);
}
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator-=(TNode e) {
+template <class Builder>
+inline Builder& NodeBuilderBase<Builder>::operator-=(TNode e) {
return collapseTo(kind::PLUS).append(NodeManager::currentNM()->mkNode(kind::UMINUS, e));
}
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator*=(TNode e) {
+template <class Builder>
+inline Builder& NodeBuilderBase<Builder>::operator*=(TNode e) {
return collapseTo(kind::MULT).append(e);
}
#include "expr/node.h"
#include "expr/node_manager.h"
-// template implementations
-
namespace CVC4 {
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>::NodeBuilder() :
- d_size(nchild_thresh),
- d_hash(0),
- d_nm(NodeManager::currentNM()),
- d_used(false),
+template <class Builder>
+inline NodeBuilderBase<Builder>::NodeBuilderBase(char* buf, unsigned maxChildren, Kind k) :
+ d_inlineNv(*reinterpret_cast<expr::NodeValue*>(buf)),
d_nv(&d_inlineNv),
- d_inlineNv(0),
- d_childrenStorage() {}
-
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>::NodeBuilder(Kind k) :
- d_size(nchild_thresh),
- d_hash(0),
d_nm(NodeManager::currentNM()),
- d_used(false),
- d_nv(&d_inlineNv),
- d_inlineNv(0),
- d_childrenStorage() {
+ d_inlineNvMaxChildren(maxChildren),
+ d_nvMaxChildren(maxChildren) {
- d_inlineNv.d_kind = k;
+ d_inlineNv.d_id = 0;
+ d_inlineNv.d_rc = 0;
+ d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
+ d_inlineNv.d_nchildren = 0;
}
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<nchild_thresh>& nb) :
- d_size(nchild_thresh),
- d_hash(0),
- d_nm(nb.d_nm),
- d_used(nb.d_used),
- d_nv(&d_inlineNv),
- d_inlineNv(0),
- d_childrenStorage() {
-
- if(nvIsAllocated(nb)) {
- realloc(nb.d_size, false);
- std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_nv->nv_begin());
- } else {
- std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_inlineNv.nv_begin());
- }
- d_nv->d_kind = nb.d_nv->d_kind;
- d_nv->d_nchildren = nb.d_nv->d_nchildren;
- for(expr::NodeValue::nv_iterator i = d_nv->nv_begin();
- i != d_nv->nv_end();
- ++i) {
- (*i)->inc();
- }
-}
-
-template <unsigned nchild_thresh>
-template <unsigned N>
-inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<N>& nb) :
- d_size(nchild_thresh),
- d_hash(0),
- d_nm(NodeManager::currentNM()),
- d_used(nb.d_used),
+template <class Builder>
+inline NodeBuilderBase<Builder>::NodeBuilderBase(char* buf, unsigned maxChildren, NodeManager* nm, Kind k) :
+ d_inlineNv(*reinterpret_cast<expr::NodeValue*>(buf)),
d_nv(&d_inlineNv),
- d_inlineNv(0),
- d_childrenStorage() {
-
- if(nb.d_nv->d_nchildren > nchild_thresh) {
- realloc(nb.d_size, false);
- std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_nv->nv_begin());
- } else {
- std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_inlineNv.nv_begin());
- }
- d_nv->d_kind = nb.d_nv->d_kind;
- d_nv->d_nchildren = nb.d_nv->d_nchildren;
- for(expr::NodeValue::nv_iterator i = d_nv->nv_begin();
- i != d_nv->nv_end();
- ++i) {
- (*i)->inc();
- }
-}
-
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm) :
- d_size(nchild_thresh),
- d_hash(0),
d_nm(nm),
- d_used(false),
- d_nv(&d_inlineNv),
- d_inlineNv(0),
- d_childrenStorage() {
- d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND);
-}
+ d_inlineNvMaxChildren(maxChildren),
+ d_nvMaxChildren(maxChildren) {
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) :
- d_size(nchild_thresh),
- d_hash(0),
- d_nm(nm),
- d_used(false),
- d_nv(&d_inlineNv),
- d_inlineNv(0),
- d_childrenStorage() {
-
- d_inlineNv.d_kind = k;
+ d_inlineNv.d_id = 0;
+ d_inlineNv.d_rc = 0;
+ d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
+ d_inlineNv.d_nchildren = 0;
}
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>::~NodeBuilder() {
- if(!d_used) {
- // Warning("NodeBuilder unused at destruction\n");
- // Commented above, as it happens a lot, for example with exceptions
+template <class Builder>
+inline NodeBuilderBase<Builder>::~NodeBuilderBase() {
+ if(EXPECT_FALSE( nvIsAllocated() )) {
dealloc();
+ } else if(EXPECT_FALSE( !isUsed() )) {
+ decrRefCounts();
}
}
-template <unsigned nchild_thresh>
-void NodeBuilder<nchild_thresh>::clear(Kind k) {
- if(!d_used) {
- Warning("NodeBuilder unused at clear\n");
-
+template <class Builder>
+void NodeBuilderBase<Builder>::clear(Kind k) {
+ if(EXPECT_FALSE( nvIsAllocated() )) {
dealloc();
+ } else if(EXPECT_FALSE( !isUsed() )) {
+ decrRefCounts();
+ } else {
+ setUnused();
}
- d_size = nchild_thresh;
- d_hash = 0;
- d_nm = NodeManager::currentNM();
- d_used = false;
- d_nv = &d_inlineNv;
- d_inlineNv.d_kind = k;
- d_inlineNv.d_nchildren = 0;//FIXME leak
-}
-
-template <unsigned nchild_thresh>
-void NodeBuilder<nchild_thresh>::realloc() {
- if(EXPECT_FALSE( nvIsAllocated() )) {
- d_nv = (expr::NodeValue*)
- std::realloc(d_nv,
- sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size *= 2) ));
- if(d_nv == NULL) {
- throw std::bad_alloc();
- }
- } else {
- d_nv = (expr::NodeValue*)
- std::malloc(sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size *= 2) ));
- if(d_nv == NULL) {
- throw std::bad_alloc();
- }
- d_nv->d_id = 0;
- d_nv->d_rc = 0;
- d_nv->d_kind = d_inlineNv.d_kind;
- d_nv->d_nchildren = nchild_thresh;
- std::copy(d_inlineNv.d_children,
- d_inlineNv.d_children + nchild_thresh,
- d_nv->d_children);
+ d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
+ for(expr::NodeValue::nv_iterator i = d_inlineNv.nv_begin();
+ i != d_inlineNv.nv_end();
+ ++i) {
+ (*i)->dec();
}
+ d_inlineNv.d_nchildren = 0;
}
-template <unsigned nchild_thresh>
-void NodeBuilder<nchild_thresh>::realloc(size_t toSize, bool copy) {
- Assert( d_size < toSize );
+template <class Builder>
+void NodeBuilderBase<Builder>::realloc(size_t toSize) {
+ Assert( toSize > d_nvMaxChildren,
+ "attempt to realloc() a NodeBuilder to a smaller/equal size!" );
if(EXPECT_FALSE( nvIsAllocated() )) {
- d_nv = (expr::NodeValue*)
+ // Ensure d_nv is not modified on allocation failure
+ expr::NodeValue* newBlock = (expr::NodeValue*)
std::realloc(d_nv, sizeof(expr::NodeValue) +
- ( sizeof(expr::NodeValue*) * (d_size = toSize) ));
- if(d_nv == NULL) {
+ ( sizeof(expr::NodeValue*) * (d_nvMaxChildren = toSize) ));
+ if(newBlock == NULL) {
+ // In this case, d_nv was NOT freed. If we throw, the
+ // deallocation should occur on destruction of the NodeBuilder.
throw std::bad_alloc();
}
+ // Here, the copy (between two heap-allocated buffers) has already
+ // been done for us by the std::realloc().
+ d_nv = newBlock;
} else {
- d_nv = (expr::NodeValue*)
+ // Ensure d_nv is not modified on allocation failure
+ expr::NodeValue* newBlock = (expr::NodeValue*)
std::malloc(sizeof(expr::NodeValue) +
- ( sizeof(expr::NodeValue*) * (d_size = toSize) ));
- if(d_nv == NULL) {
+ ( sizeof(expr::NodeValue*) * (d_nvMaxChildren = toSize) ));
+ if(newBlock == NULL) {
throw std::bad_alloc();
}
+
+ d_nv = newBlock;
d_nv->d_id = 0;
d_nv->d_rc = 0;
d_nv->d_kind = d_inlineNv.d_kind;
- d_nv->d_nchildren = nchild_thresh;
- if(copy) {
- std::copy(d_inlineNv.d_children,
- d_inlineNv.d_children + nchild_thresh,
- d_nv->d_children);
- // inhibit decr'ing refcounts of children in dtor
- d_inlineNv.d_nchildren = 0;
- }
+ d_nv->d_nchildren = d_inlineNv.d_nchildren;
+
+ std::copy(d_inlineNv.d_children,
+ d_inlineNv.d_children + d_inlineNv.d_nchildren,
+ d_nv->d_children);
+
+ // ensure "inline" children don't get decremented in dtor
+ d_inlineNv.d_nchildren = 0;
}
}
-template <unsigned nchild_thresh>
-inline void NodeBuilder<nchild_thresh>::dealloc() {
- /* Prefer asserts to if() because usually these conditions have been
- * checked already, so we don't want to do a double-check in
- * production; these are just sanity checks for debug builds */
- Assert(!d_used, "Internal error: NodeBuilder: dealloc() called with d_used");
+template <class Builder>
+void NodeBuilderBase<Builder>::dealloc() {
+ Assert( nvIsAllocated(),
+ "Internal error: NodeBuilder: dealloc() called without a "
+ "private NodeBuilder-allocated buffer" );
for(expr::NodeValue::nv_iterator i = d_nv->nv_begin();
i != d_nv->nv_end();
++i) {
(*i)->dec();
}
- if(nvIsAllocated()) {
- free(d_nv);
+
+ free(d_nv);
+ d_nv = &d_inlineNv;
+ d_nvMaxChildren = d_inlineNvMaxChildren;
+}
+
+template <class Builder>
+void NodeBuilderBase<Builder>::decrRefCounts() {
+ Assert( !nvIsAllocated(),
+ "Internal error: NodeBuilder: decrRefCounts() called with a "
+ "private NodeBuilder-allocated buffer" );
+
+ for(expr::NodeValue::nv_iterator i = d_inlineNv.nv_begin();
+ i != d_inlineNv.nv_end();
+ ++i) {
+ (*i)->dec();
}
+
+ d_inlineNv.d_nchildren = 0;
}
-template <unsigned nchild_thresh>
-NodeBuilder<nchild_thresh>::operator Node() const {// const version
- Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
- Assert(d_nv->getKind() != kind::UNDEFINED_KIND,
+// NON-CONST VERSION OF NODE EXTRACTOR
+template <class Builder>
+NodeBuilderBase<Builder>::operator Node() {
+ Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+ Assert(getKind() != kind::UNDEFINED_KIND,
"Can't make an expression of an undefined kind!");
- if(d_nv->d_kind == kind::VARIABLE) {
- Assert(d_nv->d_nchildren == 0);
+ // NOTE: The comments in this function refer to the cases in the
+ // file comments at the top of this file.
+
+ // Case 0: If a VARIABLE
+ if(getKind() == kind::VARIABLE) {
+ /* 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. */
+
+ Assert( ! nvIsAllocated(),
+ "internal NodeBuilder error: "
+ "VARIABLE-kinded NodeBuilder is heap-allocated !?" );
+ Assert( d_inlineNv.d_nchildren == 0,
+ "improperly-formed VARIABLE-kinded NodeBuilder: "
+ "no children permitted" );
+
+ // we have to copy the inline NodeValue out
expr::NodeValue* nv = (expr::NodeValue*)
- std::malloc(sizeof(expr::NodeValue) +
- (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));// FIXME :: WTF??
+ std::malloc(sizeof(expr::NodeValue));
if(nv == NULL) {
throw std::bad_alloc();
}
+ // there are no children, so we don't have to worry about
+ // reference counts in this case.
nv->d_nchildren = 0;
- nv->d_kind = kind::VARIABLE;
+ nv->d_kind = expr::NodeValue::kindToDKind(kind::VARIABLE);
nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
nv->d_rc = 0;
- //d_used = true; // const version
- //d_nv = NULL; // const version
+ setUsed();
+ Debug("gc") << "creating node value " << nv
+ << " [" << nv->d_id << "]: " << nv->toString() << "\n";
return Node(nv);
}
- // implementation differs depending on whether the expression value
- // was malloc'ed or not
+ // Implementation differs depending on whether the NodeValue was
+ // malloc'ed or not and whether or not it's in the already-been-seen
+ // NodeManager pool of Nodes. See implementation notes at the top
+ // of this file.
+
+ if(EXPECT_TRUE( ! nvIsAllocated() )) {
+ /** Case 1. d_nv points to d_inlineNv: it is the backing store
+ ** supplied by the user (or derived class) **/
+
+ // Lookup the expression value in the pool we already have
+ expr::NodeValue* nv = d_nm->poolLookup(&d_inlineNv);
+ if(nv != NULL) {
+ /* Subcase (a): The Node under construction already exists in
+ * the NodeManager's 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.
+ */
+ decrRefCounts();
+ d_inlineNv.d_nchildren = 0;
+ setUsed();
+ Debug("gc") << "creating node value " << nv
+ << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+ return Node(nv);
+ } else {
+ /* Subcase (b): The Node under construction is NOT already in
+ * the NodeManager's pool. */
+
+ /* 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. */
+
+ // create the canonical expression value for this node
+ nv = (expr::NodeValue*)
+ std::malloc(sizeof(expr::NodeValue) +
+ ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));
+ if(nv == NULL) {
+ throw std::bad_alloc();
+ }
+ nv->d_nchildren = d_inlineNv.d_nchildren;
+ nv->d_kind = d_inlineNv.d_kind;
+ nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+ nv->d_rc = 0;
+
+ std::copy(d_inlineNv.d_children,
+ d_inlineNv.d_children + d_inlineNv.d_nchildren,
+ nv->d_children);
+
+ d_inlineNv.d_nchildren = 0;
+ setUsed();
+
+ d_nm->poolInsert(nv);
+ Debug("gc") << "creating node value " << nv
+ << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+ return Node(nv);
+ }
+ } else {
+ /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger
+ ** buffer that was heap-allocated by this NodeBuilder. **/
- if(EXPECT_FALSE( nvIsAllocated() )) {
// Lookup the expression value in the pool we already have (with insert)
expr::NodeValue* nv = d_nm->poolLookup(d_nv);
// If something else is there, we reuse it
if(nv != NULL) {
- // expression already exists in node manager
- //dealloc(); // const version
- //d_used = true; // const version
+ /* Subcase (a) The Node under construction already exists in the
+ * NodeManager's pool. */
+
+ /* 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. */
+
+ dealloc();
+ setUsed();
+ Debug("gc") << "creating node value " << nv
+ << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+ return Node(nv);
+ } else {
+ /* Subcase (b) The Node under construction is NOT already in the
+ * NodeManager's pool. */
+
+ /* 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. */
+
+ crop();
+ nv = d_nv;
+ nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+ d_nv = &d_inlineNv;
+ d_nvMaxChildren = d_inlineNvMaxChildren;
+ setUsed();
+ d_nm->poolInsert(nv);
+ Debug("gc") << "creating node value " << nv
+ << " [" << nv->d_id << "]: " << nv->toString() << "\n";
return Node(nv);
}
- // Otherwise copy children out
- nv = (expr::NodeValue*)
- std::malloc(sizeof(expr::NodeValue) +
- ( sizeof(expr::NodeValue*) * d_nv->d_nchildren ));
- if(nv == NULL) {
- throw std::bad_alloc();
- }
- nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
- nv->d_rc = 0;
- nv->d_kind = d_nv->d_kind;
- nv->d_nchildren = d_nv->d_nchildren;
- std::copy(d_nv->d_children,
- d_nv->d_children + d_nv->d_nchildren,
- nv->d_children);
- // inc child refcounts
- for(expr::NodeValue::nv_iterator i = nv->nv_begin();
- i != nv->nv_end();
- ++i) {
- (*i)->inc();
- }
- d_nm->poolInsert(nv);
- return Node(nv);
}
-
- // Lookup the expression value in the pool we already have
- expr::NodeValue* ev = d_nm->poolLookup(d_nv);
- //DANGER d_nv should be ptr-to-const in the above line b/c it points to d_inlineNv
- if(ev != NULL) {
- // expression already exists in node manager
- //d_used = true; // const version
- Debug("node") << "result: " << Node(ev) << std::endl;
- return Node(ev);
- }
-
- // otherwise create the canonical expression value for this node
- ev = (expr::NodeValue*)
- std::malloc(sizeof(expr::NodeValue) +
- ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));
- if(ev == NULL) {
- throw std::bad_alloc();
- }
- ev->d_nchildren = d_inlineNv.d_nchildren;
- ev->d_kind = d_inlineNv.d_kind;
- ev->d_id = expr::NodeValue::next_id++;// FIXME multithreading
- ev->d_rc = 0;
- std::copy(d_inlineNv.d_children,
- d_inlineNv.d_children + d_inlineNv.d_nchildren,
- ev->d_children);
- //d_used = true;
- //d_nv = NULL;
- //d_inlineNv.d_nchildren = 0;// inhibit decr'ing refcounts of children in dtor
- // inc child refcounts
- for(expr::NodeValue::nv_iterator i = ev->nv_begin();
- i != ev->nv_end();
- ++i) {
- (*i)->inc();
- }
-
- // Make the new expression
- d_nm->poolInsert(ev);
- return Node(ev);
}
-template <unsigned nchild_thresh>
-NodeBuilder<nchild_thresh>::operator Node() {// not const
- Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
- Assert(d_nv->getKind() != kind::UNDEFINED_KIND,
+// CONST VERSION OF NODE EXTRACTOR
+template <class Builder>
+NodeBuilderBase<Builder>::operator Node() const {
+ Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+ Assert(getKind() != kind::UNDEFINED_KIND,
"Can't make an expression of an undefined kind!");
- if(d_nv->d_kind == kind::VARIABLE) {
- Assert(d_nv->d_nchildren == 0);
+ // NOTE: The comments in this function refer to the cases in the
+ // file comments at the top of this file.
+
+ // Case 0: If a VARIABLE
+ if(getKind() == kind::VARIABLE) {
+ /* 0. If a VARIABLE, treat similarly to 1(b), except that we know
+ * there are no children, and we don't keep VARIABLE-kinded Nodes
+ * in the NodeManager pool. */
+
+ Assert( ! nvIsAllocated(),
+ "internal NodeBuilder error: "
+ "VARIABLE-kinded NodeBuilder is heap-allocated !?" );
+ Assert( d_inlineNv.d_nchildren == 0,
+ "improperly-formed VARIABLE-kinded NodeBuilder: "
+ "no children permitted" );
+
+ // we have to copy the inline NodeValue out
expr::NodeValue* nv = (expr::NodeValue*)
- std::malloc(sizeof(expr::NodeValue) +
- (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));// FIXME :: WTF??
+ std::malloc(sizeof(expr::NodeValue));
if(nv == NULL) {
throw std::bad_alloc();
}
+ // there are no children, so we don't have to worry about
+ // reference counts in this case.
nv->d_nchildren = 0;
- nv->d_kind = kind::VARIABLE;
+ nv->d_kind = expr::NodeValue::kindToDKind(kind::VARIABLE);
nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
nv->d_rc = 0;
- d_used = true;
- d_nv = NULL;
- Debug("node") << "result: " << Node(nv) << std::endl;
+ Debug("gc") << "creating node value " << nv
+ << " [" << nv->d_id << "]: " << nv->toString() << "\n";
return Node(nv);
}
- // implementation differs depending on whether the expression value
- // was malloc'ed or not
+ // Implementation differs depending on whether the NodeValue was
+ // malloc'ed or not and whether or not it's in the already-been-seen
+ // NodeManager pool of Nodes. See implementation notes at the top
+ // of this file.
+
+ if(EXPECT_TRUE( ! nvIsAllocated() )) {
+ /** Case 1. d_nv points to d_inlineNv: it is the backing store
+ ** supplied by the user (or derived class) **/
+
+ // Lookup the expression value in the pool we already have
+ expr::NodeValue* nv = d_nm->poolLookup(&d_inlineNv);
+ if(nv != NULL) {
+ /* Subcase (a): The Node under construction already exists in
+ * the NodeManager's pool. */
+
+ /* 1(a). The existing NodeManager pool entry is returned; we
+ * leave child reference counts alone and get them at
+ * NodeBuilder destruction time. */
+
+ Debug("gc") << "creating node value " << nv
+ << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+ return Node(nv);
+ } else {
+ /* Subcase (b): The Node under construction is NOT already in
+ * the NodeManager's pool. */
+
+ /* 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 cannot be marked as "used", so we increment all
+ * child reference counts (which will be decremented to match on
+ * destruction of the NodeBuilder). We return a Node wrapper
+ * for this new NodeValue, which increments its reference
+ * count. */
+
+ // create the canonical expression value for this node
+ nv = (expr::NodeValue*)
+ std::malloc(sizeof(expr::NodeValue) +
+ ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));
+ if(nv == NULL) {
+ throw std::bad_alloc();
+ }
+ nv->d_nchildren = d_inlineNv.d_nchildren;
+ nv->d_kind = d_inlineNv.d_kind;
+ nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+ nv->d_rc = 0;
+
+ std::copy(d_inlineNv.d_children,
+ d_inlineNv.d_children + d_inlineNv.d_nchildren,
+ nv->d_children);
+
+ for(expr::NodeValue::nv_iterator i = nv->nv_begin();
+ i != nv->nv_end();
+ ++i) {
+ (*i)->inc();
+ }
+
+ d_nm->poolInsert(nv);
+ Debug("gc") << "creating node value " << nv
+ << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+ return Node(nv);
+ }
+ } else {
+ /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger
+ ** buffer that was heap-allocated by this NodeBuilder. **/
- if(EXPECT_FALSE( nvIsAllocated() )) {
// Lookup the expression value in the pool we already have (with insert)
expr::NodeValue* nv = d_nm->poolLookup(d_nv);
// If something else is there, we reuse it
if(nv != NULL) {
- // expression already exists in node manager
- dealloc();
- d_used = true;
- Debug("node") << "result: " << Node(nv) << std::endl;
+ /* Subcase (a) The Node under construction already exists in the
+ * NodeManager's pool. */
+
+ /* 2(a). The existing NodeManager pool entry is returned; we
+ * leave child reference counts alone and get them at
+ * NodeBuilder destruction time. */
+
+ Debug("gc") << "creating node value " << nv
+ << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+ return Node(nv);
+ } else {
+ /* Subcase (b) The Node under construction is NOT already in the
+ * NodeManager's pool. */
+
+ /* 2(b). The heap-allocated d_nv cannot be "cropped" to the
+ * correct size; we create a copy, increment child reference
+ * counts, place this copy into the NodeManager pool, and return
+ * a Node wrapper around it. The child reference counts will be
+ * decremented to match at NodeBuilder destruction time. */
+
+ // create the canonical expression value for this node
+ nv = (expr::NodeValue*)
+ std::malloc(sizeof(expr::NodeValue) +
+ ( sizeof(expr::NodeValue*) * d_nv->d_nchildren ));
+ if(nv == NULL) {
+ throw std::bad_alloc();
+ }
+ nv->d_nchildren = d_nv->d_nchildren;
+ nv->d_kind = d_nv->d_kind;
+ nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+ nv->d_rc = 0;
+
+ std::copy(d_nv->d_children,
+ d_nv->d_children + d_nv->d_nchildren,
+ nv->d_children);
+
+ for(expr::NodeValue::nv_iterator i = nv->nv_begin();
+ i != nv->nv_end();
+ ++i) {
+ (*i)->inc();
+ }
+
+ d_nm->poolInsert(nv);
+ Debug("gc") << "creating node value " << nv
+ << " [" << nv->d_id << "]: " << nv->toString() << "\n";
return Node(nv);
}
- // Otherwise crop and set the expression value to the allocated one
- crop();
- nv = d_nv;
- nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
- d_nv = NULL;
- d_used = true;
- d_nm->poolInsert(nv);
- return Node(nv);
}
+}
- // Lookup the expression value in the pool we already have
- expr::NodeValue* ev = d_nm->poolLookup(&d_inlineNv);
- if(ev != NULL) {
- // expression already exists in node manager
- d_used = true;
- Debug("node") << "result: " << Node(ev) << std::endl;
- return Node(ev);
+template <unsigned nchild_thresh>
+template <unsigned N>
+void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) {
+ if(nb.isUsed()) {
+ super::setUsed();
+ return;
}
- // otherwise create the canonical expression value for this node
- ev = (expr::NodeValue*)
- std::malloc(sizeof(expr::NodeValue) +
- ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));
- if(ev == NULL) {
- throw std::bad_alloc();
+ if(nb.d_nvMaxChildren > super::d_nvMaxChildren) {
+ super::realloc(nb.d_nvMaxChildren);
}
- ev->d_nchildren = d_inlineNv.d_nchildren;
- ev->d_kind = d_inlineNv.d_kind;
- ev->d_id = expr::NodeValue::next_id++;// FIXME multithreading
- ev->d_rc = 0;
- std::copy(d_inlineNv.d_children,
- d_inlineNv.d_children + d_inlineNv.d_nchildren,
- ev->d_children);
- d_used = true;
- d_nv = NULL;
- d_inlineNv.d_nchildren = 0;// inhibit decr'ing refcounts of children in dtor
- // Make the new expression
- d_nm->poolInsert(ev);
- return Node(ev);
+ std::copy(nb.d_nv->nv_begin(),
+ nb.d_nv->nv_end(),
+ super::d_nv->nv_begin());
+
+ super::d_nv->d_nchildren = nb.d_nv->d_nchildren;
+
+ for(expr::NodeValue::nv_iterator i = super::d_nv->nv_begin();
+ i != super::d_nv->nv_end();
+ ++i) {
+ (*i)->inc();
+ }
}
-template <unsigned nchild_thresh>
+template <class Builder>
inline std::ostream& operator<<(std::ostream& out,
- const NodeBuilder<nchild_thresh>& b) {
+ const NodeBuilderBase<Builder>& b) {
b.toStream(out);
return out;
}
projects / cvc5.git / commitdiff