Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/node_value.h	Lines:	105	139	75.5 %
Date:	2021-05-22	Branches:	43	187	23.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Aina Niemetz, Dejan Jovanovic
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * A node value.
 *
 * The actual node implementation.
 * Instances of this class are generally referenced through cvc5::Node rather
 * than by pointer. Note that cvc5::Node maintains the reference count on
 * NodeValue instances.
 */

#include "cvc5_private.h"

// circular dependency
#include "expr/metakind.h"

#ifndef CVC5__EXPR__NODE_VALUE_H
#define CVC5__EXPR__NODE_VALUE_H

#include <iterator>
#include <string>

#include "expr/kind.h"
#include "options/language.h"

namespace cvc5 {

template <bool ref_count> class NodeTemplate;
class TypeNode;
class NodeBuilder;
class NodeManager;

namespace expr {
  class NodeValue;
}

namespace kind {
  namespace metakind {
  template < ::cvc5::Kind k, bool pool>
  struct NodeValueConstCompare;

  struct NodeValueCompare;
  struct NodeValueConstPrinter;

  void deleteNodeValueConstant(::cvc5::expr::NodeValue* nv);
  }  // namespace metakind
  }  // namespace kind

namespace expr {

/**
 * This is a NodeValue.
 */
class NodeValue
{
  template <bool>
  friend class ::cvc5::NodeTemplate;
  friend class ::cvc5::TypeNode;
  friend class ::cvc5::NodeBuilder;
  friend class ::cvc5::NodeManager;

  template <Kind k, bool pool>
  friend struct ::cvc5::kind::metakind::NodeValueConstCompare;

  friend struct ::cvc5::kind::metakind::NodeValueCompare;
  friend struct ::cvc5::kind::metakind::NodeValueConstPrinter;

  friend void ::cvc5::kind::metakind::deleteNodeValueConstant(NodeValue* nv);

  friend class RefCountGuard;

  /* ------------------------------------------------------------------------ */
 public:
  /* ------------------------------------------------------------------------ */

  using nv_iterator = NodeValue**;
  using const_nv_iterator = NodeValue const* const*;

  template <class T>
  class iterator
  {
   public:
    using iterator_category = std::random_access_iterator_tag;
    using value_type = T;
    using difference_type = std::ptrdiff_t;
    using pointer = T*;
    using reference = T&;

    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> >()
    {
      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; }

    iterator& operator++()
    {
      ++d_i;
      return *this;
    }

    iterator operator++(int) { return iterator(d_i++); }

    iterator& operator--()
    {
      --d_i;
      return *this;
    }

    iterator operator--(int) { return iterator(d_i--); }

    iterator& operator+=(difference_type p)
    {
      d_i += p;
      return *this;
    }

    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); }

    difference_type operator-(iterator i) { return d_i - i.d_i; }

   private:
    const_nv_iterator d_i;

  }; /* class NodeValue::iterator<T> */

  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;
  }

  /* ------------------------------ Header ---------------------------------- */
  /** Number of bits reserved for reference counting. */
  static constexpr uint32_t NBITS_REFCOUNT = 20;
  /** Number of bits reserved for node kind. */
  static constexpr uint32_t NBITS_KIND = 10;
  /** Number of bits reserved for node id. */
  static constexpr uint32_t NBITS_ID = 40;
  /** Number of bits reserved for number of children. */
  static const uint32_t NBITS_NCHILDREN = 26;
  static_assert(NBITS_REFCOUNT + NBITS_KIND + NBITS_ID + NBITS_NCHILDREN == 96,
                "NodeValue header bit assignment does not sum to 96 !");
  /* ------------------- This header fits into 96 bits ---------------------- */

  /** Maximum number of children possible. */
  static constexpr uint32_t MAX_CHILDREN =
      (static_cast<uint32_t>(1) << NBITS_NCHILDREN) - 1;

  uint32_t 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
   * for expr package internal use only at present!  This is likely to
   * be POORLY PERFORMING for other uses!  For example, this gives
   * collisions for all VARIABLEs.
   * @return the hash value of this expression.
   */
  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)
    {
      hash ^= (*i)->d_id + 0x9e3779b9 + (hash << 6) + (hash >> 2);
      ++i;
    }
    return hash;
  }

  static inline uint32_t kindToDKind(Kind k)
  {
    return ((uint32_t)k) & kindMask;
  }

  static inline Kind dKindToKind(uint32_t d)
  {
    return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d);
  }

  std::string toString() const;

  void toStream(std::ostream& out,
                int toDepth = -1,
                size_t dag = 1,
                OutputLanguage = language::output::LANG_AUTO) const;

  void printAst(std::ostream& out, int indent = 0) const;

  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
   * > 0.  Otherwise, this does nothing. This does not just increment the
   * reference count to avoid maxing out the d_rc field. This is only for low
   * level functions.
   */
  class RefCountGuard
  {
   public:
    RefCountGuard(const NodeValue* nv) : d_nv(const_cast<NodeValue*>(nv))
    {
      d_increased = (d_nv->d_rc == 0);
      if (d_increased)
      {
        d_nv->d_rc = 1;
      }
    }
    ~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)
      {
        --d_nv->d_rc;
      }
    }

   private:
    NodeValue* d_nv;
    bool d_increased;
  }; /* NodeValue::RefCountGuard */

  /** Maximum reference count possible.  Used for sticky
   *  reference-counting.  Should be (1 << num_bits(d_rc)) - 1 */
  static constexpr uint32_t MAX_RC =
      (static_cast<uint32_t>(1) << NBITS_REFCOUNT) - 1;

  /** A mask for d_kind */
  static constexpr uint32_t kindMask =
      (static_cast<uint32_t>(1) << NBITS_KIND) - 1;

  /** 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++)
    {
      out << ' ';
    }
  }

  /** The ID (0 is reserved for the null value) */
  uint64_t d_id : NBITS_ID;

  /** The expression's reference count. */
  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.
 */
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.
 */
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
 * internal use only at present!  This is likely to be POORLY
 * PERFORMING for other uses!  NodeValue::poolHash() will lead to
 * collisions for all VARIABLEs.
 */
struct NodeValuePoolHashFunction {
  inline size_t operator()(const NodeValue* nv) const {
    return (size_t) nv->poolHash();
  }
};/* struct NodeValuePoolHashFunction */

/**
 * For hash_maps, hash_sets, etc.
 */
struct NodeValueIDHashFunction {
  inline size_t operator()(const NodeValue* nv) const {
    return (size_t) nv->getId();
  }
};/* struct NodeValueIDHashFunction */


/**
 * An equality predicate that is applicable between pointers to fully
 * constructed NodeValues.
 */
struct NodeValueIDEquality {
  inline bool operator()(const NodeValue* a, const NodeValue* b) const {
    return a->getId() == b->getId();
  }
};


inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv);

}  // namespace expr
}  // namespace cvc5

#include "expr/node_manager.h"

namespace cvc5 {
namespace expr {

inline NodeValue::NodeValue(int) :
  d_id(0),
  d_rc(MAX_RC),
  d_kind(kind::NULL_EXPR),
  d_nchildren(0) {
}

inline void NodeValue::decrRefCounts() {
  for(nv_iterator i = nv_begin(); i != nv_end(); ++i) {
    (*i)->dec();
  }
}

inline void NodeValue::inc() {
  Assert(!isBeingDeleted())
      << "NodeValue is currently being deleted "
         "and increment is being called on it. Don't Do That!";
  // FIXME multithreading
  if (__builtin_expect((d_rc < MAX_RC - 1), true)) {
    ++d_rc;
  } else if (__builtin_expect((d_rc == MAX_RC - 1), false)) {
    ++d_rc;
    Assert(NodeManager::currentNM() != NULL)
        << "No current NodeManager on incrementing of NodeValue: "
           "maybe a public cvc5 interface function is missing a "
           "NodeManagerScope ?";
    NodeManager::currentNM()->markRefCountMaxedOut(this);
  }
}

inline void NodeValue::dec() {
  // FIXME multithreading
  if(__builtin_expect( ( d_rc < MAX_RC ), true )) {
    --d_rc;
    if(__builtin_expect( ( d_rc == 0 ), false )) {
      Assert(NodeManager::currentNM() != NULL)
          << "No current NodeManager on destruction of NodeValue: "
             "maybe a public cvc5 interface function is missing a "
             "NodeManagerScope ?";
      NodeManager::currentNM()->markForDeletion(this);
    }
  }
}

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;
}

template <typename T>
inline NodeValue::iterator<T> NodeValue::begin() const {
  NodeValue* const* firstChild = d_children;
  if(getMetaKind() == kind::metakind::PARAMETERIZED) {
    ++firstChild;
  }
  return iterator<T>(firstChild);
}

template <typename T>
inline NodeValue::iterator<T> NodeValue::end() const {
  return iterator<T>(d_children + d_nchildren);
}

inline bool NodeValue::isBeingDeleted() const {
  return NodeManager::currentNM() != NULL &&
    NodeManager::currentNM()->isCurrentlyDeleting(this);
}

inline NodeValue* NodeValue::getOperator() const {
  Assert(getMetaKind() == kind::metakind::PARAMETERIZED);
  return d_children[0];
}

inline NodeValue* NodeValue::getChild(int i) const {
  if(getMetaKind() == kind::metakind::PARAMETERIZED) {
    ++i;
  }

  Assert(i >= 0 && unsigned(i) < d_nchildren);
  return d_children[i];
}

}  // namespace expr
}  // namespace cvc5

#include "expr/node.h"

namespace cvc5 {
namespace expr {

template <typename T>
inline T NodeValue::iterator<T>::operator*() const {
  return T(*d_i);
}

inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) {
  nv.toStream(out,
              Node::setdepth::getDepth(out),
              Node::dag::getDag(out),
              Node::setlanguage::getLanguage(out));
  return out;
}

}  // namespace expr

#ifdef CVC5_DEBUG
/**
 * Pretty printer for use within gdb.  This is not intended to be used
 * outside of gdb.  This writes to the Warning() stream and immediately
 * flushes the stream.
 */
static void __attribute__((used)) debugPrintNodeValue(const expr::NodeValue* nv) {
  Warning() << Node::setdepth(-1)
            << Node::dag(true)
            << Node::setlanguage(language::output::LANG_AST)
            << *nv << std::endl;
  Warning().flush();
}
static void __attribute__((used)) debugPrintNodeValueNoDag(const expr::NodeValue* nv) {
  Warning() << Node::setdepth(-1)
            << Node::dag(false)
            << Node::setlanguage(language::output::LANG_AST)
            << *nv << std::endl;
  Warning().flush();
}
static void __attribute__((used)) debugPrintRawNodeValue(const expr::NodeValue* nv) {
  nv->printAst(Warning(), 0);
  Warning().flush();
}
#endif /* CVC5_DEBUG */

}  // namespace cvc5

#endif /* CVC5__EXPR__NODE_VALUE_H */


Generated by: GCOVR (Version 3.2)

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