GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/node_builder.h Lines: 307 368 83.4 %
Date: 2021-03-22 Branches: 761 6309 12.1 %

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