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