GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/node_value.h Lines: 105 136 77.2 %
Date: 2021-03-23 Branches: 43 171 25.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file node_value.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Aina Niemetz, 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 An expression node.
13
 **
14
 ** An expression node.
15
 **
16
 ** Instances of this class are generally referenced through
17
 ** cvc4::Node rather than by pointer; cvc4::Node maintains the
18
 ** reference count on NodeValue instances and
19
 **/
20
21
#include "cvc4_private.h"
22
23
// circular dependency
24
#include "expr/metakind.h"
25
26
#ifndef CVC4__EXPR__NODE_VALUE_H
27
#define CVC4__EXPR__NODE_VALUE_H
28
29
#include <iterator>
30
#include <string>
31
32
#include "expr/kind.h"
33
#include "options/language.h"
34
35
namespace CVC4 {
36
37
template <bool ref_count> class NodeTemplate;
38
class TypeNode;
39
template <unsigned N> class NodeBuilder;
40
class NodeManager;
41
42
namespace expr {
43
  class NodeValue;
44
}
45
46
namespace kind {
47
  namespace metakind {
48
    template < ::CVC4::Kind k, bool pool >
49
    struct NodeValueConstCompare;
50
51
    struct NodeValueCompare;
52
    struct NodeValueConstPrinter;
53
54
    void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv);
55
  }/* CVC4::kind::metakind namespace */
56
}/* CVC4::kind namespace */
57
58
namespace expr {
59
60
/**
61
 * This is a NodeValue.
62
 */
63
class NodeValue
64
{
65
  template <bool>
66
  friend class ::CVC4::NodeTemplate;
67
  friend class ::CVC4::TypeNode;
68
  template <unsigned nchild_thresh>
69
  friend class ::CVC4::NodeBuilder;
70
  friend class ::CVC4::NodeManager;
71
72
  template <Kind k, bool pool>
73
  friend struct ::CVC4::kind::metakind::NodeValueConstCompare;
74
75
  friend struct ::CVC4::kind::metakind::NodeValueCompare;
76
  friend struct ::CVC4::kind::metakind::NodeValueConstPrinter;
77
78
  friend void ::CVC4::kind::metakind::deleteNodeValueConstant(NodeValue* nv);
79
80
  friend class RefCountGuard;
81
82
  /* ------------------------------------------------------------------------ */
83
 public:
84
  /* ------------------------------------------------------------------------ */
85
86
  using nv_iterator = NodeValue**;
87
  using const_nv_iterator = NodeValue const* const*;
88
89
  template <class T>
90
  class iterator
91
  {
92
   public:
93
    using iterator_category = std::random_access_iterator_tag;
94
    using value_type = T;
95
    using difference_type = std::ptrdiff_t;
96
    using pointer = T*;
97
    using reference = T&;
98
99
255267763
    iterator() : d_i(NULL) {}
100
1171670458
    explicit iterator(const_nv_iterator i) : d_i(i) {}
101
102
    /** Conversion of a TNode iterator to a Node iterator. */
103
255064935
    inline operator NodeValue::iterator<NodeTemplate<true> >()
104
    {
105
255064935
      return iterator<NodeTemplate<true> >(d_i);
106
    }
107
108
    inline T operator*() const;
109
110
505217638
    bool operator==(const iterator& i) const { return d_i == i.d_i; }
111
112
576878959
    bool operator!=(const iterator& i) const { return d_i != i.d_i; }
113
114
523690258
    iterator& operator++()
115
    {
116
523690258
      ++d_i;
117
523690258
      return *this;
118
    }
119
120
15246
    iterator operator++(int) { return iterator(d_i++); }
121
122
    iterator& operator--()
123
    {
124
      --d_i;
125
      return *this;
126
    }
127
128
    iterator operator--(int) { return iterator(d_i--); }
129
130
7060082
    iterator& operator+=(difference_type p)
131
    {
132
7060082
      d_i += p;
133
7060082
      return *this;
134
    }
135
136
    iterator& operator-=(difference_type p)
137
    {
138
      d_i -= p;
139
      return *this;
140
    }
141
142
1034548
    iterator operator+(difference_type p) { return iterator(d_i + p); }
143
144
610
    iterator operator-(difference_type p) { return iterator(d_i - p); }
145
146
26932543
    difference_type operator-(iterator i) { return d_i - i.d_i; }
147
148
   private:
149
    const_nv_iterator d_i;
150
151
  }; /* class NodeValue::iterator<T> */
152
153
7363637604
  uint64_t getId() const { return d_id; }
154
155
8133037824
  Kind getKind() const { return dKindToKind(d_kind); }
156
157
4735516423
  kind::MetaKind getMetaKind() const { return kind::metaKindOf(getKind()); }
158
159
1273855390
  uint32_t getNumChildren() const
160
  {
161
2446169356
    return (getMetaKind() == kind::metakind::PARAMETERIZED) ? d_nchildren - 1
162
2446169356
                                                            : d_nchildren;
163
  }
164
165
  /* ------------------------------ Header ---------------------------------- */
166
  /** Number of bits reserved for reference counting. */
167
  static constexpr uint32_t NBITS_REFCOUNT = 20;
168
  /** Number of bits reserved for node kind. */
169
  static constexpr uint32_t NBITS_KIND = 10;
170
  /** Number of bits reserved for node id. */
171
  static constexpr uint32_t NBITS_ID = 40;
172
  /** Number of bits reserved for number of children. */
173
  static const uint32_t NBITS_NCHILDREN = 26;
174
  static_assert(NBITS_REFCOUNT + NBITS_KIND + NBITS_ID + NBITS_NCHILDREN == 96,
175
                "NodeValue header bit assignment does not sum to 96 !");
176
  /* ------------------- This header fits into 96 bits ---------------------- */
177
178
  /** Maximum number of children possible. */
179
  static constexpr uint32_t MAX_CHILDREN =
180
      (static_cast<uint32_t>(1) << NBITS_NCHILDREN) - 1;
181
182
  uint32_t getRefCount() const { return d_rc; }
183
184
  NodeValue* getOperator() const;
185
  NodeValue* getChild(int i) const;
186
187
  /** If this is a CONST_* Node, extract the constant from it.  */
188
  template <class T>
189
  inline const T& getConst() const;
190
191
5488802483
  static inline NodeValue& null()
192
  {
193
5488802483
    static NodeValue* s_null = new NodeValue(0);
194
5488802483
    return *s_null;
195
  }
196
197
  /**
198
   * Hash this NodeValue.  For hash_maps, hash_sets, etc.. but this is
199
   * for expr package internal use only at present!  This is likely to
200
   * be POORLY PERFORMING for other uses!  For example, this gives
201
   * collisions for all VARIABLEs.
202
   * @return the hash value of this expression.
203
   */
204
586512085
  size_t poolHash() const
205
  {
206
586512085
    if (getMetaKind() == kind::metakind::CONSTANT)
207
    {
208
225285309
      return kind::metakind::NodeValueCompare::constHash(this);
209
    }
210
211
361226776
    size_t hash = d_kind;
212
361226776
    const_nv_iterator i = nv_begin();
213
361226776
    const_nv_iterator i_end = nv_end();
214
2053617810
    while (i != i_end)
215
    {
216
846195517
      hash ^= (*i)->d_id + 0x9e3779b9 + (hash << 6) + (hash >> 2);
217
846195517
      ++i;
218
    }
219
361226776
    return hash;
220
  }
221
222
300437301
  static inline uint32_t kindToDKind(Kind k)
223
  {
224
300437301
    return ((uint32_t)k) & kindMask;
225
  }
226
227
8133037824
  static inline Kind dKindToKind(uint32_t d)
228
  {
229
8133037824
    return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d);
230
  }
231
232
  std::string toString() const;
233
234
  void toStream(std::ostream& out,
235
                int toDepth = -1,
236
                size_t dag = 1,
237
                OutputLanguage = language::output::LANG_AUTO) const;
238
239
  void printAst(std::ostream& out, int indent = 0) const;
240
241
  template <typename T>
242
  inline iterator<T> begin() const;
243
  template <typename T>
244
  inline iterator<T> end() const;
245
246
  /* ------------------------------------------------------------------------ */
247
 private:
248
  /* ------------------------------------------------------------------------ */
249
250
  /**
251
   * RAII guard that increases the reference count if the reference count to be
252
   * > 0.  Otherwise, this does nothing. This does not just increment the
253
   * reference count to avoid maxing out the d_rc field. This is only for low
254
   * level functions.
255
   */
256
  class RefCountGuard
257
  {
258
   public:
259
662839
    RefCountGuard(const NodeValue* nv) : d_nv(const_cast<NodeValue*>(nv))
260
    {
261
662839
      d_increased = (d_nv->d_rc == 0);
262
662839
      if (d_increased)
263
      {
264
        d_nv->d_rc = 1;
265
      }
266
662839
    }
267
662839
    ~RefCountGuard()
268
662839
    {
269
      // dec() without marking for deletion: we don't want to garbage
270
      // collect this NodeValue if ours is the last reference to it.
271
      // E.g., this can happen when debugging code calls the print
272
      // routines below.  As RefCountGuards are scoped on the stack,
273
      // this should be fine---but not in multithreaded contexts!
274
662839
      if (d_increased)
275
      {
276
        --d_nv->d_rc;
277
      }
278
662839
    }
279
280
   private:
281
    NodeValue* d_nv;
282
    bool d_increased;
283
  }; /* NodeValue::RefCountGuard */
284
285
  /** Maximum reference count possible.  Used for sticky
286
   *  reference-counting.  Should be (1 << num_bits(d_rc)) - 1 */
287
  static constexpr uint32_t MAX_RC =
288
      (static_cast<uint32_t>(1) << NBITS_REFCOUNT) - 1;
289
290
  /** A mask for d_kind */
291
  static constexpr uint32_t kindMask =
292
      (static_cast<uint32_t>(1) << NBITS_KIND) - 1;
293
294
  /** Uninitializing constructor for NodeBuilder's use.  */
295
551204455
  NodeValue()
296
551204455
  { /* do not initialize! */
297
551204455
  }
298
  /** Private constructor for the null value. */
299
  NodeValue(int);
300
301
  void inc();
302
  void dec();
303
304
  /** Decrement ref counts of children */
305
  inline void decrRefCounts();
306
307
  bool isBeingDeleted() const;
308
309
  /** Returns true if the reference count is maximized. */
310
14
  inline bool HasMaximizedReferenceCount() { return d_rc == MAX_RC; }
311
312
  nv_iterator nv_begin();
313
  nv_iterator nv_end();
314
315
  const_nv_iterator nv_begin() const;
316
  const_nv_iterator nv_end() const;
317
318
  /**
319
   * Indents the given stream a given amount of spaces.
320
   * @param out the stream to indent
321
   * @param indent the numer of spaces
322
   */
323
  static inline void indent(std::ostream& out, int indent)
324
  {
325
    for (int i = 0; i < indent; i++)
326
    {
327
      out << ' ';
328
    }
329
  }
330
331
  /** The ID (0 is reserved for the null value) */
332
  uint64_t d_id : NBITS_ID;
333
334
  /** The expression's reference count.  @see cvc4::Node. */
335
  uint32_t d_rc : NBITS_REFCOUNT;
336
337
  /** Kind of the expression */
338
  uint32_t d_kind : NBITS_KIND;
339
340
  /** Number of children */
341
  uint32_t d_nchildren : NBITS_NCHILDREN;
342
343
  /** Variable number of child nodes */
344
  NodeValue* d_children[0];
345
}; /* class NodeValue */
346
347
/**
348
 * Provides a symmetric addition operator to that already defined in
349
 * the iterator class.
350
 */
351
NodeValue::iterator<NodeTemplate<true> > operator+(
352
    NodeValue::iterator<NodeTemplate<true> >::difference_type p,
353
    NodeValue::iterator<NodeTemplate<true> > i);
354
355
/**
356
 * Provides a symmetric addition operator to that already defined in
357
 * the iterator class.
358
 */
359
NodeValue::iterator<NodeTemplate<false> > operator+(
360
    NodeValue::iterator<NodeTemplate<false> >::difference_type p,
361
    NodeValue::iterator<NodeTemplate<false> > i);
362
363
/**
364
 * For hash_maps, hash_sets, etc.. but this is for expr package
365
 * internal use only at present!  This is likely to be POORLY
366
 * PERFORMING for other uses!  NodeValue::poolHash() will lead to
367
 * collisions for all VARIABLEs.
368
 */
369
struct NodeValuePoolHashFunction {
370
586512085
  inline size_t operator()(const NodeValue* nv) const {
371
586512085
    return (size_t) nv->poolHash();
372
  }
373
};/* struct NodeValuePoolHashFunction */
374
375
/**
376
 * For hash_maps, hash_sets, etc.
377
 */
378
struct NodeValueIDHashFunction {
379
112427383
  inline size_t operator()(const NodeValue* nv) const {
380
112427383
    return (size_t) nv->getId();
381
  }
382
};/* struct NodeValueIDHashFunction */
383
384
385
/**
386
 * An equality predicate that is applicable between pointers to fully
387
 * constructed NodeValues.
388
 */
389
struct NodeValueIDEquality {
390
52244755
  inline bool operator()(const NodeValue* a, const NodeValue* b) const {
391
52244755
    return a->getId() == b->getId();
392
  }
393
};
394
395
396
inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv);
397
398
}/* CVC4::expr namespace */
399
}/* CVC4 namespace */
400
401
#include "expr/node_manager.h"
402
403
namespace CVC4 {
404
namespace expr {
405
406
8895
inline NodeValue::NodeValue(int) :
407
  d_id(0),
408
  d_rc(MAX_RC),
409
  d_kind(kind::NULL_EXPR),
410
8895
  d_nchildren(0) {
411
8895
}
412
413
29459522
inline void NodeValue::decrRefCounts() {
414
110336405
  for(nv_iterator i = nv_begin(); i != nv_end(); ++i) {
415
80876883
    (*i)->dec();
416
  }
417
29459522
}
418
419
16199690826
inline void NodeValue::inc() {
420
16199690826
  Assert(!isBeingDeleted())
421
      << "NodeValue is currently being deleted "
422
         "and increment is being called on it. Don't Do That!";
423
  // FIXME multithreading
424
16199690826
  if (__builtin_expect((d_rc < MAX_RC - 1), true)) {
425
12273089394
    ++d_rc;
426
3926601432
  } else if (__builtin_expect((d_rc == MAX_RC - 1), false)) {
427
7
    ++d_rc;
428
7
    Assert(NodeManager::currentNM() != NULL)
429
        << "No current NodeManager on incrementing of NodeValue: "
430
           "maybe a public CVC4 interface function is missing a "
431
           "NodeManagerScope ?";
432
7
    NodeManager::currentNM()->markRefCountMaxedOut(this);
433
  }
434
16199690826
}
435
436
17787523271
inline void NodeValue::dec() {
437
  // FIXME multithreading
438
17787523271
  if(__builtin_expect( ( d_rc < MAX_RC ), true )) {
439
12265739834
    --d_rc;
440
12265739834
    if(__builtin_expect( ( d_rc == 0 ), false )) {
441
47506180
      Assert(NodeManager::currentNM() != NULL)
442
          << "No current NodeManager on destruction of NodeValue: "
443
             "maybe a public CVC4 interface function is missing a "
444
             "NodeManagerScope ?";
445
47506180
      NodeManager::currentNM()->markForDeletion(this);
446
    }
447
  }
448
17787523271
}
449
450
569658385
inline NodeValue::nv_iterator NodeValue::nv_begin() {
451
569658385
  return d_children;
452
}
453
454
1053135645
inline NodeValue::nv_iterator NodeValue::nv_end() {
455
1053135645
  return d_children + d_nchildren;
456
}
457
458
931588500
inline NodeValue::const_nv_iterator NodeValue::nv_begin() const {
459
931588500
  return d_children;
460
}
461
462
646407638
inline NodeValue::const_nv_iterator NodeValue::nv_end() const {
463
646407638
  return d_children + d_nchildren;
464
}
465
466
template <typename T>
467
225461310
inline NodeValue::iterator<T> NodeValue::begin() const {
468
225461310
  NodeValue* const* firstChild = d_children;
469
225461310
  if(getMetaKind() == kind::metakind::PARAMETERIZED) {
470
17541153
    ++firstChild;
471
  }
472
225461310
  return iterator<T>(firstChild);
473
}
474
475
template <typename T>
476
690093809
inline NodeValue::iterator<T> NodeValue::end() const {
477
690093809
  return iterator<T>(d_children + d_nchildren);
478
}
479
480
16199690826
inline bool NodeValue::isBeingDeleted() const {
481
32399363862
  return NodeManager::currentNM() != NULL &&
482
32399363862
    NodeManager::currentNM()->isCurrentlyDeleting(this);
483
}
484
485
inline NodeValue* NodeValue::getOperator() const {
486
  Assert(getMetaKind() == kind::metakind::PARAMETERIZED);
487
  return d_children[0];
488
}
489
490
1093000083
inline NodeValue* NodeValue::getChild(int i) const {
491
1093000083
  if(getMetaKind() == kind::metakind::PARAMETERIZED) {
492
57187455
    ++i;
493
  }
494
495
1093000083
  Assert(i >= 0 && unsigned(i) < d_nchildren);
496
1093000083
  return d_children[i];
497
}
498
499
}/* CVC4::expr namespace */
500
}/* CVC4 namespace */
501
502
#include "expr/node.h"
503
504
namespace CVC4 {
505
namespace expr {
506
507
template <typename T>
508
703004874
inline T NodeValue::iterator<T>::operator*() const {
509
703004874
  return T(*d_i);
510
}
511
512
inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) {
513
  nv.toStream(out,
514
              Node::setdepth::getDepth(out),
515
              Node::dag::getDag(out),
516
              Node::setlanguage::getLanguage(out));
517
  return out;
518
}
519
520
}/* CVC4::expr namespace */
521
522
#ifdef CVC4_DEBUG
523
/**
524
 * Pretty printer for use within gdb.  This is not intended to be used
525
 * outside of gdb.  This writes to the Warning() stream and immediately
526
 * flushes the stream.
527
 */
528
static void __attribute__((used)) debugPrintNodeValue(const expr::NodeValue* nv) {
529
  Warning() << Node::setdepth(-1)
530
            << Node::dag(true)
531
            << Node::setlanguage(language::output::LANG_AST)
532
            << *nv << std::endl;
533
  Warning().flush();
534
}
535
static void __attribute__((used)) debugPrintNodeValueNoDag(const expr::NodeValue* nv) {
536
  Warning() << Node::setdepth(-1)
537
            << Node::dag(false)
538
            << Node::setlanguage(language::output::LANG_AST)
539
            << *nv << std::endl;
540
  Warning().flush();
541
}
542
static void __attribute__((used)) debugPrintRawNodeValue(const expr::NodeValue* nv) {
543
  nv->printAst(Warning(), 0);
544
  Warning().flush();
545
}
546
#endif /* CVC4_DEBUG */
547
548
}/* CVC4 namespace */
549
550
#endif /* CVC4__EXPR__NODE_VALUE_H */