1 /********************* */
2 /*! \file node_builder.h
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Morgan Deters, Dejan Jovanovic, Christopher L. Conway
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
11 **
12 ** \brief A builder interface for Nodes.
13 **
14 ** A builder interface for Nodes.
15 **
16 ** The idea is to permit a flexible and efficient (in the common
17 ** case) interface for building Nodes. The general pattern of use is
18 ** to create a NodeBuilder, set its kind, append children to it, then
19 ** "extract" the resulting Node. This resulting Node may be one that
20 ** already exists (the NodeManager keeps a table of all Nodes in the
21 ** system), or may be entirely new.
22 **
23 ** This implementation gets a bit hairy for a handful of reasons. We
24 ** want a user-supplied "in-line" buffer (probably on the stack, see
25 ** below) to hold the children, but then the number of children must
26 ** be known ahead of time. Therefore, if this buffer is overrun, we
27 ** need to heap-allocate a new buffer to hold the children.
28 **
29 ** Note that as children are added to a NodeBuilder, they are stored
30 ** as raw pointers-to-NodeValue. However, their reference counts are
31 ** carefully maintained.
32 **
33 ** When the "in-line" buffer "d_inlineNv" is superceded by a
34 ** heap-allocated buffer, we allocate the new buffer (a NodeValue
35 ** large enough to hold more children), copy the elements to it, and
36 ** mark d_inlineNv as having zero children. We do this last bit so
37 ** that we don't have to modify any child reference counts. The new
38 ** heap-allocated buffer "takes over" the reference counts of the old
39 ** "in-line" buffer. (If we didn't mark it as having zero children,
40 ** the destructor may improperly decrement the children's reference
41 ** counts.)
42 **
43 ** There are then four normal cases at the end of a NodeBuilder's
44 ** life cycle:
45 **
46 ** 0. We have a VARIABLE-kinded Node. These are special (they have
47 ** no children and are all distinct by definition). They are
48 ** really a subcase of 1(b), below.
49 ** 1. d_nv points to d_inlineNv: it is the backing store supplied
50 ** by the user (or derived class).
51 ** (a) The Node under construction already exists in the
52 ** NodeManager's pool.
53 ** (b) The Node under construction is NOT already in the
54 ** NodeManager's pool.
55 ** 2. d_nv does NOT point to d_inlineNv: it is a new, larger buffer
56 ** that was heap-allocated by this NodeBuilder.
57 ** (a) The Node under construction already exists in the
58 ** NodeManager's pool.
59 ** (b) The Node under construction is NOT already in the
60 ** NodeManager's pool.
61 **
62 ** When a Node is extracted, we convert the NodeBuilder to a Node and
63 ** make sure the reference counts are properly maintained. That
64 ** means we must ensure there are no reference-counting errors among
65 ** the node's children, that the children aren't re-decremented on
66 ** clear() or NodeBuilder destruction, and that the returned Node
67 ** wraps a NodeValue with a reference count of 1.
68 **
69 ** 0. If a VARIABLE, treat similarly to 1(b), except that we
70 ** know there are no children (no reference counts to reason
71 ** about) and we don't keep VARIABLE-kinded Nodes in the
72 ** NodeManager pool.
73 **
74 ** 1(a). Reference-counts for all children in d_inlineNv must be
75 ** decremented, and the NodeBuilder must be marked as "used"
76 ** and the number of children set to zero so that we don't
77 ** decrement them again on destruction. The existing
78 ** NodeManager pool entry is returned.
79 **
80 ** 1(b). A new heap-allocated NodeValue must be constructed and all
81 ** settings and children from d_inlineNv copied into it.
82 ** This new NodeValue is put into the NodeManager's pool.
83 ** The NodeBuilder is marked as "used" and the number of
84 ** children in d_inlineNv set to zero so that we don't
85 ** decrement child reference counts on destruction (the child
86 ** reference counts have been "taken over" by the new
87 ** NodeValue). We return a Node wrapper for this new
88 ** NodeValue, which increments its reference count.
89 **
90 ** 2(a). Reference counts for all children in d_nv must be
91 ** decremented. The NodeBuilder is marked as "used" and the
92 ** heap-allocated d_nv deleted. d_nv is repointed to
93 ** d_inlineNv so that destruction of the NodeBuilder doesn't
94 ** cause any problems. The existing NodeManager pool entry
95 ** is returned.
96 **
97 ** 2(b). The heap-allocated d_nv is "cropped" to the correct size
98 ** (based on the number of children it _actually_ has). d_nv
99 ** is repointed to d_inlineNv so that destruction of the
100 ** NodeBuilder doesn't cause any problems, and the (old)
101 ** value it had is placed into the NodeManager's pool and
102 ** returned in a Node wrapper.
103 **
104 ** NOTE IN 1(b) AND 2(b) THAT we can NOT create Node wrapper
105 ** temporary for the NodeValue in the NodeBuilder<>::operator Node()
106 ** member function. If we create a temporary (for example by writing
107 ** Debug("builder") << Node(nv) << endl), the NodeValue will have its
108 ** reference count incremented from zero to one, then decremented,
109 ** which makes it eligible for collection before the builder has even
110 ** returned it! So this is a no-no.
111 **
112 ** There are also two cases when the NodeBuilder is clear()'ed:
113 **
114 ** 1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied
115 ** backing store): all d_inlineNv children have their reference
116 ** counts decremented, d_inlineNv.d_nchildren is set to zero,
117 ** and its kind is set to UNDEFINED_KIND.
118 **
119 ** 2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all
120 ** d_nv children have their reference counts decremented, d_nv
121 ** is deallocated, and d_nv is set to &d_inlineNv. d_inlineNv's
122 ** kind is set to UNDEFINED_KIND.
123 **
124 ** ... destruction is similar:
125 **
126 ** 1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied
127 ** backing store): all d_inlineNv children have their reference
128 ** counts decremented.
129 **
130 ** 2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all
131 ** d_nv children have their reference counts decremented, and
132 ** d_nv is deallocated.
133 **
134 ** Regarding the backing store (typically on the stack): the file
135 ** below provides the template:
136 **
137 ** template < unsigned nchild_thresh > class NodeBuilder;
138 **
139 ** The default:
140 **
141 ** NodeBuilder<> b;
142 **
143 ** gives you a backing buffer with capacity for 10 children in
144 ** the same place as the NodeBuilder<> itself is allocated. You
145 ** can specify another size as a template parameter, but it must
146 ** be a compile-time constant.
147 **/
148
149 #include "cvc4_private.h"
150
151 /* strong dependency; make sure node is included first */
152 #include "expr/node.h"
153 #include "expr/type_node.h"
154
155 #ifndef __CVC4__NODE_BUILDER_H
156 #define __CVC4__NODE_BUILDER_H
157
158 #include <cstdlib>
159 #include <iostream>
160 #include <memory>
161 #include <stdint.h>
162 #include <vector>
163
164 namespace CVC4 {
165 static const unsigned default_nchild_thresh = 10;
166
167 template <unsigned nchild_thresh>
168 class NodeBuilder;
169
170 class NodeManager;
171 }/* CVC4 namespace */
172
173 #include "base/cvc4_assert.h"
174 #include "base/output.h"
175 #include "expr/kind.h"
176 #include "expr/metakind.h"
177 #include "expr/node_value.h"
178
179
180 namespace CVC4 {
181
182 // Sometimes it's useful for debugging to output a NodeBuilder that
183 // isn't yet a Node..
184 template <unsigned nchild_thresh>
185 std::ostream& operator<<(std::ostream& out, const NodeBuilder<nchild_thresh>& nb);
186
187 /**
188 * The main template NodeBuilder.
189 */
190 template <unsigned nchild_thresh = default_nchild_thresh>
191 class NodeBuilder {
192 /**
193 * An "in-line" stack-allocated buffer for use by the
194 * NodeBuilder.
195 */
196 expr::NodeValue d_inlineNv;
197 /**
198 * Space for the children of the node being constructed. This is
199 * never accessed directly, but rather through
200 * d_inlineNv.d_children[i].
201 */
202 expr::NodeValue* d_inlineNvChildSpace[nchild_thresh];
203
204 /**
205 * A pointer to the "current" NodeValue buffer; either &d_inlineNv
206 * or a heap-allocated one if d_inlineNv wasn't big enough.
207 */
208 expr::NodeValue* d_nv;
209
210 /** The NodeManager at play */
211 NodeManager* d_nm;
212
213 /**
214 * The number of children allocated in d_nv.
215 */
216 uint32_t d_nvMaxChildren;
217
218 template <unsigned N>
219 void internalCopy(const NodeBuilder<N>& nb);
220
221 /**
222 * Returns whether or not this NodeBuilder has been "used"---i.e.,
223 * whether a Node has been extracted with operator Node().
224 * Internally, this state is represented by d_nv pointing to NULL.
225 */
isUsed()226 inline bool isUsed() const {
227 return __builtin_expect( ( d_nv == NULL ), false );
228 }
229
230 /**
231 * Set this NodeBuilder to the `used' state.
232 */
setUsed()233 inline void setUsed() {
234 Assert(!isUsed(), "Internal error: bad `used' state in NodeBuilder!");
235 Assert(d_inlineNv.d_nchildren == 0 &&
236 d_nvMaxChildren == nchild_thresh,
237 "Internal error: bad `inline' state in NodeBuilder!");
238 d_nv = NULL;
239 }
240
241 /**
242 * Set this NodeBuilder to the `unused' state. Should only be done
243 * from clear().
244 */
setUnused()245 inline void setUnused() {
246 Assert(isUsed(), "Internal error: bad `used' state in NodeBuilder!");
247 Assert(d_inlineNv.d_nchildren == 0 &&
248 d_nvMaxChildren == nchild_thresh,
249 "Internal error: bad `inline' state in NodeBuilder!");
250 d_nv = &d_inlineNv;
251 }
252
253 /**
254 * Returns true if d_nv is *not* the "in-line" one (it was
255 * heap-allocated by this class).
256 */
nvIsAllocated()257 inline bool nvIsAllocated() const {
258 return __builtin_expect( ( d_nv != &d_inlineNv ), false ) && __builtin_expect(( d_nv != NULL ), true );
259 }
260
261 /**
262 * Returns true if adding a child requires (re)allocation of d_nv
263 * first.
264 */
nvNeedsToBeAllocated()265 inline bool nvNeedsToBeAllocated() const {
266 return __builtin_expect( ( d_nv->d_nchildren == d_nvMaxChildren ), false );
267 }
268
269 /**
270 * (Re)allocate d_nv using a default grow factor. Ensure that child
271 * pointers are copied into the new buffer, and if the "inline"
272 * NodeValue is evacuated, make sure its children won't be
273 * double-decremented later (on destruction/clear).
274 */
realloc()275 inline void realloc() {
276 size_t newSize = 2 * size_t(d_nvMaxChildren);
277 size_t hardLimit = (1lu << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1;
278 realloc(__builtin_expect( ( newSize > hardLimit ), false ) ? hardLimit : newSize);
279 }
280
281 /**
282 * (Re)allocate d_nv to a specific size. Specify "copy" if the
283 * children should be copied; if they are, and if the "inline"
284 * NodeValue is evacuated, make sure its children won't be
285 * double-decremented later (on destruction/clear).
286 */
287 void realloc(size_t toSize);
288
289 /**
290 * If d_nv needs to be (re)allocated to add an additional child, do
291 * so using realloc(), which ensures child pointers are copied and
292 * that the reference counts of the "inline" NodeValue won't be
293 * double-decremented on destruction/clear. Otherwise, do nothing.
294 */
allocateNvIfNecessaryForAppend()295 inline void allocateNvIfNecessaryForAppend() {
296 if(__builtin_expect( ( nvNeedsToBeAllocated() ), false )) {
297 realloc();
298 }
299 }
300
301 /**
302 * Deallocate a d_nv that was heap-allocated by this class during
303 * grow operations. (Marks this NodeValue no longer allocated so
304 * that double-deallocations don't occur.)
305 *
306 * PRECONDITION: only call this when nvIsAllocated() == true.
307 * POSTCONDITION: !nvIsAllocated()
308 */
309 void dealloc();
310
311 /**
312 * "Purge" the "inline" children. Decrement all their reference
313 * counts and set the number of children to zero.
314 *
315 * PRECONDITION: only call this when nvIsAllocated() == false.
316 * POSTCONDITION: d_inlineNv.d_nchildren == 0.
317 */
318 void decrRefCounts();
319
320 /**
321 * Trim d_nv down to the size it needs to be for the number of
322 * children it has. Used when a Node is extracted from a
323 * NodeBuilder and we want the returned memory not to suffer from
324 * internal fragmentation. If d_nv was not heap-allocated by this
325 * class, or is already the right size, this function does nothing.
326 *
327 * @throws bad_alloc if the reallocation fails
328 */
crop()329 void crop() {
330 if(__builtin_expect( ( nvIsAllocated() ), false ) &&
331 __builtin_expect( ( d_nvMaxChildren > d_nv->d_nchildren ), true )) {
332 // Ensure d_nv is not modified on allocation failure
333 expr::NodeValue* newBlock = (expr::NodeValue*)
334 std::realloc(d_nv,
335 sizeof(expr::NodeValue) +
336 ( sizeof(expr::NodeValue*) * d_nv->d_nchildren ));
337 if(newBlock == NULL) {
338 // In this case, d_nv was NOT freed. If we throw, the
339 // deallocation should occur on destruction of the
340 // NodeBuilder.
341 throw std::bad_alloc();
342 }
343 d_nv = newBlock;
344 d_nvMaxChildren = d_nv->d_nchildren;
345 }
346 }
347
348 // used by convenience node builders
collapseTo(Kind k)349 NodeBuilder<nchild_thresh>& collapseTo(Kind k) {
350 AssertArgument(k != kind::UNDEFINED_KIND &&
351 k != kind::NULL_EXPR &&
352 k < kind::LAST_KIND,
353 k, "illegal collapsing kind");
354
355 if(getKind() != k) {
356 Node n = operator Node();
357 clear();
358 d_nv->d_kind = expr::NodeValue::kindToDKind(k);
359 d_nv->d_id = 1; // have a kind already
360 return append(n);
361 }
362 return *this;
363 }
364
365 public:
366
NodeBuilder()367 inline NodeBuilder() :
368 d_nv(&d_inlineNv),
369 d_nm(NodeManager::currentNM()),
370 d_nvMaxChildren(nchild_thresh) {
371
372 d_inlineNv.d_id = 0;
373 d_inlineNv.d_rc = 0;
374 d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND);
375 d_inlineNv.d_nchildren = 0;
376 }
377
NodeBuilder(Kind k)378 inline NodeBuilder(Kind k) :
379 d_nv(&d_inlineNv),
380 d_nm(NodeManager::currentNM()),
381 d_nvMaxChildren(nchild_thresh) {
382
383 Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND,
384 "illegal Node-building kind");
385
386 d_inlineNv.d_id = 1; // have a kind already
387 d_inlineNv.d_rc = 0;
388 d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
389 d_inlineNv.d_nchildren = 0;
390 }
391
NodeBuilder(NodeManager * nm)392 inline NodeBuilder(NodeManager* nm) :
393 d_nv(&d_inlineNv),
394 d_nm(nm),
395 d_nvMaxChildren(nchild_thresh) {
396
397 d_inlineNv.d_id = 0;
398 d_inlineNv.d_rc = 0;
399 d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND);
400 d_inlineNv.d_nchildren = 0;
401 }
402
NodeBuilder(NodeManager * nm,Kind k)403 inline NodeBuilder(NodeManager* nm, Kind k) :
404 d_nv(&d_inlineNv),
405 d_nm(nm),
406 d_nvMaxChildren(nchild_thresh) {
407
408 Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND,
409 "illegal Node-building kind");
410
411 d_inlineNv.d_id = 1; // have a kind already
412 d_inlineNv.d_rc = 0;
413 d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
414 d_inlineNv.d_nchildren = 0;
415 }
416
~NodeBuilder()417 inline ~NodeBuilder() {
418 if(__builtin_expect( ( nvIsAllocated() ), false )) {
419 dealloc();
420 } else if(__builtin_expect( ( !isUsed() ), false )) {
421 decrRefCounts();
422 }
423 }
424
425 // These implementations are identical, but we need to have both of
426 // these because the templatized version isn't recognized as a
427 // generalization of a copy constructor (and a default copy
428 // constructor will be generated [?])
NodeBuilder(const NodeBuilder & nb)429 inline NodeBuilder(const NodeBuilder& nb) :
430 d_nv(&d_inlineNv),
431 d_nm(nb.d_nm),
432 d_nvMaxChildren(nchild_thresh) {
433
434 d_inlineNv.d_id = nb.d_nv->d_id;
435 d_inlineNv.d_rc = 0;
436 d_inlineNv.d_kind = nb.d_nv->d_kind;
437 d_inlineNv.d_nchildren = 0;
438
439 internalCopy(nb);
440 }
441
442 // technically this is a conversion, not a copy
443 template <unsigned N>
NodeBuilder(const NodeBuilder<N> & nb)444 inline NodeBuilder(const NodeBuilder<N>& nb) :
445 d_nv(&d_inlineNv),
446 d_nm(nb.d_nm),
447 d_nvMaxChildren(nchild_thresh) {
448
449 d_inlineNv.d_id = nb.d_nv->d_id;
450 d_inlineNv.d_rc = 0;
451 d_inlineNv.d_kind = nb.d_nv->d_kind;
452 d_inlineNv.d_nchildren = 0;
453
454 internalCopy(nb);
455 }
456
457 typedef expr::NodeValue::iterator< NodeTemplate<true> > iterator;
458 typedef expr::NodeValue::iterator< NodeTemplate<true> > const_iterator;
459
460 /** Get the begin-const-iterator of this Node-under-construction. */
begin()461 inline const_iterator begin() const {
462 Assert(!isUsed(), "NodeBuilder is one-shot only; "
463 "attempt to access it after conversion");
464 Assert(getKind() != kind::UNDEFINED_KIND,
465 "Iterators over NodeBuilder<> are undefined "
466 "until a Kind is set");
467 return d_nv->begin< NodeTemplate<true> >();
468 }
469
470 /** Get the end-const-iterator of this Node-under-construction. */
end()471 inline const_iterator end() const {
472 Assert(!isUsed(), "NodeBuilder is one-shot only; "
473 "attempt to access it after conversion");
474 Assert(getKind() != kind::UNDEFINED_KIND,
475 "Iterators over NodeBuilder<> are undefined "
476 "until a Kind is set");
477 return d_nv->end< NodeTemplate<true> >();
478 }
479
480 /** Get the kind of this Node-under-construction. */
getKind()481 inline Kind getKind() const {
482 Assert(!isUsed(), "NodeBuilder is one-shot only; "
483 "attempt to access it after conversion");
484 return d_nv->getKind();
485 }
486
487 /** Get the kind of this Node-under-construction. */
getMetaKind()488 inline kind::MetaKind getMetaKind() const {
489 Assert(!isUsed(), "NodeBuilder is one-shot only; "
490 "attempt to access it after conversion");
491 Assert(getKind() != kind::UNDEFINED_KIND,
492 "The metakind of a NodeBuilder<> is undefined "
493 "until a Kind is set");
494 return d_nv->getMetaKind();
495 }
496
497 /** Get the current number of children of this Node-under-construction. */
getNumChildren()498 inline unsigned getNumChildren() const {
499 Assert(!isUsed(), "NodeBuilder is one-shot only; "
500 "attempt to access it after conversion");
501 Assert(getKind() != kind::UNDEFINED_KIND,
502 "The number of children of a NodeBuilder<> is undefined "
503 "until a Kind is set");
504 return d_nv->getNumChildren();
505 }
506
507 /**
508 * Access to the operator of this Node-under-construction. Only
509 * allowed if this NodeBuilder is unused, and has a defined kind
510 * that is of PARAMETERIZED metakind.
511 */
getOperator()512 inline Node getOperator() const {
513 Assert(!isUsed(), "NodeBuilder is one-shot only; "
514 "attempt to access it after conversion");
515 Assert(getKind() != kind::UNDEFINED_KIND,
516 "NodeBuilder<> operator access is not permitted "
517 "until a Kind is set");
518 Assert(getMetaKind() == kind::metakind::PARAMETERIZED,
519 "NodeBuilder<> operator access is only permitted "
520 "on parameterized kinds, not `%s'",
521 kind::kindToString(getKind()).c_str());
522 return Node(d_nv->getOperator());
523 }
524
525 /**
526 * Access to children of this Node-under-construction. Only allowed
527 * if this NodeBuilder is unused and has a defined kind.
528 */
getChild(int i)529 inline Node getChild(int i) const {
530 Assert(!isUsed(), "NodeBuilder is one-shot only; "
531 "attempt to access it after conversion");
532 Assert(getKind() != kind::UNDEFINED_KIND,
533 "NodeBuilder<> child access is not permitted "
534 "until a Kind is set");
535 Assert(i >= 0 && unsigned(i) < d_nv->getNumChildren(),
536 "index out of range for NodeBuilder::getChild()");
537 return Node(d_nv->getChild(i));
538 }
539
540 /** Access to children of this Node-under-construction. */
541 inline Node operator[](int i) const {
542 return getChild(i);
543 }
544
545 /**
546 * "Reset" this node builder (optionally setting a new kind for it),
547 * using the same "inline" memory as at construction time. This
548 * deallocates NodeBuilder-allocated heap memory, if it was
549 * allocated, and decrements the reference counts of any currently
550 * children in the NodeBuilder.
551 *
552 * This should leave the NodeBuilder in the state it was after
553 * initial construction, except for Kind, which is set to the
554 * argument, if provided, or UNDEFINED_KIND. In particular, the
555 * associated NodeManager is not affected by clear().
556 */
557 void clear(Kind k = kind::UNDEFINED_KIND);
558
559 // "Stream" expression constructor syntax
560
561 /** Set the Kind of this Node-under-construction. */
562 inline NodeBuilder<nchild_thresh>& operator<<(const Kind& k) {
563 Assert(!isUsed(), "NodeBuilder is one-shot only; "
564 "attempt to access it after conversion");
565 Assert(getKind() == kind::UNDEFINED_KIND || d_nv->d_id == 0,
566 "can't redefine the Kind of a NodeBuilder");
567 Assert(d_nv->d_id == 0,
568 "internal inconsistency with NodeBuilder: d_id != 0");
569 AssertArgument(k != kind::UNDEFINED_KIND &&
570 k != kind::NULL_EXPR &&
571 k < kind::LAST_KIND,
572 k, "illegal node-building kind");
573 // This test means: we didn't have a Kind at the beginning (on
574 // NodeBuilder construction or at the last clear()), but we do
575 // now. That means we appended a Kind with operator<<(Kind),
576 // which now (lazily) we'll collapse.
577 if(__builtin_expect( ( d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND ), false )) {
578 Node n2 = operator Node();
579 clear();
580 append(n2);
581 } else if(d_nv->d_nchildren == 0) {
582 d_nv->d_id = 1; // remember that we had a kind from the start
583 }
584 d_nv->d_kind = expr::NodeValue::kindToDKind(k);
585 return *this;
586 }
587
588 /**
589 * If this Node-under-construction has a Kind set, collapse it and
590 * append the given Node as a child. Otherwise, simply append.
591 */
592 NodeBuilder<nchild_thresh>& operator<<(TNode n) {
593 Assert(!isUsed(), "NodeBuilder is one-shot only; "
594 "attempt to access it after conversion");
595 // This test means: we didn't have a Kind at the beginning (on
596 // NodeBuilder construction or at the last clear()), but we do
597 // now. That means we appended a Kind with operator<<(Kind),
598 // which now (lazily) we'll collapse.
599 if(__builtin_expect( ( d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND ), false )) {
600 Node n2 = operator Node();
601 clear();
602 append(n2);
603 }
604 return append(n);
605 }
606
607 /**
608 * If this Node-under-construction has a Kind set, collapse it and
609 * append the given Node as a child. Otherwise, simply append.
610 */
611 NodeBuilder<nchild_thresh>& operator<<(TypeNode n) {
612 Assert(!isUsed(), "NodeBuilder is one-shot only; "
613 "attempt to access it after conversion");
614 // This test means: we didn't have a Kind at the beginning (on
615 // NodeBuilder construction or at the last clear()), but we do
616 // now. That means we appended a Kind with operator<<(Kind),
617 // which now (lazily) we'll collapse.
618 if(__builtin_expect( ( d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND ), false )) {
619 Node n2 = operator Node();
620 clear();
621 append(n2);
622 }
623 return append(n);
624 }
625
626 /** Append a sequence of children to this TypeNode-under-construction. */
627 inline NodeBuilder<nchild_thresh>&
append(const std::vector<TypeNode> & children)628 append(const std::vector<TypeNode>& children) {
629 Assert(!isUsed(), "NodeBuilder is one-shot only; "
630 "attempt to access it after conversion");
631 return append(children.begin(), children.end());
632 }
633
634 /** Append a sequence of children to this Node-under-construction. */
635 template <bool ref_count>
636 inline NodeBuilder<nchild_thresh>&
append(const std::vector<NodeTemplate<ref_count>> & children)637 append(const std::vector<NodeTemplate<ref_count> >& children) {
638 Assert(!isUsed(), "NodeBuilder is one-shot only; "
639 "attempt to access it after conversion");
640 return append(children.begin(), children.end());
641 }
642
643 /** Append a sequence of children to this Node-under-construction. */
644 template <class Iterator>
append(const Iterator & begin,const Iterator & end)645 NodeBuilder<nchild_thresh>& append(const Iterator& begin, const Iterator& end) {
646 Assert(!isUsed(), "NodeBuilder is one-shot only; "
647 "attempt to access it after conversion");
648 for(Iterator i = begin; i != end; ++i) {
649 append(*i);
650 }
651 return *this;
652 }
653
654 /** Append a child to this Node-under-construction. */
append(TNode n)655 NodeBuilder<nchild_thresh>& append(TNode n) {
656 Assert(!isUsed(), "NodeBuilder is one-shot only; "
657 "attempt to access it after conversion");
658 Assert(!n.isNull(), "Cannot use NULL Node as a child of a Node");
659 if(n.getKind() == kind::BUILTIN) {
660 return *this << NodeManager::operatorToKind(n);
661 }
662 allocateNvIfNecessaryForAppend();
663 expr::NodeValue* nv = n.d_nv;
664 nv->inc();
665 d_nv->d_children[d_nv->d_nchildren++] = nv;
666 Assert(d_nv->d_nchildren <= d_nvMaxChildren);
667 return *this;
668 }
669
670 /** Append a child to this Node-under-construction. */
append(const TypeNode & typeNode)671 NodeBuilder<nchild_thresh>& append(const TypeNode& typeNode) {
672 Assert(!isUsed(), "NodeBuilder is one-shot only; "
673 "attempt to access it after conversion");
674 Assert(!typeNode.isNull(), "Cannot use NULL Node as a child of a Node");
675 allocateNvIfNecessaryForAppend();
676 expr::NodeValue* nv = typeNode.d_nv;
677 nv->inc();
678 d_nv->d_children[d_nv->d_nchildren++] = nv;
679 Assert(d_nv->d_nchildren <= d_nvMaxChildren);
680 return *this;
681 }
682
683 private:
684
685 /** Construct the node value out of the node builder */
686 expr::NodeValue* constructNV();
687 expr::NodeValue* constructNV() const;
688
689 #ifdef CVC4_DEBUG
690 // Throws a TypeCheckingExceptionPrivate on a failure.
691 void maybeCheckType(const TNode n) const;
692 #else /* CVC4_DEBUG */
693 // Do nothing if not in debug mode.
maybeCheckType(const TNode n)694 inline void maybeCheckType(const TNode n) const {}
695 #endif /* CVC4_DEBUG */
696
697 public:
698
699 /** Construct the Node out of the node builder */
700 Node constructNode();
701 Node constructNode() const;
702
703 /** Construct a Node on the heap out of the node builder */
704 Node* constructNodePtr();
705 Node* constructNodePtr() const;
706
707 /** Construction of the TypeNode out of the node builder */
708 TypeNode constructTypeNode();
709 TypeNode constructTypeNode() const;
710
711 // two versions, so we can support extraction from (const)
712 // NodeBuilders which are temporaries appearing as rvalues
713 operator Node();
714 operator Node() const;
715
716 // similarly for TypeNode
717 operator TypeNode();
718 operator TypeNode() const;
719
720 NodeBuilder<nchild_thresh>& operator&=(TNode);
721 NodeBuilder<nchild_thresh>& operator|=(TNode);
722 NodeBuilder<nchild_thresh>& operator+=(TNode);
723 NodeBuilder<nchild_thresh>& operator-=(TNode);
724 NodeBuilder<nchild_thresh>& operator*=(TNode);
725
726 // This is needed for copy constructors of different sizes to access
727 // private fields
728 template <unsigned N>
729 friend class NodeBuilder;
730
731 template <unsigned N>
732 friend std::ostream& operator<<(std::ostream& out, const NodeBuilder<N>& nb);
733
734 };/* class NodeBuilder<> */
735
736 }/* CVC4 namespace */
737
738 // TODO: add templatized NodeTemplate<ref_count> to all above and
739 // below inlines for 'const [T]Node&' arguments? Technically a lot of
740 // time is spent in the TNode conversion and copy constructor, but
741 // this should be optimized into a simple pointer copy (?)
742 // TODO: double-check this.
743
744 #include "expr/node.h"
745 #include "expr/node_manager.h"
746 #include "options/expr_options.h"
747
748 namespace CVC4 {
749
750 template <unsigned nchild_thresh>
clear(Kind k)751 void NodeBuilder<nchild_thresh>::clear(Kind k) {
752 Assert(k != kind::NULL_EXPR, "illegal Node-building clear kind");
753
754 if(__builtin_expect( ( nvIsAllocated() ), false )) {
755 dealloc();
756 } else if(__builtin_expect( ( !isUsed() ), false )) {
757 decrRefCounts();
758 } else {
759 setUnused();
760 }
761
762 d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
763 for(expr::NodeValue::nv_iterator i = d_inlineNv.nv_begin();
764 i != d_inlineNv.nv_end();
765 ++i) {
766 (*i)->dec();
767 }
768 d_inlineNv.d_nchildren = 0;
769 // keep track of whether or not we hvae a kind already
770 d_inlineNv.d_id = (k == kind::UNDEFINED_KIND) ? 0 : 1;
771 }
772
773 template <unsigned nchild_thresh>
realloc(size_t toSize)774 void NodeBuilder<nchild_thresh>::realloc(size_t toSize) {
775 Assert( toSize > d_nvMaxChildren,
776 "attempt to realloc() a NodeBuilder to a smaller/equal size!" );
777 Assert( toSize < (1lu << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN),
778 "attempt to realloc() a NodeBuilder to size %u (beyond hard limit of %u)",
779 toSize, (1lu << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1 );
780
781 if(__builtin_expect( ( nvIsAllocated() ), false )) {
782 // Ensure d_nv is not modified on allocation failure
783 expr::NodeValue* newBlock = (expr::NodeValue*)
784 std::realloc(d_nv, sizeof(expr::NodeValue) +
785 ( sizeof(expr::NodeValue*) * toSize ));
786 if(newBlock == NULL) {
787 // In this case, d_nv was NOT freed. If we throw, the
788 // deallocation should occur on destruction of the NodeBuilder.
789 throw std::bad_alloc();
790 }
791 d_nvMaxChildren = toSize;
792 Assert(d_nvMaxChildren == toSize);//overflow check
793 // Here, the copy (between two heap-allocated buffers) has already
794 // been done for us by the std::realloc().
795 d_nv = newBlock;
796 } else {
797 // Ensure d_nv is not modified on allocation failure
798 expr::NodeValue* newBlock = (expr::NodeValue*)
799 std::malloc(sizeof(expr::NodeValue) +
800 ( sizeof(expr::NodeValue*) * toSize ));
801 if(newBlock == NULL) {
802 throw std::bad_alloc();
803 }
804 d_nvMaxChildren = toSize;
805 Assert(d_nvMaxChildren == toSize);//overflow check
806
807 d_nv = newBlock;
808 d_nv->d_id = d_inlineNv.d_id;
809 d_nv->d_rc = 0;
810 d_nv->d_kind = d_inlineNv.d_kind;
811 d_nv->d_nchildren = d_inlineNv.d_nchildren;
812
813 std::copy(d_inlineNv.d_children,
814 d_inlineNv.d_children + d_inlineNv.d_nchildren,
815 d_nv->d_children);
816
817 // ensure "inline" children don't get decremented in dtor
818 d_inlineNv.d_nchildren = 0;
819 }
820 }
821
822 template <unsigned nchild_thresh>
dealloc()823 void NodeBuilder<nchild_thresh>::dealloc() {
824 Assert( nvIsAllocated(),
825 "Internal error: NodeBuilder: dealloc() called without a "
826 "private NodeBuilder-allocated buffer" );
827
828 for(expr::NodeValue::nv_iterator i = d_nv->nv_begin();
829 i != d_nv->nv_end();
830 ++i) {
831 (*i)->dec();
832 }
833
834 free(d_nv);
835 d_nv = &d_inlineNv;
836 d_nvMaxChildren = nchild_thresh;
837 }
838
839 template <unsigned nchild_thresh>
decrRefCounts()840 void NodeBuilder<nchild_thresh>::decrRefCounts() {
841 Assert( !nvIsAllocated(),
842 "Internal error: NodeBuilder: decrRefCounts() called with a "
843 "private NodeBuilder-allocated buffer" );
844
845 for(expr::NodeValue::nv_iterator i = d_inlineNv.nv_begin();
846 i != d_inlineNv.nv_end();
847 ++i) {
848 (*i)->dec();
849 }
850
851 d_inlineNv.d_nchildren = 0;
852 }
853
854
855 template <unsigned nchild_thresh>
constructTypeNode()856 TypeNode NodeBuilder<nchild_thresh>::constructTypeNode() {
857 return TypeNode(constructNV());
858 }
859
860 template <unsigned nchild_thresh>
constructTypeNode()861 TypeNode NodeBuilder<nchild_thresh>::constructTypeNode() const {
862 return TypeNode(constructNV());
863 }
864
865 template <unsigned nchild_thresh>
constructNode()866 Node NodeBuilder<nchild_thresh>::constructNode() {
867 Node n = Node(constructNV());
868 maybeCheckType(n);
869 return n;
870 }
871
872 template <unsigned nchild_thresh>
constructNode()873 Node NodeBuilder<nchild_thresh>::constructNode() const {
874 Node n = Node(constructNV());
875 maybeCheckType(n);
876 return n;
877 }
878
879 template <unsigned nchild_thresh>
constructNodePtr()880 Node* NodeBuilder<nchild_thresh>::constructNodePtr() {
881 // maybeCheckType() can throw an exception. Make sure to call the destructor
882 // on the exception branch.
883 std::unique_ptr<Node> np(new Node(constructNV()));
884 maybeCheckType(*np.get());
885 return np.release();
886 }
887
888 template <unsigned nchild_thresh>
constructNodePtr()889 Node* NodeBuilder<nchild_thresh>::constructNodePtr() const {
890 std::unique_ptr<Node> np(new Node(constructNV()));
891 maybeCheckType(*np.get());
892 return np.release();
893 }
894
895 template <unsigned nchild_thresh>
Node()896 NodeBuilder<nchild_thresh>::operator Node() {
897 return constructNode();
898 }
899
900 template <unsigned nchild_thresh>
Node()901 NodeBuilder<nchild_thresh>::operator Node() const {
902 return constructNode();
903 }
904
905 template <unsigned nchild_thresh>
TypeNode()906 NodeBuilder<nchild_thresh>::operator TypeNode() {
907 return constructTypeNode();
908 }
909
910 template <unsigned nchild_thresh>
TypeNode()911 NodeBuilder<nchild_thresh>::operator TypeNode() const {
912 return constructTypeNode();
913 }
914
915 template <unsigned nchild_thresh>
constructNV()916 expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
917 Assert(!isUsed(), "NodeBuilder is one-shot only; "
918 "attempt to access it after conversion");
919 Assert(getKind() != kind::UNDEFINED_KIND,
920 "Can't make an expression of an undefined kind!");
921
922 // NOTE: The comments in this function refer to the cases in the
923 // file comments at the top of this file.
924
925 // Case 0: If a VARIABLE
926 if(getMetaKind() == kind::metakind::VARIABLE || getMetaKind() == kind::metakind::NULLARY_OPERATOR) {
927 /* 0. If a VARIABLE, treat similarly to 1(b), except that we know
928 * there are no children (no reference counts to reason about),
929 * and we don't keep VARIABLE-kinded Nodes in the NodeManager
930 * pool. */
931
932 Assert( ! nvIsAllocated(),
933 "internal NodeBuilder error: "
934 "VARIABLE-kinded NodeBuilder is heap-allocated !?" );
935 Assert( d_inlineNv.d_nchildren == 0,
936 "improperly-formed VARIABLE-kinded NodeBuilder: "
937 "no children permitted" );
938
939 // we have to copy the inline NodeValue out
940 expr::NodeValue* nv = (expr::NodeValue*)
941 std::malloc(sizeof(expr::NodeValue));
942 if(nv == NULL) {
943 throw std::bad_alloc();
944 }
945 // there are no children, so we don't have to worry about
946 // reference counts in this case.
947 nv->d_nchildren = 0;
948 nv->d_kind = d_nv->d_kind;
949 nv->d_id = d_nm->next_id++;// FIXME multithreading
950 nv->d_rc = 0;
951 setUsed();
952 if(Debug.isOn("gc")) {
953 Debug("gc") << "creating node value " << nv
954 << " [" << nv->d_id << "]: ";
955 nv->printAst(Debug("gc"));
956 Debug("gc") << std::endl;
957 }
958 return nv;
959 }
960
961 // check that there are the right # of children for this kind
962 Assert(getMetaKind() != kind::metakind::CONSTANT,
963 "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds");
964 Assert(getNumChildren() >= kind::metakind::getLowerBoundForKind(getKind()),
965 "Nodes with kind %s must have at least %u children (the one under "
966 "construction has %u)",
967 kind::kindToString(getKind()).c_str(),
968 kind::metakind::getLowerBoundForKind(getKind()),
969 getNumChildren());
970 Assert(getNumChildren() <= kind::metakind::getUpperBoundForKind(getKind()),
971 "Nodes with kind %s must have at most %u children (the one under "
972 "construction has %u)",
973 kind::kindToString(getKind()).c_str(),
974 kind::metakind::getUpperBoundForKind(getKind()),
975 getNumChildren());
976
977 #if 0
978 // if the kind is PARAMETERIZED, check that the operator is correctly-kinded
979 Assert(kind::metaKindOf(getKind()) != kind::metakind::PARAMETERIZED ||
980 NodeManager::operatorToKind(getOperator()) == getKind(),
981 "Attempted to construct a parameterized kind `%s' with "
982 "incorrectly-kinded operator `%s'",
983 kind::kindToString(getKind()).c_str(),
984 kind::kindToString(getOperator().getKind()).c_str());
985 #endif /* 0 */
986
987 // Implementation differs depending on whether the NodeValue was
988 // malloc'ed or not and whether or not it's in the already-been-seen
989 // NodeManager pool of Nodes. See implementation notes at the top
990 // of this file.
991
992 if(__builtin_expect( ( ! nvIsAllocated() ), true )) {
993 /** Case 1. d_nv points to d_inlineNv: it is the backing store
994 ** allocated "inline" in this NodeBuilder. **/
995
996 // Lookup the expression value in the pool we already have
997 expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv);
998 // If something else is there, we reuse it
999 if(poolNv != NULL) {
1000 /* Subcase (a): The Node under construction already exists in
1001 * the NodeManager's pool. */
1002
1003 /* 1(a). Reference-counts for all children in d_inlineNv must be
1004 * decremented, and the NodeBuilder must be marked as "used" and
1005 * the number of children set to zero so that we don't decrement
1006 * them again on destruction. The existing NodeManager pool
1007 * entry is returned.
1008 */
1009 decrRefCounts();
1010 d_inlineNv.d_nchildren = 0;
1011 setUsed();
1012 return poolNv;
1013 } else {
1014 /* Subcase (b): The Node under construction is NOT already in
1015 * the NodeManager's pool. */
1016
1017 /* 1(b). A new heap-allocated NodeValue must be constructed and
1018 * all settings and children from d_inlineNv copied into it.
1019 * This new NodeValue is put into the NodeManager's pool. The
1020 * NodeBuilder is marked as "used" and the number of children in
1021 * d_inlineNv set to zero so that we don't decrement child
1022 * reference counts on destruction (the child reference counts
1023 * have been "taken over" by the new NodeValue). We return a
1024 * Node wrapper for this new NodeValue, which increments its
1025 * reference count. */
1026
1027 // create the canonical expression value for this node
1028 expr::NodeValue* nv = (expr::NodeValue*)
1029 std::malloc(sizeof(expr::NodeValue) +
1030 ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));
1031 if(nv == NULL) {
1032 throw std::bad_alloc();
1033 }
1034 nv->d_nchildren = d_inlineNv.d_nchildren;
1035 nv->d_kind = d_inlineNv.d_kind;
1036 nv->d_id = d_nm->next_id++;// FIXME multithreading
1037 nv->d_rc = 0;
1038
1039 std::copy(d_inlineNv.d_children,
1040 d_inlineNv.d_children + d_inlineNv.d_nchildren,
1041 nv->d_children);
1042
1043 d_inlineNv.d_nchildren = 0;
1044 setUsed();
1045
1046 //poolNv = nv;
1047 d_nm->poolInsert(nv);
1048 if(Debug.isOn("gc")) {
1049 Debug("gc") << "creating node value " << nv
1050 << " [" << nv->d_id << "]: ";
1051 nv->printAst(Debug("gc"));
1052 Debug("gc") << std::endl;
1053 }
1054 return nv;
1055 }
1056 } else {
1057 /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger
1058 ** buffer that was heap-allocated by this NodeBuilder. **/
1059
1060 // Lookup the expression value in the pool we already have (with insert)
1061 expr::NodeValue* poolNv = d_nm->poolLookup(d_nv);
1062 // If something else is there, we reuse it
1063 if(poolNv != NULL) {
1064 /* Subcase (a): The Node under construction already exists in
1065 * the NodeManager's pool. */
1066
1067 /* 2(a). Reference-counts for all children in d_nv must be
1068 * decremented. The NodeBuilder is marked as "used" and the
1069 * heap-allocated d_nv deleted. d_nv is repointed to d_inlineNv
1070 * so that destruction of the NodeBuilder doesn't cause any
1071 * problems. The existing NodeManager pool entry is
1072 * returned. */
1073
1074 dealloc();
1075 setUsed();
1076 return poolNv;
1077 } else {
1078 /* Subcase (b) The Node under construction is NOT already in the
1079 * NodeManager's pool. */
1080
1081 /* 2(b). The heap-allocated d_nv is "cropped" to the correct
1082 * size (based on the number of children it _actually_ has).
1083 * d_nv is repointed to d_inlineNv so that destruction of the
1084 * NodeBuilder doesn't cause any problems, and the (old) value
1085 * it had is placed into the NodeManager's pool and returned in
1086 * a Node wrapper. */
1087
1088 crop();
1089 expr::NodeValue* nv = d_nv;
1090 nv->d_id = d_nm->next_id++;// FIXME multithreading
1091 d_nv = &d_inlineNv;
1092 d_nvMaxChildren = nchild_thresh;
1093 setUsed();
1094
1095 //poolNv = nv;
1096 d_nm->poolInsert(nv);
1097 Debug("gc") << "creating node value " << nv
1098 << " [" << nv->d_id << "]: " << *nv << "\n";
1099 return nv;
1100 }
1101 }
1102 }
1103
1104 // CONST VERSION OF NODE EXTRACTOR
1105 template <unsigned nchild_thresh>
constructNV()1106 expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
1107 Assert(!isUsed(), "NodeBuilder is one-shot only; "
1108 "attempt to access it after conversion");
1109 Assert(getKind() != kind::UNDEFINED_KIND,
1110 "Can't make an expression of an undefined kind!");
1111
1112 // NOTE: The comments in this function refer to the cases in the
1113 // file comments at the top of this file.
1114
1115 // Case 0: If a VARIABLE
1116 if(getMetaKind() == kind::metakind::VARIABLE || getMetaKind() == kind::metakind::NULLARY_OPERATOR) {
1117 /* 0. If a VARIABLE, treat similarly to 1(b), except that we know
1118 * there are no children (no reference counts to reason about),
1119 * and we don't keep VARIABLE-kinded Nodes in the NodeManager
1120 * pool. */
1121
1122 Assert( ! nvIsAllocated(),
1123 "internal NodeBuilder error: "
1124 "VARIABLE-kinded NodeBuilder is heap-allocated !?" );
1125 Assert( d_inlineNv.d_nchildren == 0,
1126 "improperly-formed VARIABLE-kinded NodeBuilder: "
1127 "no children permitted" );
1128
1129 // we have to copy the inline NodeValue out
1130 expr::NodeValue* nv = (expr::NodeValue*)
1131 std::malloc(sizeof(expr::NodeValue));
1132 if(nv == NULL) {
1133 throw std::bad_alloc();
1134 }
1135 // there are no children, so we don't have to worry about
1136 // reference counts in this case.
1137 nv->d_nchildren = 0;
1138 nv->d_kind = d_nv->d_kind;
1139 nv->d_id = d_nm->next_id++;// FIXME multithreading
1140 nv->d_rc = 0;
1141 Debug("gc") << "creating node value " << nv
1142 << " [" << nv->d_id << "]: " << *nv << "\n";
1143 return nv;
1144 }
1145
1146 // check that there are the right # of children for this kind
1147 Assert(getMetaKind() != kind::metakind::CONSTANT,
1148 "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds");
1149 Assert(getNumChildren() >= kind::metakind::getLowerBoundForKind(getKind()),
1150 "Nodes with kind %s must have at least %u children (the one under "
1151 "construction has %u)",
1152 kind::kindToString(getKind()).c_str(),
1153 kind::metakind::getLowerBoundForKind(getKind()),
1154 getNumChildren());
1155 Assert(getNumChildren() <= kind::metakind::getUpperBoundForKind(getKind()),
1156 "Nodes with kind %s must have at most %u children (the one under "
1157 "construction has %u)",
1158 kind::kindToString(getKind()).c_str(),
1159 kind::metakind::getUpperBoundForKind(getKind()),
1160 getNumChildren());
1161
1162 #if 0
1163 // if the kind is PARAMETERIZED, check that the operator is correctly-kinded
1164 Assert(kind::metaKindOf(getKind()) != kind::metakind::PARAMETERIZED ||
1165 NodeManager::operatorToKind(getOperator()) == getKind(),
1166 "Attempted to construct a parameterized kind `%s' with "
1167 "incorrectly-kinded operator `%s'",
1168 kind::kindToString(getKind()).c_str(),
1169 kind::kindToString(getOperator().getKind()).c_str());
1170 #endif /* 0 */
1171
1172 // Implementation differs depending on whether the NodeValue was
1173 // malloc'ed or not and whether or not it's in the already-been-seen
1174 // NodeManager pool of Nodes. See implementation notes at the top
1175 // of this file.
1176
1177 if(__builtin_expect( ( ! nvIsAllocated() ), true )) {
1178 /** Case 1. d_nv points to d_inlineNv: it is the backing store
1179 ** allocated "inline" in this NodeBuilder. **/
1180
1181 // Lookup the expression value in the pool we already have
1182 expr::NodeValue* poolNv = d_nm->poolLookup(const_cast<expr::NodeValue*>(&d_inlineNv));
1183 // If something else is there, we reuse it
1184 if(poolNv != NULL) {
1185 /* Subcase (a): The Node under construction already exists in
1186 * the NodeManager's pool. */
1187
1188 /* 1(a). The existing NodeManager pool entry is returned; we
1189 * leave child reference counts alone and get them at
1190 * NodeBuilder destruction time. */
1191
1192 return poolNv;
1193 } else {
1194 /* Subcase (b): The Node under construction is NOT already in
1195 * the NodeManager's pool. */
1196
1197 /* 1(b). A new heap-allocated NodeValue must be constructed and
1198 * all settings and children from d_inlineNv copied into it.
1199 * This new NodeValue is put into the NodeManager's pool. The
1200 * NodeBuilder cannot be marked as "used", so we increment all
1201 * child reference counts (which will be decremented to match on
1202 * destruction of the NodeBuilder). We return a Node wrapper
1203 * for this new NodeValue, which increments its reference
1204 * count. */
1205
1206 // create the canonical expression value for this node
1207 expr::NodeValue* nv = (expr::NodeValue*)
1208 std::malloc(sizeof(expr::NodeValue) +
1209 ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));
1210 if(nv == NULL) {
1211 throw std::bad_alloc();
1212 }
1213 nv->d_nchildren = d_inlineNv.d_nchildren;
1214 nv->d_kind = d_inlineNv.d_kind;
1215 nv->d_id = d_nm->next_id++;// FIXME multithreading
1216 nv->d_rc = 0;
1217
1218 std::copy(d_inlineNv.d_children,
1219 d_inlineNv.d_children + d_inlineNv.d_nchildren,
1220 nv->d_children);
1221
1222 for(expr::NodeValue::nv_iterator i = nv->nv_begin();
1223 i != nv->nv_end();
1224 ++i) {
1225 (*i)->inc();
1226 }
1227
1228 //poolNv = nv;
1229 d_nm->poolInsert(nv);
1230 Debug("gc") << "creating node value " << nv
1231 << " [" << nv->d_id << "]: " << *nv << "\n";
1232 return nv;
1233 }
1234 } else {
1235 /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger
1236 ** buffer that was heap-allocated by this NodeBuilder. **/
1237
1238 // Lookup the expression value in the pool we already have (with insert)
1239 expr::NodeValue* poolNv = d_nm->poolLookup(d_nv);
1240 // If something else is there, we reuse it
1241 if(poolNv != NULL) {
1242 /* Subcase (a): The Node under construction already exists in
1243 * the NodeManager's pool. */
1244
1245 /* 2(a). The existing NodeManager pool entry is returned; we
1246 * leave child reference counts alone and get them at
1247 * NodeBuilder destruction time. */
1248
1249 return poolNv;
1250 } else {
1251 /* Subcase (b) The Node under construction is NOT already in the
1252 * NodeManager's pool. */
1253
1254 /* 2(b). The heap-allocated d_nv cannot be "cropped" to the
1255 * correct size; we create a copy, increment child reference
1256 * counts, place this copy into the NodeManager pool, and return
1257 * a Node wrapper around it. The child reference counts will be
1258 * decremented to match at NodeBuilder destruction time. */
1259
1260 // create the canonical expression value for this node
1261 expr::NodeValue* nv = (expr::NodeValue*)
1262 std::malloc(sizeof(expr::NodeValue) +
1263 ( sizeof(expr::NodeValue*) * d_nv->d_nchildren ));
1264 if(nv == NULL) {
1265 throw std::bad_alloc();
1266 }
1267 nv->d_nchildren = d_nv->d_nchildren;
1268 nv->d_kind = d_nv->d_kind;
1269 nv->d_id = d_nm->next_id++;// FIXME multithreading
1270 nv->d_rc = 0;
1271
1272 std::copy(d_nv->d_children,
1273 d_nv->d_children + d_nv->d_nchildren,
1274 nv->d_children);
1275
1276 for(expr::NodeValue::nv_iterator i = nv->nv_begin();
1277 i != nv->nv_end();
1278 ++i) {
1279 (*i)->inc();
1280 }
1281
1282 //poolNv = nv;
1283 d_nm->poolInsert(nv);
1284 Debug("gc") << "creating node value " << nv
1285 << " [" << nv->d_id << "]: " << *nv << "\n";
1286 return nv;
1287 }
1288 }
1289 }
1290
1291 template <unsigned nchild_thresh>
1292 template <unsigned N>
internalCopy(const NodeBuilder<N> & nb)1293 void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) {
1294 if(nb.isUsed()) {
1295 setUsed();
1296 return;
1297 }
1298
1299 bool realloced CVC4_UNUSED = false;
1300 if(nb.d_nvMaxChildren > d_nvMaxChildren) {
1301 realloced = true;
1302 realloc(nb.d_nvMaxChildren);
1303 }
1304
1305 Assert(nb.d_nvMaxChildren <= d_nvMaxChildren);
1306 Assert(nb.d_nv->nv_end() >= nb.d_nv->nv_begin());
1307 Assert((size_t)(nb.d_nv->nv_end() - nb.d_nv->nv_begin()) <= d_nvMaxChildren, "realloced:%s, d_nvMax:%u, size:%u, nc:%u", realloced ? "true" : "false", d_nvMaxChildren, nb.d_nv->nv_end() - nb.d_nv->nv_begin(), nb.d_nv->getNumChildren());
1308 std::copy(nb.d_nv->nv_begin(),
1309 nb.d_nv->nv_end(),
1310 d_nv->nv_begin());
1311
1312 d_nv->d_nchildren = nb.d_nv->d_nchildren;
1313
1314 for(expr::NodeValue::nv_iterator i = d_nv->nv_begin();
1315 i != d_nv->nv_end();
1316 ++i) {
1317 (*i)->inc();
1318 }
1319 }
1320
1321 #ifdef CVC4_DEBUG
1322 template <unsigned nchild_thresh>
maybeCheckType(const TNode n)1323 inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const
1324 {
1325 /* force an immediate type check, if early type checking is
1326 enabled and the current node isn't a variable or constant */
1327 if( d_nm->getOptions()[options::earlyTypeChecking] ) {
1328 kind::MetaKind mk = n.getMetaKind();
1329 if( mk != kind::metakind::VARIABLE
1330 && mk != kind::metakind::NULLARY_OPERATOR
1331 && mk != kind::metakind::CONSTANT ) {
1332 d_nm->getType(n, true);
1333 }
1334 }
1335 }
1336 #endif /* CVC4_DEBUG */
1337
1338 template <unsigned nchild_thresh>
1339 std::ostream& operator<<(std::ostream& out, const NodeBuilder<nchild_thresh>& nb) {
1340 return out << *nb.d_nv;
1341 }
1342
1343 }/* CVC4 namespace */
1344
1345 #endif /* __CVC4__NODE_BUILDER_H */
1346