/**
* This is a NodeValue.
*/
-class NodeValue {
- static const uint32_t NBITS_REFCOUNT =
- CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT;
- static const uint32_t NBITS_KIND = CVC4__EXPR__NODE_VALUE__NBITS__KIND;
- static const uint32_t NBITS_ID = CVC4__EXPR__NODE_VALUE__NBITS__ID;
- static const uint32_t NBITS_NCHILDREN =
- CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN;
-
- /** Maximum reference count possible. Used for sticky
- * reference-counting. Should be (1 << num_bits(d_rc)) - 1 */
- static const uint32_t MAX_RC = (((uint32_t)1) << NBITS_REFCOUNT) - 1;
-
- /** A mask for d_kind */
- static const uint32_t kindMask = (((uint32_t)1) << NBITS_KIND) - 1;
-
- // This header fits into 96 bits
-
- /** The ID (0 is reserved for the null value) */
- uint64_t d_id : NBITS_ID;
-
- /** The expression's reference count. @see cvc4::Node. */
- uint32_t d_rc : NBITS_REFCOUNT;
-
- /** Kind of the expression */
- uint32_t d_kind : NBITS_KIND;
-
- /** Number of children */
- uint32_t d_nchildren : NBITS_NCHILDREN;
-
- /** Variable number of child nodes */
- NodeValue* d_children[0];
-
- // todo add exprMgr ref in debug case
-
- template <bool> friend class ::CVC4::NodeTemplate;
+class NodeValue
+{
+ template <bool>
+ friend class ::CVC4::NodeTemplate;
friend class ::CVC4::TypeNode;
- template <unsigned nchild_thresh> friend class ::CVC4::NodeBuilder;
+ template <unsigned nchild_thresh>
+ friend class ::CVC4::NodeBuilder;
friend class ::CVC4::NodeManager;
template <Kind k, bool pool>
friend void ::CVC4::kind::metakind::deleteNodeValueConstant(NodeValue* nv);
- void inc();
- void dec();
-
- // Returns true if the reference count is maximized.
- inline bool HasMaximizedReferenceCount() { return d_rc == MAX_RC; }
+ friend class RefCountGuard;
- /**
- * Uninitializing constructor for NodeBuilder's use.
- */
- NodeValue() { /* do not initialize! */ }
-
-private:
- /** Private constructor for the null value. */
- NodeValue(int);
+ /* ------------------------------------------------------------------------ */
+ public:
+ /* ------------------------------------------------------------------------ */
typedef NodeValue** nv_iterator;
typedef NodeValue const* const* const_nv_iterator;
- nv_iterator nv_begin();
- nv_iterator nv_end();
-
- const_nv_iterator nv_begin() const;
- const_nv_iterator nv_end() const;
-
template <class T>
- class iterator {
- const_nv_iterator d_i;
- public:
+ class iterator
+ {
+ public:
typedef std::random_access_iterator_tag iterator_category;
typedef T value_type;
typedef std::ptrdiff_t difference_type;
iterator() : d_i(NULL) {}
explicit iterator(const_nv_iterator i) : d_i(i) {}
- // conversion of a TNode iterator to a Node iterator
- inline operator NodeValue::iterator<NodeTemplate<true> >() {
+ /** Conversion of a TNode iterator to a Node iterator. */
+ inline operator NodeValue::iterator<NodeTemplate<true> >()
+ {
return iterator<NodeTemplate<true> >(d_i);
}
inline T operator*() const;
- bool operator==(const iterator& i) const {
- return d_i == i.d_i;
- }
+ bool operator==(const iterator& i) const { return d_i == i.d_i; }
- bool operator!=(const iterator& i) const {
- return d_i != i.d_i;
- }
+ bool operator!=(const iterator& i) const { return d_i != i.d_i; }
- iterator& operator++() {
+ iterator& operator++()
+ {
++d_i;
return *this;
}
- iterator operator++(int) {
- return iterator(d_i++);
- }
+ iterator operator++(int) { return iterator(d_i++); }
- iterator& operator--() {
+ iterator& operator--()
+ {
--d_i;
return *this;
}
- iterator operator--(int) {
- return iterator(d_i--);
- }
+ iterator operator--(int) { return iterator(d_i--); }
- iterator& operator+=(difference_type p) {
+ iterator& operator+=(difference_type p)
+ {
d_i += p;
return *this;
}
- iterator& operator-=(difference_type p) {
+ iterator& operator-=(difference_type p)
+ {
d_i -= p;
return *this;
}
- iterator operator+(difference_type p) {
- return iterator(d_i + p);
- }
+ iterator operator+(difference_type p) { return iterator(d_i + p); }
- iterator operator-(difference_type p) {
- return iterator(d_i - p);
- }
+ iterator operator-(difference_type p) { return iterator(d_i - p); }
- difference_type operator-(iterator i) {
- return d_i - i.d_i;
- }
- };/* class NodeValue::iterator<T> */
+ difference_type operator-(iterator i) { return d_i - i.d_i; }
- // operator+ (as a function) cannot be a template, so we have to
- // define two versions
- friend NodeValue::iterator<NodeTemplate<true> >
- operator+(NodeValue::iterator<NodeTemplate<true> >::difference_type p,
- NodeValue::iterator<NodeTemplate<true> > i);
- friend NodeValue::iterator<NodeTemplate<false> >
- operator+(NodeValue::iterator<NodeTemplate<false> >::difference_type p,
- NodeValue::iterator<NodeTemplate<false> > i);
+ private:
+ const_nv_iterator d_i;
- /** Decrement ref counts of children */
- inline void decrRefCounts();
+ }; /* class NodeValue::iterator<T> */
- bool isBeingDeleted() const;
+ uint64_t getId() const { return d_id; }
-public:
+ Kind getKind() const { return dKindToKind(d_kind); }
- template <typename T>
- inline iterator<T> begin() const;
+ kind::MetaKind getMetaKind() const { return kind::metaKindOf(getKind()); }
- template <typename T>
- inline iterator<T> end() const;
+ uint32_t getNumChildren() const
+ {
+ return (getMetaKind() == kind::metakind::PARAMETERIZED) ? d_nchildren - 1
+ : d_nchildren;
+ }
+
+ unsigned getRefCount() const { return d_rc; }
+
+ NodeValue* getOperator() const;
+ NodeValue* getChild(int i) const;
+
+ /** If this is a CONST_* Node, extract the constant from it. */
+ template <class T>
+ inline const T& getConst() const;
+
+ static inline NodeValue& null()
+ {
+ static NodeValue* s_null = new NodeValue(0);
+ return *s_null;
+ }
/**
* Hash this NodeValue. For hash_maps, hash_sets, etc.. but this is
* collisions for all VARIABLEs.
* @return the hash value of this expression.
*/
- size_t poolHash() const {
- if(getMetaKind() == kind::metakind::CONSTANT) {
+ size_t poolHash() const
+ {
+ if (getMetaKind() == kind::metakind::CONSTANT)
+ {
return kind::metakind::NodeValueCompare::constHash(this);
}
size_t hash = d_kind;
const_nv_iterator i = nv_begin();
const_nv_iterator i_end = nv_end();
- while(i != i_end) {
+ while (i != i_end)
+ {
hash ^= (*i)->d_id + 0x9e3779b9 + (hash << 6) + (hash >> 2);
++i;
}
return hash;
}
- uint64_t getId() const { return d_id; }
-
- Kind getKind() const { return dKindToKind(d_kind); }
-
- kind::MetaKind getMetaKind() const { return kind::metaKindOf(getKind()); }
-
- uint32_t getNumChildren() const
- {
- return (getMetaKind() == kind::metakind::PARAMETERIZED) ? d_nchildren - 1
- : d_nchildren;
- }
-
- unsigned getRefCount() const { return d_rc; }
-
- std::string toString() const;
- void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
- OutputLanguage = language::output::LANG_AUTO) const;
-
static inline uint32_t kindToDKind(Kind k)
{
return ((uint32_t)k) & kindMask;
return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d);
}
- static inline NodeValue& null() {
- static NodeValue* s_null = new NodeValue(0);
- return *s_null;
- }
-
- /**
- * If this is a CONST_* Node, extract the constant from it.
- */
- template <class T>
- inline const T& getConst() const;
+ std::string toString() const;
- NodeValue* getOperator() const;
- NodeValue* getChild(int i) const;
+ void toStream(std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage = language::output::LANG_AUTO) const;
void printAst(std::ostream& out, int indent = 0) const;
-private:
+ template <typename T>
+ inline iterator<T> begin() const;
+ template <typename T>
+ inline iterator<T> end() const;
+
+ /* ------------------------------------------------------------------------ */
+ private:
+ /* ------------------------------------------------------------------------ */
/**
* RAII guard that increases the reference count if the reference count to be
* reference count to avoid maxing out the d_rc field. This is only for low
* level functions.
*/
- class RefCountGuard {
- NodeValue* d_nv;
- bool d_increased;
- public:
- RefCountGuard(const NodeValue* nv) :
- d_nv(const_cast<NodeValue*>(nv)) {
+ class RefCountGuard
+ {
+ public:
+ RefCountGuard(const NodeValue* nv) : d_nv(const_cast<NodeValue*>(nv))
+ {
d_increased = (d_nv->d_rc == 0);
- if(d_increased) {
+ if (d_increased)
+ {
d_nv->d_rc = 1;
}
}
- ~RefCountGuard() {
+ ~RefCountGuard()
+ {
// dec() without marking for deletion: we don't want to garbage
// collect this NodeValue if ours is the last reference to it.
// E.g., this can happen when debugging code calls the print
// routines below. As RefCountGuards are scoped on the stack,
// this should be fine---but not in multithreaded contexts!
- if(d_increased) {
+ if (d_increased)
+ {
--d_nv->d_rc;
}
}
- };/* NodeValue::RefCountGuard */
- friend class RefCountGuard;
+ private:
+ NodeValue* d_nv;
+ bool d_increased;
+ }; /* NodeValue::RefCountGuard */
+
+ /* ------------------------------ Header ---------------------------------- */
+ static const uint32_t NBITS_REFCOUNT =
+ CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT;
+ static const uint32_t NBITS_KIND = CVC4__EXPR__NODE_VALUE__NBITS__KIND;
+ static const uint32_t NBITS_ID = CVC4__EXPR__NODE_VALUE__NBITS__ID;
+ static const uint32_t NBITS_NCHILDREN =
+ CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN;
+
+ /** Maximum reference count possible. Used for sticky
+ * reference-counting. Should be (1 << num_bits(d_rc)) - 1 */
+ static const uint32_t MAX_RC = (((uint32_t)1) << NBITS_REFCOUNT) - 1;
+
+ /** A mask for d_kind */
+ static const uint32_t kindMask = (((uint32_t)1) << NBITS_KIND) - 1;
+ /* ------------------- This header fits into 96 bits ---------------------- */
+
+ /** Uninitializing constructor for NodeBuilder's use. */
+ NodeValue()
+ { /* do not initialize! */
+ }
+ /** Private constructor for the null value. */
+ NodeValue(int);
+
+ void inc();
+ void dec();
+
+ /** Decrement ref counts of children */
+ inline void decrRefCounts();
+
+ bool isBeingDeleted() const;
+
+ /** Returns true if the reference count is maximized. */
+ inline bool HasMaximizedReferenceCount() { return d_rc == MAX_RC; }
+
+ nv_iterator nv_begin();
+ nv_iterator nv_end();
+
+ const_nv_iterator nv_begin() const;
+ const_nv_iterator nv_end() const;
/**
* Indents the given stream a given amount of spaces.
* @param out the stream to indent
* @param indent the numer of spaces
*/
- static inline void indent(std::ostream& out, int indent) {
- for(int i = 0; i < indent; i++) {
+ static inline void indent(std::ostream& out, int indent)
+ {
+ for (int i = 0; i < indent; i++)
+ {
out << ' ';
}
}
-};/* class NodeValue */
+ /** The ID (0 is reserved for the null value) */
+ uint64_t d_id : NBITS_ID;
+
+ /** The expression's reference count. @see cvc4::Node. */
+ uint32_t d_rc : NBITS_REFCOUNT;
+
+ /** Kind of the expression */
+ uint32_t d_kind : NBITS_KIND;
+
+ /** Number of children */
+ uint32_t d_nchildren : NBITS_NCHILDREN;
+
+ /** Variable number of child nodes */
+ NodeValue* d_children[0];
+}; /* class NodeValue */
/**
* Provides a symmetric addition operator to that already defined in
* the iterator class.
*/
-inline NodeValue::iterator<NodeTemplate<true> >
-operator+(NodeValue::iterator<NodeTemplate<true> >::difference_type p,
- NodeValue::iterator<NodeTemplate<true> > i) {
- return i + p;
-}
+NodeValue::iterator<NodeTemplate<true> > operator+(
+ NodeValue::iterator<NodeTemplate<true> >::difference_type p,
+ NodeValue::iterator<NodeTemplate<true> > i);
/**
* Provides a symmetric addition operator to that already defined in
* the iterator class.
*/
-inline NodeValue::iterator<NodeTemplate<false> >
-operator+(NodeValue::iterator<NodeTemplate<false> >::difference_type p,
- NodeValue::iterator<NodeTemplate<false> > i) {
- return i + p;
-}
+NodeValue::iterator<NodeTemplate<false> > operator+(
+ NodeValue::iterator<NodeTemplate<false> >::difference_type p,
+ NodeValue::iterator<NodeTemplate<false> > i);
/**
* For hash_maps, hash_sets, etc.. but this is for expr package
projects / cvc5.git / commitdiff