1 /********************* */
3 ** Original author: mdeters
4 ** Major contributors: none
5 ** Minor contributors (to current version): taking, dejan
6 ** This file is part of the CVC4 prototype.
7 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
8 ** Courant Institute of Mathematical Sciences
10 ** See the file COPYING in the top-level source directory for licensing
13 ** A builder interface for Nodes.
15 ** The idea is to permit a flexible and efficient (in the common
16 ** case) interface for building Nodes. The general pattern of use is
17 ** to create a NodeBuilder, set its kind, append children to it, then
18 ** "extract" the resulting Node. This resulting Node may be one that
19 ** already exists (the NodeManager keeps a table of all Nodes in the
20 ** system), or may be entirely new.
22 ** This implementation gets a bit hairy for a handful of reasons. We
23 ** want a user-supplied "in-line" buffer (probably on the stack, see
24 ** below) to hold the children, but then the number of children must
25 ** be known ahead of time. Therefore, if this buffer is overrun, we
26 ** need to heap-allocate a new buffer to hold the children.
28 ** Note that as children are added to a NodeBuilder, they are stored
29 ** as raw pointers-to-NodeValue. However, their reference counts are
30 ** carefully maintained.
32 ** When the "in-line" buffer "d_inlineNv" is superceded by a
33 ** heap-allocated buffer, we allocate the new buffer (a NodeValue
34 ** large enough to hold more children), copy the elements to it, and
35 ** mark d_inlineNv as having zero children. We do this last bit so
36 ** that we don't have to modify any child reference counts. The new
37 ** heap-allocated buffer "takes over" the reference counts of the old
38 ** "in-line" buffer. (If we didn't mark it as having zero children,
39 ** the destructor may improperly decrement the children's reference
42 ** There are then four normal cases at the end of a NodeBuilder's
45 ** 0. We have a VARIABLE-kinded Node. These are special (they have
46 ** no children and are all distinct by definition). They are
47 ** really a subcase of 1(b), below.
48 ** 1. d_nv points to d_inlineNv: it is the backing store supplied
49 ** by the user (or derived class).
50 ** (a) The Node under construction already exists in the
51 ** NodeManager's pool.
52 ** (b) The Node under construction is NOT already in the
53 ** NodeManager's pool.
54 ** 2. d_nv does NOT point to d_inlineNv: it is a new, larger buffer
55 ** that was heap-allocated by this NodeBuilder.
56 ** (a) The Node under construction already exists in the
57 ** NodeManager's pool.
58 ** (b) The Node under construction is NOT already in the
59 ** NodeManager's pool.
61 ** When a Node is extracted, we convert the NodeBuilder to a Node and
62 ** make sure the reference counts are properly maintained. That
63 ** means we must ensure there are no reference-counting errors among
64 ** the node's children, that the children aren't re-decremented on
65 ** clear() or NodeBuilder destruction, and that the returned Node
66 ** wraps a NodeValue with a reference count of 1.
68 ** 0. If a VARIABLE, treat similarly to 1(b), except that we
69 ** know there are no children (no reference counts to reason
70 ** about) and we don't keep VARIABLE-kinded Nodes in the
73 ** 1(a). Reference-counts for all children in d_inlineNv must be
74 ** decremented, and the NodeBuilder must be marked as "used"
75 ** and the number of children set to zero so that we don't
76 ** decrement them again on destruction. The existing
77 ** NodeManager pool entry is returned.
79 ** 1(b). A new heap-allocated NodeValue must be constructed and all
80 ** settings and children from d_inlineNv copied into it.
81 ** This new NodeValue is put into the NodeManager's pool.
82 ** The NodeBuilder is marked as "used" and the number of
83 ** children in d_inlineNv set to zero so that we don't
84 ** decrement child reference counts on destruction (the child
85 ** reference counts have been "taken over" by the new
86 ** NodeValue). We return a Node wrapper for this new
87 ** NodeValue, which increments its reference count.
89 ** 2(a). Reference counts for all children in d_nv must be
90 ** decremented. The NodeBuilder is marked as "used" and the
91 ** heap-allocated d_nv deleted. d_nv is repointed to
92 ** d_inlineNv so that destruction of the NodeBuilder doesn't
93 ** cause any problems. The existing NodeManager pool entry
96 ** 2(b). The heap-allocated d_nv is "cropped" to the correct size
97 ** (based on the number of children it _actually_ has). d_nv
98 ** is repointed to d_inlineNv so that destruction of the
99 ** NodeBuilder doesn't cause any problems, and the (old)
100 ** value it had is placed into the NodeManager's pool and
101 ** returned in a Node wrapper.
103 ** NOTE IN 1(b) AND 2(b) THAT we can NOT create Node wrapper
104 ** temporary for the NodeValue in the NodeBuilderBase<>::operator
105 ** Node() member function. If we create a temporary (for example by
106 ** writing Debug("builder") << Node(nv) << endl), the NodeValue will
107 ** have its reference count incremented from zero to one, then
108 ** decremented, which makes it eligible for collection before the
109 ** builder has even returned it! So this is a no-no.
111 ** There are also two cases when the NodeBuilder is clear()'ed:
113 ** 1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied
114 ** backing store): all d_inlineNv children have their reference
115 ** counts decremented, d_inlineNv.d_nchildren is set to zero,
116 ** and its kind is set to UNDEFINED_KIND.
118 ** 2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all
119 ** d_nv children have their reference counts decremented, d_nv
120 ** is deallocated, and d_nv is set to &d_inlineNv. d_inlineNv's
121 ** kind is set to UNDEFINED_KIND.
123 ** ... destruction is similar:
125 ** 1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied
126 ** backing store): all d_inlineNv children have their reference
127 ** counts decremented.
129 ** 2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all
130 ** d_nv children have their reference counts decremented, and
131 ** d_nv is deallocated.
133 ** Regarding the backing store (typically on the stack): the file
134 ** below provides three classes (two of them are templates):
136 ** template <class Builder> class NodeBuilderBase;
138 ** This is the base class for node builders. It can not be used
139 ** directly. It contains a shared implementation but is intended
140 ** to be subclassed. Derived classes supply its "in-line" buffer.
142 ** class BackedNodeBuilder;
144 ** This is the usable form for a user-supplied-backing-store node
145 ** builder. A user can allocate a buffer large enough for a
146 ** NodeValue with N children (say, on the stack), then pass a
147 ** pointer to this buffer, and the parameter N, to a
148 ** BackedNodeBuilder. It will use this buffer to build its
149 ** NodeValue until the number of children exceeds N; then it will
150 ** allocate d_nv on the heap.
152 ** To ensure that the buffer is properly-sized, it is recommended
153 ** to use the makeStackNodeBuilder(b, N) macro to make a
154 ** BackedNodeBuilder "b" with a stack-allocated buffer large
155 ** enough to hold N children.
157 ** template <unsigned nchild_thresh> class NodeBuilder;
159 ** This is the conceptually easiest form of NodeBuilder to use.
164 ** gives you a backing buffer with capacity for 10 children in
165 ** the same place as the NodeBuilder<> itself is allocated. You
166 ** can specify another size as a template parameter, but it must
167 ** be a compile-time constant (which is why the BackedNodeBuilder
168 ** creator-macro "makeStackNodeBuilder(b, N)" is sometimes
172 #include "cvc4_private.h"
174 /* strong dependency; make sure node is included first */
176 #include "type_node.h"
178 #ifndef __CVC4__NODE_BUILDER_H
179 #define __CVC4__NODE_BUILDER_H
186 static const unsigned default_nchild_thresh
= 10;
188 template <class Builder
>
189 class NodeBuilderBase
;
192 }/* CVC4 namespace */
194 #include "expr/kind.h"
195 #include "expr/metakind.h"
196 #include "util/Assert.h"
197 #include "expr/node_value.h"
198 #include "util/output.h"
202 template <class Builder
>
203 inline std::ostream
& operator<<(std::ostream
&, const NodeBuilderBase
<Builder
>&);
205 class AndNodeBuilder
;
207 class PlusNodeBuilder
;
208 class MultNodeBuilder
;
211 * A base class for NodeBuilders. When extending this class, use:
213 * class MyExtendedNodeBuilder :
214 * public NodeBuilderBase<MyExtendedNodeBuilder> { ... };
216 * This ensures that certain member functions return the right
217 * (derived) class type.
219 * There are no virtual functions here, and that should remain the
220 * case! This class is just used for sharing of implementation. Two
221 * types derive from it: BackedNodeBuilder (which allows for an
222 * external buffer), and the NodeBuilder<> template, which requires
223 * that you give it a compile-time constant backing-store size.
225 template <class Builder
>
226 class NodeBuilderBase
{
230 * A reference to an "in-line" stack-allocated buffer for use by the
233 expr::NodeValue
& d_inlineNv
;
236 * A pointer to the "current" NodeValue buffer; either &d_inlineNv
237 * or a heap-allocated one if d_inlineNv wasn't big enough.
239 expr::NodeValue
* d_nv
;
241 /** The NodeManager at play */
245 * The maximum number of children that can be held in this "in-line"
248 const uint16_t d_inlineNvMaxChildren
;
251 * The number of children allocated in d_nv.
253 uint16_t d_nvMaxChildren
;
256 * Returns whether or not this NodeBuilder has been "used"---i.e.,
257 * whether a Node has been extracted with operator Node().
258 * Internally, this state is represented by d_nv pointing to NULL.
260 inline bool isUsed() const {
261 return EXPECT_FALSE( d_nv
== NULL
);
265 * Set this NodeBuilder to the `used' state.
267 inline void setUsed() {
268 Assert(!isUsed(), "Internal error: bad `used' state in NodeBuilder!");
269 Assert(d_inlineNv
.d_nchildren
== 0 &&
270 d_nvMaxChildren
== d_inlineNvMaxChildren
,
271 "Internal error: bad `inline' state in NodeBuilder!");
276 * Set this NodeBuilder to the `unused' state. Should only be done
279 inline void setUnused() {
280 Assert(isUsed(), "Internal error: bad `used' state in NodeBuilder!");
281 Assert(d_inlineNv
.d_nchildren
== 0 &&
282 d_nvMaxChildren
== d_inlineNvMaxChildren
,
283 "Internal error: bad `inline' state in NodeBuilder!");
288 * Returns true if d_nv is *not* the "in-line" one (it was
289 * heap-allocated by this class).
291 inline bool nvIsAllocated() const {
292 return EXPECT_FALSE( d_nv
!= &d_inlineNv
) && EXPECT_TRUE( d_nv
!= NULL
);
296 * Returns true if adding a child requires (re)allocation of d_nv
299 inline bool nvNeedsToBeAllocated() const {
300 return EXPECT_FALSE( d_nv
->d_nchildren
== d_nvMaxChildren
);
304 * (Re)allocate d_nv using a default grow factor. Ensure that child
305 * pointers are copied into the new buffer, and if the "inline"
306 * NodeValue is evacuated, make sure its children won't be
307 * double-decremented later (on destruction/clear).
309 inline void realloc() {
310 realloc(d_nvMaxChildren
* 2);
314 * (Re)allocate d_nv to a specific size. Specify "copy" if the
315 * children should be copied; if they are, and if the "inline"
316 * NodeValue is evacuated, make sure its children won't be
317 * double-decremented later (on destruction/clear).
319 void realloc(size_t toSize
);
322 * If d_nv needs to be (re)allocated to add an additional child, do
323 * so using realloc(), which ensures child pointers are copied and
324 * that the reference counts of the "inline" NodeValue won't be
325 * double-decremented on destruction/clear. Otherwise, do nothing.
327 inline void allocateNvIfNecessaryForAppend() {
328 if(EXPECT_FALSE( nvNeedsToBeAllocated() )) {
334 * Deallocate a d_nv that was heap-allocated by this class during
335 * grow operations. (Marks this NodeValue no longer allocated so
336 * that double-deallocations don't occur.)
338 * PRECONDITION: only call this when nvIsAllocated() == true.
339 * POSTCONDITION: !nvIsAllocated()
344 * "Purge" the "inline" children. Decrement all their reference
345 * counts and set the number of children to zero.
347 * PRECONDITION: only call this when nvIsAllocated() == false.
348 * POSTCONDITION: d_inlineNv.d_nchildren == 0.
350 void decrRefCounts();
353 * Trim d_nv down to the size it needs to be for the number of
354 * children it has. Used when a Node is extracted from a
355 * NodeBuilder and we want the returned memory not to suffer from
356 * internal fragmentation. If d_nv was not heap-allocated by this
357 * class, or is already the right size, this function does nothing.
359 * @throws bad_alloc if the reallocation fails
362 if(EXPECT_FALSE( nvIsAllocated() ) &&
363 EXPECT_TRUE( d_nvMaxChildren
> d_nv
->d_nchildren
)) {
364 // Ensure d_nv is not modified on allocation failure
365 expr::NodeValue
* newBlock
= (expr::NodeValue
*)
367 sizeof(expr::NodeValue
) +
368 ( sizeof(expr::NodeValue
*) * d_nv
->d_nchildren
));
369 if(newBlock
== NULL
) {
370 // In this case, d_nv was NOT freed. If we throw, the
371 // deallocation should occur on destruction of the
373 throw std::bad_alloc();
375 d_nvMaxChildren
= d_nv
->d_nchildren
;
380 Builder
& collapseTo(Kind k
) {
381 AssertArgument(k
!= kind::UNDEFINED_KIND
&&
382 k
!= kind::NULL_EXPR
&&
384 k
, "illegal collapsing kind");
387 Node n
= operator Node();
389 d_nv
->d_kind
= expr::NodeValue::kindToDKind(k
);
392 return static_cast<Builder
&>(*this);
397 inline NodeBuilderBase(expr::NodeValue
* buf
, unsigned maxChildren
,
398 Kind k
= kind::UNDEFINED_KIND
);
399 inline NodeBuilderBase(expr::NodeValue
* buf
, unsigned maxChildren
,
400 NodeManager
* nm
, Kind k
= kind::UNDEFINED_KIND
);
403 // disallow copy or assignment of these base classes directly (there
404 // would be no backing store!)
405 NodeBuilderBase(const NodeBuilderBase
& nb
);
406 NodeBuilderBase
& operator=(const NodeBuilderBase
& nb
);
410 // Intentionally not virtual; we don't want a vtable. Don't
411 // override this in a derived class.
412 inline ~NodeBuilderBase();
414 typedef expr::NodeValue::iterator
< NodeTemplate
<true> > iterator
;
415 typedef expr::NodeValue::iterator
< NodeTemplate
<true> > const_iterator
;
417 /** Get the begin-const-iterator of this Node-under-construction. */
418 inline const_iterator
begin() const {
419 Assert(!isUsed(), "NodeBuilder is one-shot only; "
420 "attempt to access it after conversion");
421 return d_nv
->begin
< NodeTemplate
<true> >();
424 /** Get the end-const-iterator of this Node-under-construction. */
425 inline const_iterator
end() const {
426 Assert(!isUsed(), "NodeBuilder is one-shot only; "
427 "attempt to access it after conversion");
428 return d_nv
->end
< NodeTemplate
<true> >();
431 /** Get the kind of this Node-under-construction. */
432 inline Kind
getKind() const {
433 Assert(!isUsed(), "NodeBuilder is one-shot only; "
434 "attempt to access it after conversion");
435 return d_nv
->getKind();
438 /** Get the kind of this Node-under-construction. */
439 inline kind::MetaKind
getMetaKind() const {
440 Assert(!isUsed(), "NodeBuilder is one-shot only; "
441 "attempt to access it after conversion");
442 return d_nv
->getMetaKind();
445 /** Get the current number of children of this Node-under-construction. */
446 inline unsigned getNumChildren() const {
447 Assert(!isUsed(), "NodeBuilder is one-shot only; "
448 "attempt to access it after conversion");
449 return d_nv
->getNumChildren();
452 /** Access to children of this Node-under-construction. */
453 inline Node
operator[](int i
) const {
454 Assert(!isUsed(), "NodeBuilder is one-shot only; "
455 "attempt to access it after conversion");
456 Assert(i
>= 0 && unsigned(i
) < d_nv
->getNumChildren(),
457 "index out of range for NodeBuilder[]");
458 return Node(d_nv
->getChild(i
));
462 * "Reset" this node builder (optionally setting a new kind for it),
463 * using the same "inline" memory as at construction time. This
464 * deallocates NodeBuilder-allocated heap memory, if it was
465 * allocated, and decrements the reference counts of any currently
466 * children in the NodeBuilder.
468 * This should leave the BackedNodeBuilder in the state it was after
469 * initial construction, except for Kind, which is set to the
470 * argument (if provided), or UNDEFINED_KIND. In particular, the
471 * associated NodeManager is not affected by clear().
473 void clear(Kind k
= kind::UNDEFINED_KIND
);
475 // "Stream" expression constructor syntax
477 /** Set the Kind of this Node-under-construction. */
478 inline Builder
& operator<<(const Kind
& k
) {
479 Assert(!isUsed(), "NodeBuilder is one-shot only; "
480 "attempt to access it after conversion");
481 Assert(getKind() == kind::UNDEFINED_KIND
,
482 "can't redefine the Kind of a NodeBuilder");
483 AssertArgument(k
!= kind::UNDEFINED_KIND
&&
484 k
!= kind::NULL_EXPR
&&
486 k
, "illegal node-building kind");
487 d_nv
->d_kind
= expr::NodeValue::kindToDKind(k
);
488 return static_cast<Builder
&>(*this);
492 * If this Node-under-construction has a Kind set, collapse it and
493 * append the given Node as a child. Otherwise, simply append.
494 * FIXME: do we really want that collapse behavior? We had agreed
495 * on it but then never wrote code like that.
497 Builder
& operator<<(TNode n
) {
498 Assert(!isUsed(), "NodeBuilder is one-shot only; "
499 "attempt to access it after conversion");
500 /* FIXME: disable this "collapsing" for now..
501 if(EXPECT_FALSE( getKind() != kind::UNDEFINED_KIND )) {
502 Node n2 = operator Node();
509 /** Append a sequence of children to this TypeNode-under-construction. */
511 append(const std::vector
<TypeNode
>& children
) {
512 Assert(!isUsed(), "NodeBuilder is one-shot only; "
513 "attempt to access it after conversion");
514 return append(children
.begin(), children
.end());
517 /** Append a sequence of children to this Node-under-construction. */
518 template <bool ref_count
>
520 append(const std::vector
<NodeTemplate
<ref_count
> >& children
) {
521 Assert(!isUsed(), "NodeBuilder is one-shot only; "
522 "attempt to access it after conversion");
523 return append(children
.begin(), children
.end());
526 /** Append a sequence of children to this Node-under-construction. */
527 template <class Iterator
>
528 Builder
& append(const Iterator
& begin
, const Iterator
& end
) {
529 Assert(!isUsed(), "NodeBuilder is one-shot only; "
530 "attempt to access it after conversion");
531 for(Iterator i
= begin
; i
!= end
; ++i
) {
534 return static_cast<Builder
&>(*this);
537 /** Append a child to this Node-under-construction. */
538 Builder
& append(TNode n
) {
539 Assert(!isUsed(), "NodeBuilder is one-shot only; "
540 "attempt to access it after conversion");
541 Assert(!n
.isNull(), "Cannot use NULL Node as a child of a Node");
542 allocateNvIfNecessaryForAppend();
543 expr::NodeValue
* nv
= n
.d_nv
;
545 d_nv
->d_children
[d_nv
->d_nchildren
++] = nv
;
546 return static_cast<Builder
&>(*this);
549 /** Append a child to this Node-under-construction. */
550 Builder
& append(const TypeNode
& typeNode
) {
551 Assert(!isUsed(), "NodeBuilder is one-shot only; "
552 "attempt to access it after conversion");
553 Assert(!typeNode
.isNull(), "Cannot use NULL Node as a child of a Node");
554 allocateNvIfNecessaryForAppend();
555 expr::NodeValue
* nv
= typeNode
.d_nv
;
557 d_nv
->d_children
[d_nv
->d_nchildren
++] = nv
;
558 return static_cast<Builder
&>(*this);
563 /** Construct the node value out of the node builder */
564 expr::NodeValue
* constructNV();
565 expr::NodeValue
* constructNV() const;
569 /** Construct the Node out of the node builder */
570 Node
constructNode();
571 Node
constructNode() const;
573 /** Construct a Node on the heap out of the node builder */
574 Node
* constructNodePtr();
575 Node
* constructNodePtr() const;
577 /** Construction of the TypeNode out of the node builder */
578 TypeNode
constructTypeNode();
579 TypeNode
constructTypeNode() const;
581 // two versions, so we can support extraction from (const)
582 // NodeBuilders which are temporaries appearing as rvalues
584 operator Node() const;
586 inline void toStream(std::ostream
& out
, int depth
= -1) const {
587 Assert(!isUsed(), "NodeBuilder is one-shot only; "
588 "attempt to access it after conversion");
589 d_nv
->toStream(out
, depth
);
592 Builder
& operator&=(TNode
);
593 Builder
& operator|=(TNode
);
594 Builder
& operator+=(TNode
);
595 Builder
& operator-=(TNode
);
596 Builder
& operator*=(TNode
);
598 friend class AndNodeBuilder
;
599 friend class OrNodeBuilder
;
600 friend class PlusNodeBuilder
;
601 friend class MultNodeBuilder
;
603 };/* class NodeBuilderBase */
606 * Backing-store interface version for NodeBuilders. To construct one
607 * of these, you need to create a backing store (preferably on the
608 * stack) for it to hold its "inline" NodeValue. There's a
609 * convenience macro defined below, makeStackNodeBuilder(b, N),
610 * defined below to define a stack-allocated BackedNodeBuilder "b"
611 * with room for N children on the stack.
613 class BackedNodeBuilder
: public NodeBuilderBase
<BackedNodeBuilder
> {
615 inline BackedNodeBuilder(expr::NodeValue
* buf
, unsigned maxChildren
) :
616 NodeBuilderBase
<BackedNodeBuilder
>(buf
, maxChildren
) {
619 inline BackedNodeBuilder(expr::NodeValue
* buf
, unsigned maxChildren
, Kind k
) :
620 NodeBuilderBase
<BackedNodeBuilder
>(buf
, maxChildren
) {
623 inline BackedNodeBuilder(expr::NodeValue
* buf
,
624 unsigned maxChildren
,
626 NodeBuilderBase
<BackedNodeBuilder
>(buf
, maxChildren
) {
629 inline BackedNodeBuilder(expr::NodeValue
* buf
,
630 unsigned maxChildren
,
633 NodeBuilderBase
<BackedNodeBuilder
>(buf
, maxChildren
) {
636 // we don't want a vtable, so do not declare a dtor!
637 //inline ~BackedNodeBuilder();
640 // disallow copy or assignment (there would be no backing store!)
641 BackedNodeBuilder(const BackedNodeBuilder
& nb
);
642 BackedNodeBuilder
& operator=(const BackedNodeBuilder
& nb
);
644 };/* class BackedNodeBuilder */
647 * Stack-allocate a BackedNodeBuilder with a stack-allocated backing
648 * store of size __n. The BackedNodeBuilder will be named __v.
650 * __v must be a simple name. __n must be convertible to size_t, and
651 * will be evaluated only once. This macro may only be used where
652 * declarations are permitted.
654 #define makeStackNodeBuilder(__v, __n) \
655 const size_t __cvc4_backednodebuilder_nchildren__ ## __v = (__n); \
656 ::CVC4::expr::NodeValue __cvc4_backednodebuilder_buf__ ## __v \
657 [1 + ( ( ( sizeof(::CVC4::expr::NodeValue) + \
658 sizeof(::CVC4::expr::NodeValue*) + 1 ) / \
659 sizeof(::CVC4::expr::NodeValue*) ) * \
660 __cvc4_backednodebuilder_nchildren__ ## __v)]; \
661 ::CVC4::BackedNodeBuilder __v(__cvc4_backednodebuilder_buf__ ## __v, \
662 __cvc4_backednodebuilder_nchildren__ ## __v)
663 // IF THE ABOVE ASSERTION FAILS, write another compiler-specific
664 // version of makeStackNodeBuilder() that works for your compiler
665 // (even if it's suboptimal, ignoring its __n argument, and just
666 // creates a NodeBuilder<10>).
670 * Simple NodeBuilder interface. This is a template that requires
671 * that the number of children of the "inline"-allocated NodeValue be
672 * specified as a template parameter (which means it must be a
673 * compile-time constant).
675 template <unsigned nchild_thresh
= default_nchild_thresh
>
676 class NodeBuilder
: public NodeBuilderBase
<NodeBuilder
<nchild_thresh
> > {
678 // 1. This (anonymous) struct here must be a POD to avoid the
679 // compiler laying out things in a different way.
680 // 2. The layout is engineered carefully. We can't just
681 // stack-allocate enough bytes as a char[] because we break
682 // strict-aliasing rules. The first thing in the struct is a
683 // "NodeValue" so a pointer to this struct should be safely
684 // castable to a pointer to a NodeValue (same alignment).
685 struct BackingStore
{
687 expr::NodeValue
* c
[nchild_thresh
];
690 typedef NodeBuilderBase
<NodeBuilder
<nchild_thresh
> > super
;
692 template <unsigned N
>
693 void internalCopy(const NodeBuilder
<N
>& nb
);
696 inline NodeBuilder() :
697 NodeBuilderBase
<NodeBuilder
<nchild_thresh
> >
698 (reinterpret_cast<expr::NodeValue
*>(&d_backingStore
),
702 inline NodeBuilder(Kind k
) :
703 NodeBuilderBase
<NodeBuilder
<nchild_thresh
> >
704 (reinterpret_cast<expr::NodeValue
*>(&d_backingStore
),
709 inline NodeBuilder(NodeManager
* nm
) :
710 NodeBuilderBase
<NodeBuilder
<nchild_thresh
> >
711 (reinterpret_cast<expr::NodeValue
*>(&d_backingStore
),
716 inline NodeBuilder(NodeManager
* nm
, Kind k
) :
717 NodeBuilderBase
<NodeBuilder
<nchild_thresh
> >
718 (reinterpret_cast<expr::NodeValue
*>(&d_backingStore
),
724 // These implementations are identical, but we need to have both of
725 // these because the templatized version isn't recognized as a
726 // generalization of a copy constructor (and a default copy
727 // constructor will be generated [?])
728 inline NodeBuilder(const NodeBuilder
& nb
) :
729 NodeBuilderBase
<NodeBuilder
<nchild_thresh
> >
730 (reinterpret_cast<expr::NodeValue
*>(&d_backingStore
),
737 // technically this is a conversion, not a copy
738 template <unsigned N
>
739 inline NodeBuilder(const NodeBuilder
<N
>& nb
) :
740 NodeBuilderBase
<NodeBuilder
<nchild_thresh
> >
741 (reinterpret_cast<expr::NodeValue
*>(&d_backingStore
),
748 // we don't want a vtable, so do not declare a dtor!
749 //inline ~NodeBuilder();
751 // This is needed for copy constructors of different sizes to access
753 template <unsigned N
>
754 friend class NodeBuilder
;
756 };/* class NodeBuilder<> */
758 // TODO: add templatized NodeTemplate<ref_count> to all above and
759 // below inlines for 'const [T]Node&' arguments? Technically a lot of
760 // time is spent in the TNode conversion and copy constructor, but
761 // this should be optimized into a simple pointer copy (?)
762 // TODO: double-check this.
764 class AndNodeBuilder
{
768 inline AndNodeBuilder(const NodeBuilder
<>& eb
) : d_eb(eb
) {
769 d_eb
.collapseTo(kind::AND
);
772 inline AndNodeBuilder(TNode a
, TNode b
) : d_eb(kind::AND
) {
777 inline AndNodeBuilder
& operator&&(const NodeTemplate
<rc
>&);
780 inline OrNodeBuilder
operator||(const NodeTemplate
<rc
>&);
782 inline operator NodeBuilder
<>() { return d_eb
; }
783 inline operator Node() { return d_eb
; }
785 };/* class AndNodeBuilder */
787 class OrNodeBuilder
{
791 inline OrNodeBuilder(const NodeBuilder
<>& eb
) : d_eb(eb
) {
792 d_eb
.collapseTo(kind::OR
);
795 inline OrNodeBuilder(TNode a
, TNode b
) : d_eb(kind::OR
) {
800 inline AndNodeBuilder
operator&&(const NodeTemplate
<rc
>&);
803 inline OrNodeBuilder
& operator||(const NodeTemplate
<rc
>&);
805 inline operator NodeBuilder
<>() { return d_eb
; }
806 inline operator Node() { return d_eb
; }
808 };/* class OrNodeBuilder */
810 class PlusNodeBuilder
{
814 inline PlusNodeBuilder(const NodeBuilder
<>& eb
) : d_eb(eb
) {
815 d_eb
.collapseTo(kind::PLUS
);
818 inline PlusNodeBuilder(TNode a
, TNode b
) : d_eb(kind::PLUS
) {
823 inline PlusNodeBuilder
& operator+(const NodeTemplate
<rc
>&);
826 inline PlusNodeBuilder
& operator-(const NodeTemplate
<rc
>&);
829 inline MultNodeBuilder
operator*(const NodeTemplate
<rc
>&);
831 inline operator NodeBuilder
<>() { return d_eb
; }
832 inline operator Node() { return d_eb
; }
834 };/* class PlusNodeBuilder */
836 class MultNodeBuilder
{
840 inline MultNodeBuilder(const NodeBuilder
<>& eb
) : d_eb(eb
) {
841 d_eb
.collapseTo(kind::MULT
);
844 inline MultNodeBuilder(TNode a
, TNode b
) : d_eb(kind::MULT
) {
849 inline PlusNodeBuilder
operator+(const NodeTemplate
<rc
>&);
852 inline PlusNodeBuilder
operator-(const NodeTemplate
<rc
>&);
855 inline MultNodeBuilder
& operator*(const NodeTemplate
<rc
>&);
857 inline operator NodeBuilder
<>() { return d_eb
; }
858 inline operator Node() { return d_eb
; }
860 };/* class MultNodeBuilder */
862 template <class Builder
>
863 inline Builder
& NodeBuilderBase
<Builder
>::operator&=(TNode e
) {
864 return collapseTo(kind::AND
).append(e
);
867 template <class Builder
>
868 inline Builder
& NodeBuilderBase
<Builder
>::operator|=(TNode e
) {
869 return collapseTo(kind::OR
).append(e
);
872 template <class Builder
>
873 inline Builder
& NodeBuilderBase
<Builder
>::operator+=(TNode e
) {
874 return collapseTo(kind::PLUS
).append(e
);
877 template <class Builder
>
878 inline Builder
& NodeBuilderBase
<Builder
>::operator-=(TNode e
) {
879 return collapseTo(kind::PLUS
).
880 append(NodeManager::currentNM()->mkNode(kind::UMINUS
, e
));
883 template <class Builder
>
884 inline Builder
& NodeBuilderBase
<Builder
>::operator*=(TNode e
) {
885 return collapseTo(kind::MULT
).append(e
);
889 inline AndNodeBuilder
& AndNodeBuilder::operator&&(const NodeTemplate
<rc
>& n
) {
895 inline OrNodeBuilder
AndNodeBuilder::operator||(const NodeTemplate
<rc
>& n
) {
896 return OrNodeBuilder(Node(d_eb
), n
);
899 inline AndNodeBuilder
& operator&&(AndNodeBuilder
& a
,
900 const AndNodeBuilder
& b
) {
901 return a
&& Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
903 inline AndNodeBuilder
& operator&&(AndNodeBuilder
& a
,
904 const OrNodeBuilder
& b
) {
905 return a
&& Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
907 inline OrNodeBuilder
operator||(AndNodeBuilder
& a
,
908 const AndNodeBuilder
& b
) {
909 return a
|| Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
911 inline OrNodeBuilder
operator||(AndNodeBuilder
& a
,
912 const OrNodeBuilder
& b
) {
913 return a
|| Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
917 inline AndNodeBuilder
OrNodeBuilder::operator&&(const NodeTemplate
<rc
>& n
) {
918 return AndNodeBuilder(Node(d_eb
), n
);
922 inline OrNodeBuilder
& OrNodeBuilder::operator||(const NodeTemplate
<rc
>& n
) {
927 inline AndNodeBuilder
operator&&(OrNodeBuilder
& a
,
928 const AndNodeBuilder
& b
) {
929 return a
&& Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
931 inline AndNodeBuilder
operator&&(OrNodeBuilder
& a
,
932 const OrNodeBuilder
& b
) {
933 return a
&& Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
935 inline OrNodeBuilder
& operator||(OrNodeBuilder
& a
,
936 const AndNodeBuilder
& b
) {
937 return a
|| Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
939 inline OrNodeBuilder
& operator||(OrNodeBuilder
& a
,
940 const OrNodeBuilder
& b
) {
941 return a
|| Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
945 inline PlusNodeBuilder
& PlusNodeBuilder::operator+(const NodeTemplate
<rc
>& n
) {
951 inline PlusNodeBuilder
& PlusNodeBuilder::operator-(const NodeTemplate
<rc
>& n
) {
952 d_eb
.append(NodeManager::currentNM()->mkNode(kind::UMINUS
, n
));
957 inline MultNodeBuilder
PlusNodeBuilder::operator*(const NodeTemplate
<rc
>& n
) {
958 return MultNodeBuilder(Node(d_eb
), n
);
961 inline PlusNodeBuilder
& operator+(PlusNodeBuilder
& a
,
962 const PlusNodeBuilder
& b
) {
963 return a
+ Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
965 inline PlusNodeBuilder
& operator+(PlusNodeBuilder
& a
,
966 const MultNodeBuilder
& b
) {
967 return a
+ Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
969 inline PlusNodeBuilder
& operator-(PlusNodeBuilder
&a
,
970 const PlusNodeBuilder
& b
) {
971 return a
- Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
973 inline PlusNodeBuilder
& operator-(PlusNodeBuilder
& a
,
974 const MultNodeBuilder
& b
) {
975 return a
- Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
977 inline MultNodeBuilder
operator*(PlusNodeBuilder
& a
,
978 const PlusNodeBuilder
& b
) {
979 return a
* Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
981 inline MultNodeBuilder
operator*(PlusNodeBuilder
& a
,
982 const MultNodeBuilder
& b
) {
983 return a
* Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
987 inline PlusNodeBuilder
MultNodeBuilder::operator+(const NodeTemplate
<rc
>& n
) {
988 return PlusNodeBuilder(Node(d_eb
), n
);
992 inline PlusNodeBuilder
MultNodeBuilder::operator-(const NodeTemplate
<rc
>& n
) {
993 return PlusNodeBuilder(Node(d_eb
),
994 NodeManager::currentNM()->mkNode(kind::UMINUS
, n
));
998 inline MultNodeBuilder
& MultNodeBuilder::operator*(const NodeTemplate
<rc
>& n
) {
1003 inline PlusNodeBuilder
operator+(MultNodeBuilder
& a
,
1004 const PlusNodeBuilder
& b
) {
1005 return a
+ Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
1007 inline PlusNodeBuilder
operator+(MultNodeBuilder
& a
,
1008 const MultNodeBuilder
& b
) {
1009 return a
+ Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
1011 inline PlusNodeBuilder
operator-(MultNodeBuilder
& a
,
1012 const PlusNodeBuilder
& b
) {
1013 return a
- Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
1015 inline PlusNodeBuilder
operator-(MultNodeBuilder
& a
,
1016 const MultNodeBuilder
& b
) {
1017 return a
- Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
1019 inline MultNodeBuilder
& operator*(MultNodeBuilder
& a
,
1020 const PlusNodeBuilder
& b
) {
1021 return a
* Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
1023 inline MultNodeBuilder
& operator*(MultNodeBuilder
& a
,
1024 const MultNodeBuilder
& b
) {
1025 return a
* Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
1028 template <bool rc1
, bool rc2
>
1029 inline AndNodeBuilder
operator&&(const NodeTemplate
<rc1
>& a
,
1030 const NodeTemplate
<rc2
>& b
) {
1031 return AndNodeBuilder(a
, b
);
1034 template <bool rc1
, bool rc2
>
1035 inline OrNodeBuilder
operator||(const NodeTemplate
<rc1
>& a
,
1036 const NodeTemplate
<rc2
>& b
) {
1037 return OrNodeBuilder(a
, b
);
1040 template <bool rc1
, bool rc2
>
1041 inline PlusNodeBuilder
operator+(const NodeTemplate
<rc1
>& a
,
1042 const NodeTemplate
<rc2
>& b
) {
1043 return PlusNodeBuilder(a
, b
);
1046 template <bool rc1
, bool rc2
>
1047 inline PlusNodeBuilder
operator-(const NodeTemplate
<rc1
>& a
,
1048 const NodeTemplate
<rc2
>& b
) {
1049 return PlusNodeBuilder(a
, NodeManager::currentNM()->mkNode(kind::UMINUS
, b
));
1052 template <bool rc1
, bool rc2
>
1053 inline MultNodeBuilder
operator*(const NodeTemplate
<rc1
>& a
,
1054 const NodeTemplate
<rc2
>& b
) {
1055 return MultNodeBuilder(a
, b
);
1059 inline AndNodeBuilder
operator&&(const NodeTemplate
<rc
>& a
,
1060 const AndNodeBuilder
& b
) {
1061 return a
&& Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
1065 inline AndNodeBuilder
operator&&(const NodeTemplate
<rc
>& a
,
1066 const OrNodeBuilder
& b
) {
1067 return a
&& Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
1071 inline OrNodeBuilder
operator||(const NodeTemplate
<rc
>& a
,
1072 const AndNodeBuilder
& b
) {
1073 return a
|| Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
1077 inline OrNodeBuilder
operator||(const NodeTemplate
<rc
>& a
,
1078 const OrNodeBuilder
& b
) {
1079 return a
|| Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
1083 inline PlusNodeBuilder
operator+(const NodeTemplate
<rc
>& a
,
1084 const PlusNodeBuilder
& b
) {
1085 return a
+ Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
1089 inline PlusNodeBuilder
operator+(const NodeTemplate
<rc
>& a
,
1090 const MultNodeBuilder
& b
) {
1091 return a
+ Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
1095 inline PlusNodeBuilder
operator-(const NodeTemplate
<rc
>& a
,
1096 const PlusNodeBuilder
& b
) {
1097 return a
- Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
1101 inline PlusNodeBuilder
operator-(const NodeTemplate
<rc
>& a
,
1102 const MultNodeBuilder
& b
) {
1103 return a
- Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
1107 inline MultNodeBuilder
operator*(const NodeTemplate
<rc
>& a
,
1108 const PlusNodeBuilder
& b
) {
1109 return a
* Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
1113 inline MultNodeBuilder
operator*(const NodeTemplate
<rc
>& a
,
1114 const MultNodeBuilder
& b
) {
1115 return a
* Node(const_cast<NodeBuilder
<>&>(b
.d_eb
));
1119 inline NodeTemplate
<true> operator-(const NodeTemplate
<rc
>& a
) {
1120 return NodeManager::currentNM()->mkNode(kind::UMINUS
, a
);
1123 }/* CVC4 namespace */
1125 #include "expr/node.h"
1126 #include "expr/node_manager.h"
1130 template <class Builder
>
1131 inline NodeBuilderBase
<Builder
>::NodeBuilderBase(expr::NodeValue
* buf
,
1132 unsigned maxChildren
,
1136 d_nm(NodeManager::currentNM()),
1137 d_inlineNvMaxChildren(maxChildren
),
1138 d_nvMaxChildren(maxChildren
) {
1140 Assert(k
!= kind::NULL_EXPR
, "illegal Node-building kind");
1142 d_inlineNv
.d_id
= 0;
1143 d_inlineNv
.d_rc
= 0;
1144 d_inlineNv
.d_kind
= expr::NodeValue::kindToDKind(k
);
1145 d_inlineNv
.d_nchildren
= 0;
1148 template <class Builder
>
1149 inline NodeBuilderBase
<Builder
>::NodeBuilderBase(expr::NodeValue
* buf
,
1150 unsigned maxChildren
,
1156 d_inlineNvMaxChildren(maxChildren
),
1157 d_nvMaxChildren(maxChildren
) {
1159 Assert(k
!= kind::NULL_EXPR
, "illegal Node-building kind");
1161 d_inlineNv
.d_id
= 0;
1162 d_inlineNv
.d_rc
= 0;
1163 d_inlineNv
.d_kind
= expr::NodeValue::kindToDKind(k
);
1164 d_inlineNv
.d_nchildren
= 0;
1167 template <class Builder
>
1168 inline NodeBuilderBase
<Builder
>::~NodeBuilderBase() {
1169 if(EXPECT_FALSE( nvIsAllocated() )) {
1171 } else if(EXPECT_FALSE( !isUsed() )) {
1176 template <class Builder
>
1177 void NodeBuilderBase
<Builder
>::clear(Kind k
) {
1178 Assert(k
!= kind::NULL_EXPR
, "illegal Node-building clear kind");
1180 if(EXPECT_FALSE( nvIsAllocated() )) {
1182 } else if(EXPECT_FALSE( !isUsed() )) {
1188 d_inlineNv
.d_kind
= expr::NodeValue::kindToDKind(k
);
1189 for(expr::NodeValue::nv_iterator i
= d_inlineNv
.nv_begin();
1190 i
!= d_inlineNv
.nv_end();
1194 d_inlineNv
.d_nchildren
= 0;
1197 template <class Builder
>
1198 void NodeBuilderBase
<Builder
>::realloc(size_t toSize
) {
1199 Assert( toSize
> d_nvMaxChildren
,
1200 "attempt to realloc() a NodeBuilder to a smaller/equal size!" );
1202 if(EXPECT_FALSE( nvIsAllocated() )) {
1203 // Ensure d_nv is not modified on allocation failure
1204 expr::NodeValue
* newBlock
= (expr::NodeValue
*)
1205 std::realloc(d_nv
, sizeof(expr::NodeValue
) +
1206 ( sizeof(expr::NodeValue
*) * toSize
));
1207 if(newBlock
== NULL
) {
1208 // In this case, d_nv was NOT freed. If we throw, the
1209 // deallocation should occur on destruction of the NodeBuilder.
1210 throw std::bad_alloc();
1212 d_nvMaxChildren
= toSize
;
1213 // Here, the copy (between two heap-allocated buffers) has already
1214 // been done for us by the std::realloc().
1217 // Ensure d_nv is not modified on allocation failure
1218 expr::NodeValue
* newBlock
= (expr::NodeValue
*)
1219 std::malloc(sizeof(expr::NodeValue
) +
1220 ( sizeof(expr::NodeValue
*) * toSize
));
1221 if(newBlock
== NULL
) {
1222 throw std::bad_alloc();
1224 d_nvMaxChildren
= toSize
;
1229 d_nv
->d_kind
= d_inlineNv
.d_kind
;
1230 d_nv
->d_nchildren
= d_inlineNv
.d_nchildren
;
1232 std::copy(d_inlineNv
.d_children
,
1233 d_inlineNv
.d_children
+ d_inlineNv
.d_nchildren
,
1236 // ensure "inline" children don't get decremented in dtor
1237 d_inlineNv
.d_nchildren
= 0;
1241 template <class Builder
>
1242 void NodeBuilderBase
<Builder
>::dealloc() {
1243 Assert( nvIsAllocated(),
1244 "Internal error: NodeBuilder: dealloc() called without a "
1245 "private NodeBuilder-allocated buffer" );
1247 for(expr::NodeValue::nv_iterator i
= d_nv
->nv_begin();
1248 i
!= d_nv
->nv_end();
1255 d_nvMaxChildren
= d_inlineNvMaxChildren
;
1258 template <class Builder
>
1259 void NodeBuilderBase
<Builder
>::decrRefCounts() {
1260 Assert( !nvIsAllocated(),
1261 "Internal error: NodeBuilder: decrRefCounts() called with a "
1262 "private NodeBuilder-allocated buffer" );
1264 for(expr::NodeValue::nv_iterator i
= d_inlineNv
.nv_begin();
1265 i
!= d_inlineNv
.nv_end();
1270 d_inlineNv
.d_nchildren
= 0;
1274 template <class Builder
>
1275 TypeNode NodeBuilderBase
<Builder
>::constructTypeNode() {
1276 return TypeNode(constructNV());
1279 template <class Builder
>
1280 TypeNode NodeBuilderBase
<Builder
>::constructTypeNode() const {
1281 return TypeNode(constructNV());
1284 template <class Builder
>
1285 Node NodeBuilderBase
<Builder
>::constructNode() {
1286 return Node(constructNV());
1289 template <class Builder
>
1290 Node NodeBuilderBase
<Builder
>::constructNode() const {
1291 return Node(constructNV());
1294 template <class Builder
>
1295 Node
* NodeBuilderBase
<Builder
>::constructNodePtr() {
1296 return new Node(constructNV());
1299 template <class Builder
>
1300 Node
* NodeBuilderBase
<Builder
>::constructNodePtr() const {
1301 return new Node(constructNV());
1304 template <class Builder
>
1305 NodeBuilderBase
<Builder
>::operator Node() {
1306 return constructNode();
1309 template <class Builder
>
1310 NodeBuilderBase
<Builder
>::operator Node() const {
1311 return constructNode();
1314 template <class Builder
>
1315 expr::NodeValue
* NodeBuilderBase
<Builder
>::constructNV() {
1316 Assert(!isUsed(), "NodeBuilder is one-shot only; "
1317 "attempt to access it after conversion");
1318 Assert(getKind() != kind::UNDEFINED_KIND
,
1319 "Can't make an expression of an undefined kind!");
1321 // NOTE: The comments in this function refer to the cases in the
1322 // file comments at the top of this file.
1324 // Case 0: If a VARIABLE
1325 if(getMetaKind() == kind::metakind::VARIABLE
) {
1326 /* 0. If a VARIABLE, treat similarly to 1(b), except that we know
1327 * there are no children (no reference counts to reason about),
1328 * and we don't keep VARIABLE-kinded Nodes in the NodeManager
1331 Assert( ! nvIsAllocated(),
1332 "internal NodeBuilder error: "
1333 "VARIABLE-kinded NodeBuilder is heap-allocated !?" );
1334 Assert( d_inlineNv
.d_nchildren
== 0,
1335 "improperly-formed VARIABLE-kinded NodeBuilder: "
1336 "no children permitted" );
1338 // we have to copy the inline NodeValue out
1339 expr::NodeValue
* nv
= (expr::NodeValue
*)
1340 std::malloc(sizeof(expr::NodeValue
));
1342 throw std::bad_alloc();
1344 // there are no children, so we don't have to worry about
1345 // reference counts in this case.
1346 nv
->d_nchildren
= 0;
1347 nv
->d_kind
= d_nv
->d_kind
;
1348 nv
->d_id
= expr::NodeValue::next_id
++;// FIXME multithreading
1351 Debug("gc") << "creating node value " << nv
1352 << " [" << nv
->d_id
<< "]: " << nv
->toString() << "\n";
1356 // check that there are the right # of children for this kind
1357 Assert(getMetaKind() != kind::metakind::CONSTANT
,
1358 "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds");
1359 Assert(d_nv
->d_nchildren
>= kind::metakind::getLowerBoundForKind(getKind()),
1360 "Nodes with kind %s must have at least %u children (the one under "
1361 "construction has %u)",
1362 kind::kindToString(getKind()).c_str(),
1363 kind::metakind::getLowerBoundForKind(getKind()),
1365 Assert(d_nv
->d_nchildren
<= kind::metakind::getUpperBoundForKind(getKind()),
1366 "Nodes with kind %s must have at most %u children (the one under "
1367 "construction has %u)",
1368 kind::kindToString(getKind()).c_str(),
1369 kind::metakind::getUpperBoundForKind(getKind()),
1372 // Implementation differs depending on whether the NodeValue was
1373 // malloc'ed or not and whether or not it's in the already-been-seen
1374 // NodeManager pool of Nodes. See implementation notes at the top
1377 if(EXPECT_TRUE( ! nvIsAllocated() )) {
1378 /** Case 1. d_nv points to d_inlineNv: it is the backing store
1379 ** supplied by the user (or derived class) **/
1381 // Lookup the expression value in the pool we already have
1382 expr::NodeValue
* poolNv
= d_nm
->poolLookup(&d_inlineNv
);
1383 // If something else is there, we reuse it
1384 if(poolNv
!= NULL
) {
1385 /* Subcase (a): The Node under construction already exists in
1386 * the NodeManager's pool. */
1388 /* 1(a). Reference-counts for all children in d_inlineNv must be
1389 * decremented, and the NodeBuilder must be marked as "used" and
1390 * the number of children set to zero so that we don't decrement
1391 * them again on destruction. The existing NodeManager pool
1392 * entry is returned.
1395 d_inlineNv
.d_nchildren
= 0;
1399 /* Subcase (b): The Node under construction is NOT already in
1400 * the NodeManager's pool. */
1402 /* 1(b). A new heap-allocated NodeValue must be constructed and
1403 * all settings and children from d_inlineNv copied into it.
1404 * This new NodeValue is put into the NodeManager's pool. The
1405 * NodeBuilder is marked as "used" and the number of children in
1406 * d_inlineNv set to zero so that we don't decrement child
1407 * reference counts on destruction (the child reference counts
1408 * have been "taken over" by the new NodeValue). We return a
1409 * Node wrapper for this new NodeValue, which increments its
1410 * reference count. */
1412 // create the canonical expression value for this node
1413 expr::NodeValue
* nv
= (expr::NodeValue
*)
1414 std::malloc(sizeof(expr::NodeValue
) +
1415 ( sizeof(expr::NodeValue
*) * d_inlineNv
.d_nchildren
));
1417 throw std::bad_alloc();
1419 nv
->d_nchildren
= d_inlineNv
.d_nchildren
;
1420 nv
->d_kind
= d_inlineNv
.d_kind
;
1421 nv
->d_id
= expr::NodeValue::next_id
++;// FIXME multithreading
1424 std::copy(d_inlineNv
.d_children
,
1425 d_inlineNv
.d_children
+ d_inlineNv
.d_nchildren
,
1428 d_inlineNv
.d_nchildren
= 0;
1432 d_nm
->poolInsert(nv
);
1433 Debug("gc") << "creating node value " << nv
1434 << " [" << nv
->d_id
<< "]: " << *nv
<< "\n";
1438 /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger
1439 ** buffer that was heap-allocated by this NodeBuilder. **/
1441 // Lookup the expression value in the pool we already have (with insert)
1442 expr::NodeValue
* poolNv
= d_nm
->poolLookup(d_nv
);
1443 // If something else is there, we reuse it
1444 if(poolNv
!= NULL
) {
1445 /* Subcase (a): The Node under construction already exists in
1446 * the NodeManager's pool. */
1448 /* 2(a). Reference-counts for all children in d_nv must be
1449 * decremented. The NodeBuilder is marked as "used" and the
1450 * heap-allocated d_nv deleted. d_nv is repointed to d_inlineNv
1451 * so that destruction of the NodeBuilder doesn't cause any
1452 * problems. The existing NodeManager pool entry is
1459 /* Subcase (b) The Node under construction is NOT already in the
1460 * NodeManager's pool. */
1462 /* 2(b). The heap-allocated d_nv is "cropped" to the correct
1463 * size (based on the number of children it _actually_ has).
1464 * d_nv is repointed to d_inlineNv so that destruction of the
1465 * NodeBuilder doesn't cause any problems, and the (old) value
1466 * it had is placed into the NodeManager's pool and returned in
1467 * a Node wrapper. */
1470 expr::NodeValue
* nv
= d_nv
;
1471 nv
->d_id
= expr::NodeValue::next_id
++;// FIXME multithreading
1473 d_nvMaxChildren
= d_inlineNvMaxChildren
;
1477 d_nm
->poolInsert(nv
);
1478 Debug("gc") << "creating node value " << nv
1479 << " [" << nv
->d_id
<< "]: " << *nv
<< "\n";
1485 // CONST VERSION OF NODE EXTRACTOR
1486 template <class Builder
>
1487 expr::NodeValue
* NodeBuilderBase
<Builder
>::constructNV() const {
1488 Assert(!isUsed(), "NodeBuilder is one-shot only; "
1489 "attempt to access it after conversion");
1490 Assert(getKind() != kind::UNDEFINED_KIND
,
1491 "Can't make an expression of an undefined kind!");
1493 // NOTE: The comments in this function refer to the cases in the
1494 // file comments at the top of this file.
1496 // Case 0: If a VARIABLE
1497 if(getMetaKind() == kind::metakind::VARIABLE
) {
1498 /* 0. If a VARIABLE, treat similarly to 1(b), except that we know
1499 * there are no children (no reference counts to reason about),
1500 * and we don't keep VARIABLE-kinded Nodes in the NodeManager
1503 Assert( ! nvIsAllocated(),
1504 "internal NodeBuilder error: "
1505 "VARIABLE-kinded NodeBuilder is heap-allocated !?" );
1506 Assert( d_inlineNv
.d_nchildren
== 0,
1507 "improperly-formed VARIABLE-kinded NodeBuilder: "
1508 "no children permitted" );
1510 // we have to copy the inline NodeValue out
1511 expr::NodeValue
* nv
= (expr::NodeValue
*)
1512 std::malloc(sizeof(expr::NodeValue
));
1514 throw std::bad_alloc();
1516 // there are no children, so we don't have to worry about
1517 // reference counts in this case.
1518 nv
->d_nchildren
= 0;
1519 nv
->d_kind
= d_nv
->d_kind
;
1520 nv
->d_id
= expr::NodeValue::next_id
++;// FIXME multithreading
1522 Debug("gc") << "creating node value " << nv
1523 << " [" << nv
->d_id
<< "]: " << *nv
<< "\n";
1527 // check that there are the right # of children for this kind
1528 Assert(getMetaKind() != kind::metakind::CONSTANT
,
1529 "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds");
1530 Assert(d_nv
->d_nchildren
>= kind::metakind::getLowerBoundForKind(getKind()),
1531 "Nodes with kind %s must have at least %u children (the one under "
1532 "construction has %u)",
1533 kind::kindToString(getKind()).c_str(),
1534 kind::metakind::getLowerBoundForKind(getKind()),
1536 Assert(d_nv
->d_nchildren
<= kind::metakind::getUpperBoundForKind(getKind()),
1537 "Nodes with kind %s must have at most %u children (the one under "
1538 "construction has %u)",
1539 kind::kindToString(getKind()).c_str(),
1540 kind::metakind::getUpperBoundForKind(getKind()),
1543 // Implementation differs depending on whether the NodeValue was
1544 // malloc'ed or not and whether or not it's in the already-been-seen
1545 // NodeManager pool of Nodes. See implementation notes at the top
1548 if(EXPECT_TRUE( ! nvIsAllocated() )) {
1549 /** Case 1. d_nv points to d_inlineNv: it is the backing store
1550 ** supplied by the user (or derived class) **/
1552 // Lookup the expression value in the pool we already have
1553 expr::NodeValue
* poolNv
= d_nm
->poolLookup(&d_inlineNv
);
1554 // If something else is there, we reuse it
1555 if(poolNv
!= NULL
) {
1556 /* Subcase (a): The Node under construction already exists in
1557 * the NodeManager's pool. */
1559 /* 1(a). The existing NodeManager pool entry is returned; we
1560 * leave child reference counts alone and get them at
1561 * NodeBuilder destruction time. */
1565 /* Subcase (b): The Node under construction is NOT already in
1566 * the NodeManager's pool. */
1568 /* 1(b). A new heap-allocated NodeValue must be constructed and
1569 * all settings and children from d_inlineNv copied into it.
1570 * This new NodeValue is put into the NodeManager's pool. The
1571 * NodeBuilder cannot be marked as "used", so we increment all
1572 * child reference counts (which will be decremented to match on
1573 * destruction of the NodeBuilder). We return a Node wrapper
1574 * for this new NodeValue, which increments its reference
1577 // create the canonical expression value for this node
1578 expr::NodeValue
* nv
= (expr::NodeValue
*)
1579 std::malloc(sizeof(expr::NodeValue
) +
1580 ( sizeof(expr::NodeValue
*) * d_inlineNv
.d_nchildren
));
1582 throw std::bad_alloc();
1584 nv
->d_nchildren
= d_inlineNv
.d_nchildren
;
1585 nv
->d_kind
= d_inlineNv
.d_kind
;
1586 nv
->d_id
= expr::NodeValue::next_id
++;// FIXME multithreading
1589 std::copy(d_inlineNv
.d_children
,
1590 d_inlineNv
.d_children
+ d_inlineNv
.d_nchildren
,
1593 for(expr::NodeValue::nv_iterator i
= nv
->nv_begin();
1600 d_nm
->poolInsert(nv
);
1601 Debug("gc") << "creating node value " << nv
1602 << " [" << nv
->d_id
<< "]: " << *nv
<< "\n";
1606 /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger
1607 ** buffer that was heap-allocated by this NodeBuilder. **/
1609 // Lookup the expression value in the pool we already have (with insert)
1610 expr::NodeValue
* poolNv
= d_nm
->poolLookup(d_nv
);
1611 // If something else is there, we reuse it
1612 if(poolNv
!= NULL
) {
1613 /* Subcase (a): The Node under construction already exists in
1614 * the NodeManager's pool. */
1616 /* 2(a). The existing NodeManager pool entry is returned; we
1617 * leave child reference counts alone and get them at
1618 * NodeBuilder destruction time. */
1622 /* Subcase (b) The Node under construction is NOT already in the
1623 * NodeManager's pool. */
1625 /* 2(b). The heap-allocated d_nv cannot be "cropped" to the
1626 * correct size; we create a copy, increment child reference
1627 * counts, place this copy into the NodeManager pool, and return
1628 * a Node wrapper around it. The child reference counts will be
1629 * decremented to match at NodeBuilder destruction time. */
1631 // create the canonical expression value for this node
1632 expr::NodeValue
* nv
= (expr::NodeValue
*)
1633 std::malloc(sizeof(expr::NodeValue
) +
1634 ( sizeof(expr::NodeValue
*) * d_nv
->d_nchildren
));
1636 throw std::bad_alloc();
1638 nv
->d_nchildren
= d_nv
->d_nchildren
;
1639 nv
->d_kind
= d_nv
->d_kind
;
1640 nv
->d_id
= expr::NodeValue::next_id
++;// FIXME multithreading
1643 std::copy(d_nv
->d_children
,
1644 d_nv
->d_children
+ d_nv
->d_nchildren
,
1647 for(expr::NodeValue::nv_iterator i
= nv
->nv_begin();
1654 d_nm
->poolInsert(nv
);
1655 Debug("gc") << "creating node value " << nv
1656 << " [" << nv
->d_id
<< "]: " << *nv
<< "\n";
1662 template <unsigned nchild_thresh
>
1663 template <unsigned N
>
1664 void NodeBuilder
<nchild_thresh
>::internalCopy(const NodeBuilder
<N
>& nb
) {
1670 if(nb
.d_nvMaxChildren
> super::d_nvMaxChildren
) {
1671 super::realloc(nb
.d_nvMaxChildren
);
1674 std::copy(nb
.d_nv
->nv_begin(),
1676 super::d_nv
->nv_begin());
1678 super::d_nv
->d_nchildren
= nb
.d_nv
->d_nchildren
;
1680 for(expr::NodeValue::nv_iterator i
= super::d_nv
->nv_begin();
1681 i
!= super::d_nv
->nv_end();
1687 template <class Builder
>
1688 inline std::ostream
& operator<<(std::ostream
& out
,
1689 const NodeBuilderBase
<Builder
>& b
) {
1690 b
.toStream(out
, Node::setdepth::getDepth(out
));
1694 }/* CVC4 namespace */
1696 #endif /* __CVC4__NODE_BUILDER_H */