diff options
Diffstat (limited to 'src/expr/node_value.h')
-rw-r--r-- | src/expr/node_value.h | 55 |
1 files changed, 54 insertions, 1 deletions
diff --git a/src/expr/node_value.h b/src/expr/node_value.h index f0220d37a..85b8a6d60 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -191,10 +191,63 @@ public: return ((unsigned) k) & kindMask; } static inline Kind dKindToKind(unsigned d) { - return (d == kindMask) ? UNDEFINED_KIND : Kind(d); + return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d); } }; +inline NodeValue::NodeValue() : + d_id(0), + d_rc(MAX_RC), + d_kind(kind::NULL_EXPR), + d_nchildren(0) { +} + +inline NodeValue::NodeValue(int) : + d_id(0), + d_rc(0), + d_kind(kindToDKind(kind::UNDEFINED_KIND)), + d_nchildren(0) { +} + +inline NodeValue::~NodeValue() { + for(nv_iterator i = nv_begin(); i != nv_end(); ++i) { + (*i)->dec(); + } +} + +inline void NodeValue::inc() { + // FIXME multithreading + if(EXPECT_TRUE( d_rc < MAX_RC )) { + ++d_rc; + } +} + +inline void NodeValue::dec() { + // FIXME multithreading + if(EXPECT_TRUE( d_rc < MAX_RC )) { + --d_rc; + if(EXPECT_FALSE( d_rc == 0 )) { + // FIXME gc + } + } +} + +inline NodeValue::nv_iterator NodeValue::nv_begin() { + return d_children; +} + +inline NodeValue::nv_iterator NodeValue::nv_end() { + return d_children + d_nchildren; +} + +inline NodeValue::const_nv_iterator NodeValue::nv_begin() const { + return d_children; +} + +inline NodeValue::const_nv_iterator NodeValue::nv_end() const { + return d_children + d_nchildren; +} + }/* CVC4::expr namespace */ }/* CVC4 namespace */ |