Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/attribute_internals.h	Lines:	68	68	100.0 %
Date:	2021-05-22	Branches:	56	184	30.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Tim King, Andres Noetzli
 *
 * 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.
 * ****************************************************************************
 *
 * Node attributes' internals.
 */

#include "cvc5_private.h"

#ifndef CVC5_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
#  error expr/attribute_internals.h should only be included by expr/attribute.h
#endif /* CVC5_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H */

#ifndef CVC5__EXPR__ATTRIBUTE_INTERNALS_H
#define CVC5__EXPR__ATTRIBUTE_INTERNALS_H

#include <unordered_map>

namespace cvc5 {
namespace expr {

// ATTRIBUTE HASH FUNCTIONS ====================================================

namespace attr {

/**
 * A hash function for attribute table keys.  Attribute table keys are
 * pairs, (unique-attribute-id, Node).
 */
struct AttrHashFunction {
  enum { LARGE_PRIME = 32452843ul };
  std::size_t operator()(const std::pair<uint64_t, NodeValue*>& p) const {
    return p.first * LARGE_PRIME + p.second->getId();
  }
};/* struct AttrHashFunction */

/**
 * A hash function for boolean-valued attribute table keys; here we
 * don't have to store a pair as the key, because we use a known bit
 * in [0..63] for each attribute
 */
struct AttrBoolHashFunction {
  std::size_t operator()(NodeValue* nv) const {
    return (size_t)nv->getId();
  }
};/* struct AttrBoolHashFunction */

}  // namespace attr

// ATTRIBUTE TYPE MAPPINGS =====================================================

namespace attr {

/**
 * KindValueToTableValueMapping is a compile-time-only mechanism to
 * convert "attribute value types" into "table value types" and back
 * again.
 *
 * Each instantiation < T > is expected to have three members:
 *
 *   typename table_value_type
 *
 *      A type representing the underlying table's value_type for
 *      attribute value type (T).  It may be different from T, e.g. T
 *      could be a pointer-to-Foo, but the underlying table value_type
 *      might be pointer-to-void.
 *
 *   static [convertible-to-table_value_type] convert([convertible-from-T])
 *
 *      Converts a T into a table_value_type.  Used to convert an
 *      attribute value on setting it (and assigning it into the
 *      underlying table).  See notes on specializations of
 *      KindValueToTableValueMapping, below.
 *
 *   static [convertible-to-T] convertBack([convertible-from-table_value_type])
 *
 *      Converts a table_value_type back into a T.  Used to convert an
 *      underlying table value back into the attribute's expected type
 *      when retrieving it from the table.  See notes on
 *      specializations of KindValueToTableValueMapping, below.
 *
 * This general (non-specialized) implementation of the template does
 * nothing.
 *
 * The `Enable` template parameter is used to instantiate the template
 * conditionally: If the template substitution of Enable fails (e.g. when using
 * `std::enable_if` in the template parameter and the condition is false), the
 * instantiation is ignored due to the SFINAE rule.
 */
template <class T, class Enable = void>
struct KindValueToTableValueMapping
{
  /** Simple case: T == table_value_type */
  typedef T table_value_type;
  /** No conversion necessary */
  inline static T convert(const T& t) { return t; }
  /** No conversion necessary */
  inline static T convertBack(const T& t) { return t; }
};

/**
 * This converts arbitrary unsigned integers (up to 64-bit) to and from 64-bit
 * integers s.t. they can be stored in the hash table for integral-valued
 * attributes.
 */
template <class T>
struct KindValueToTableValueMapping<
    T,
    // Use this specialization only for unsigned integers
    typename std::enable_if<std::is_unsigned<T>::value>::type>
{
  typedef uint64_t table_value_type;
  /** Convert from unsigned integer to uint64_t */
  static uint64_t convert(const T& t)
  {
    static_assert(sizeof(T) <= sizeof(uint64_t),
                  "Cannot store integer attributes of a bit-width that is "
                  "greater than 64-bits");
    return static_cast<uint64_t>(t);
  }
  /** Convert from uint64_t to unsigned integer */
  static T convertBack(const uint64_t& t) { return static_cast<T>(t); }
};

}  // namespace attr

// ATTRIBUTE HASH TABLES =======================================================

namespace attr {

// Returns a 64 bit integer with a single `bit` set when `bit` < 64.
// Avoids problems in (1 << x) when sizeof(x) <= sizeof(uint64_t).
inline uint64_t GetBitSet(uint64_t bit)
{
  constexpr uint64_t kOne = 1;
  return kOne << bit;
}

/**
 * An "AttrHash<value_type>"---the hash table underlying
 * attributes---is simply a mapping of pair<unique-attribute-id, Node>
 * to value_type using our specialized hash function for these pairs.
 */
template <class value_type>
class AttrHash :
    public std::unordered_map<std::pair<uint64_t, NodeValue*>,
                               value_type,
                               AttrHashFunction> {
};/* class AttrHash<> */

/**
 * In the case of Boolean-valued attributes we have a special
 * "AttrHash<bool>" to pack bits together in words.
 */
template <>
class AttrHash<bool> :
    protected std::unordered_map<NodeValue*,
                                  uint64_t,
                                  AttrBoolHashFunction> {

  /** A "super" type, like in Java, for easy reference below. */
  typedef std::unordered_map<NodeValue*, uint64_t, AttrBoolHashFunction> super;

  /**
   * BitAccessor allows us to return a bit "by reference."  Of course,
   * we don't require bit-addressibility supported by the system, we
   * do it with a complex type.
   */
  class BitAccessor {

    uint64_t& d_word;

    uint64_t d_bit;

   public:
    BitAccessor(uint64_t& word, uint64_t bit) : d_word(word), d_bit(bit) {}

    BitAccessor& operator=(bool b) {
      if(b) {
        // set the bit
        d_word |= GetBitSet(d_bit);
      } else {
        // clear the bit
        d_word &= ~GetBitSet(d_bit);
      }

      return *this;
    }

    operator bool() const { return (d_word & GetBitSet(d_bit)) ? true : false; }
  };/* class AttrHash<bool>::BitAccessor */

  /**
   * A (somewhat degenerate) iterator over boolean-valued attributes.
   * This iterator doesn't support anything except comparison and
   * dereference.  It's intended just for the result of find() on the
   * table.
   */
  class BitIterator {

    std::pair<NodeValue* const, uint64_t>* d_entry;

    uint64_t d_bit;

   public:

    BitIterator() :
      d_entry(NULL),
      d_bit(0) {
    }

    BitIterator(std::pair<NodeValue* const, uint64_t>& entry, uint64_t bit)
        : d_entry(&entry), d_bit(bit)
    {
    }

    std::pair<NodeValue* const, BitAccessor> operator*() {
      return std::make_pair(d_entry->first,
                            BitAccessor(d_entry->second, d_bit));
    }

    bool operator==(const BitIterator& b) {
      return d_entry == b.d_entry && d_bit == b.d_bit;
    }
  };/* class AttrHash<bool>::BitIterator */

  /**
   * A (somewhat degenerate) const_iterator over boolean-valued
   * attributes.  This const_iterator doesn't support anything except
   * comparison and dereference.  It's intended just for the result of
   * find() on the table.
   */
  class ConstBitIterator {

    const std::pair<NodeValue* const, uint64_t>* d_entry;

    uint64_t d_bit;

   public:

    ConstBitIterator() :
      d_entry(NULL),
      d_bit(0) {
    }

    ConstBitIterator(const std::pair<NodeValue* const, uint64_t>& entry,
                     uint64_t bit)
        : d_entry(&entry), d_bit(bit)
    {
    }

    std::pair<NodeValue* const, bool> operator*()
    {
      return std::make_pair(
          d_entry->first, (d_entry->second & GetBitSet(d_bit)) ? true : false);
    }

    bool operator==(const ConstBitIterator& b) {
      return d_entry == b.d_entry && d_bit == b.d_bit;
    }
  };/* class AttrHash<bool>::ConstBitIterator */

public:

  typedef std::pair<uint64_t, NodeValue*> key_type;
  typedef bool data_type;
  typedef std::pair<const key_type, data_type> value_type;

  /** an iterator type; see above for limitations */
  typedef BitIterator iterator;
  /** a const_iterator type; see above for limitations */
  typedef ConstBitIterator const_iterator;

  /**
   * Find the boolean value in the hash table.  Returns something ==
   * end() if not found.
   */
  BitIterator find(const std::pair<uint64_t, NodeValue*>& k) {
    super::iterator i = super::find(k.second);
    if(i == super::end()) {
      return BitIterator();
    }
    /*
    Debug.printf("boolattr",
                 "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
                 &(*i).second,
                 (uint64_t)((*i).second),
                 uint64_t(k.first));
    */
    return BitIterator(*i, k.first);
  }

  /** The "off the end" iterator */
  BitIterator end() {
    return BitIterator();
  }

  /**
   * Find the boolean value in the hash table.  Returns something ==
   * end() if not found.
   */
  ConstBitIterator find(const std::pair<uint64_t, NodeValue*>& k) const {
    super::const_iterator i = super::find(k.second);
    if(i == super::end()) {
      return ConstBitIterator();
    }
    /*
    Debug.printf("boolattr",
                 "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
                 &(*i).second,
                 (uint64_t)((*i).second),
                 uint64_t(k.first));
    */
    return ConstBitIterator(*i, k.first);
  }

  /** The "off the end" const_iterator */
  ConstBitIterator end() const {
    return ConstBitIterator();
  }

  /**
   * Access the hash table using the underlying operator[].  Inserts
   * the key into the table (associated to default value) if it's not
   * already there.
   */
  BitAccessor operator[](const std::pair<uint64_t, NodeValue*>& k) {
    uint64_t& word = super::operator[](k.second);
    return BitAccessor(word, k.first);
  }

  /**
   * Delete all flags from the given node.
   */
  void erase(NodeValue* nv) {
    super::erase(nv);
  }

  /**
   * Clear the hash table.
   */
  void clear() {
    super::clear();
  }

  /** Is the hash table empty? */
  bool empty() const {
    return super::empty();
  }

  /** This is currently very misleading! */
  size_t size() const {
    return super::size();
  }
};/* class AttrHash<bool> */

}  // namespace attr

// ATTRIBUTE IDENTIFIER ASSIGNMENT TEMPLATE ====================================

namespace attr {

/**
 * This is the last-attribute-assigner.  IDs are not globally
 * unique; rather, they are unique for each table_value_type.
 */
template <class T, bool context_dep>
struct LastAttributeId {
 public:
  static uint64_t getNextId() {
    uint64_t* id = raw_id();
    const uint64_t next_id = *id;
    ++(*id);
    return next_id;
  }
  static uint64_t getId() {
    return *raw_id();
  }
 private:
  static uint64_t* raw_id()
  {
    static uint64_t s_id = 0;
    return &s_id;
  }
};

}  // namespace attr

// ATTRIBUTE DEFINITION ========================================================

/**
 * An "attribute type" structure.
 *
 * @param T the tag for the attribute kind.
 *
 * @param value_t the underlying value_type for the attribute kind
 *
 * @param context_dep whether this attribute kind is
 * context-dependent
 */
template <class T, class value_t, bool context_dep = false>
class Attribute
{
  /**
   * The unique ID associated to this attribute.  Assigned statically,
   * at load time.
   */
  static const uint64_t s_id;

public:

  /** The value type for this attribute. */
  typedef value_t value_type;

  /** Get the unique ID associated to this attribute. */
  static inline uint64_t getId() { return s_id; }

  /**
   * This attribute does not have a default value: calling
   * hasAttribute() for a Node that hasn't had this attribute set will
   * return false, and getAttribute() for the Node will return a
   * default-constructed value_type.
   */
  static const bool has_default_value = false;

  /**
   * Expose this setting to the users of this Attribute kind.
   */
  static const bool context_dependent = context_dep;

  /**
   * Register this attribute kind and check that the ID is a valid ID
   * for bool-valued attributes.  Fail an assert if not.  Otherwise
   * return the id.
   */
  static inline uint64_t registerAttribute() {
    typedef typename attr::KindValueToTableValueMapping<value_t>::
                     table_value_type table_value_type;
    return attr::LastAttributeId<table_value_type, context_dep>::getNextId();
  }
};/* class Attribute<> */

/**
 * An "attribute type" structure for boolean flags (special).
 */
template <class T, bool context_dep>
class Attribute<T, bool, context_dep>
{
  /** IDs for bool-valued attributes are actually bit assignments. */
  static const uint64_t s_id;

public:

  /** The value type for this attribute; here, bool. */
  typedef bool value_type;

  /** Get the unique ID associated to this attribute. */
  static inline uint64_t getId() { return s_id; }

  /**
   * Such bool-valued attributes ("flags") have a default value: they
   * are false for all nodes on entry.  Calling hasAttribute() for a
   * Node that hasn't had this attribute set will return true, and
   * getAttribute() for the Node will return the default_value below.
   */
  static const bool has_default_value = true;

  /**
   * Default value of the attribute for Nodes without one explicitly
   * set.
   */
  static const bool default_value = false;

  /**
   * Expose this setting to the users of this Attribute kind.
   */
  static const bool context_dependent = context_dep;

  /**
   * Register this attribute kind and check that the ID is a valid ID
   * for bool-valued attributes.  Fail an assert if not.  Otherwise
   * return the id.
   */
  static inline uint64_t registerAttribute() {
    const uint64_t id = attr::LastAttributeId<bool, context_dep>::getNextId();
    AlwaysAssert(id <= 63) << "Too many boolean node attributes registered "
                              "during initialization !";
    return id;
  }
};/* class Attribute<..., bool, ...> */

// ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================

/** Assign unique IDs to attributes at load time. */
template <class T, class value_t, bool context_dep>
const uint64_t Attribute<T, value_t, context_dep>::s_id =
    Attribute<T, value_t,  context_dep>::registerAttribute();


/** Assign unique IDs to attributes at load time. */
template <class T, bool context_dep>
const uint64_t Attribute<T, bool, context_dep>::s_id =
    Attribute<T, bool, context_dep>::registerAttribute();

}  // namespace expr
}  // namespace cvc5

#endif /* CVC5__EXPR__ATTRIBUTE_INTERNALS_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters, Tim King, Andres Noetzli
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		* Node attributes' internals.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
19		# error expr/attribute_internals.h should only be included by expr/attribute.h
20		#endif /* CVC5_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H */
21
22		#ifndef CVC5__EXPR__ATTRIBUTE_INTERNALS_H
23		#define CVC5__EXPR__ATTRIBUTE_INTERNALS_H
24
25		#include <unordered_map>
26
27		namespace cvc5 {
28		namespace expr {
29
30		// ATTRIBUTE HASH FUNCTIONS ====================================================
31
32		namespace attr {
33
34		/**
35		* A hash function for attribute table keys. Attribute table keys are
36		* pairs, (unique-attribute-id, Node).
37		*/
38		struct AttrHashFunction {
39		enum { LARGE_PRIME = 32452843ul };
40	3912433818	std::size_t operator()(const std::pair<uint64_t, NodeValue*>& p) const {
41	3912433818	return p.first * LARGE_PRIME + p.second->getId();
42		}
43		};/* struct AttrHashFunction */
44
45		/**
46		* A hash function for boolean-valued attribute table keys; here we
47		* don't have to store a pair as the key, because we use a known bit
48		* in [0..63] for each attribute
49		*/
50		struct AttrBoolHashFunction {
51	773967192	std::size_t operator()(NodeValue* nv) const {
52	773967192	return (size_t)nv->getId();
53		}
54		};/* struct AttrBoolHashFunction */
55
56		} // namespace attr
57
58		// ATTRIBUTE TYPE MAPPINGS =====================================================
59
60		namespace attr {
61
62		/**
63		* KindValueToTableValueMapping is a compile-time-only mechanism to
64		* convert "attribute value types" into "table value types" and back
65		* again.
66		*
67		* Each instantiation < T > is expected to have three members:
68		*
69		* typename table_value_type
70		*
71		* A type representing the underlying table's value_type for
72		* attribute value type (T). It may be different from T, e.g. T
73		* could be a pointer-to-Foo, but the underlying table value_type
74		* might be pointer-to-void.
75		*
76		* static [convertible-to-table_value_type] convert([convertible-from-T])
77		*
78		* Converts a T into a table_value_type. Used to convert an
79		* attribute value on setting it (and assigning it into the
80		* underlying table). See notes on specializations of
81		* KindValueToTableValueMapping, below.
82		*
83		* static [convertible-to-T] convertBack([convertible-from-table_value_type])
84		*
85		* Converts a table_value_type back into a T. Used to convert an
86		* underlying table value back into the attribute's expected type
87		* when retrieving it from the table. See notes on
88		* specializations of KindValueToTableValueMapping, below.
89		*
90		* This general (non-specialized) implementation of the template does
91		* nothing.
92		*
93		* The `Enable` template parameter is used to instantiate the template
94		* conditionally: If the template substitution of Enable fails (e.g. when using
95		* `std::enable_if` in the template parameter and the condition is false), the
96		* instantiation is ignored due to the SFINAE rule.
97		*/
98		template <class T, class Enable = void>
99		struct KindValueToTableValueMapping
100		{
101		/** Simple case: T == table_value_type */
102		typedef T table_value_type;
103		/** No conversion necessary */
104	51815178	inline static T convert(const T& t) { return t; }
105		/** No conversion necessary */
106	767637676	inline static T convertBack(const T& t) { return t; }
107		};
108
109		/**
110		* This converts arbitrary unsigned integers (up to 64-bit) to and from 64-bit
111		* integers s.t. they can be stored in the hash table for integral-valued
112		* attributes.
113		*/
114		template <class T>
115		struct KindValueToTableValueMapping<
116		T,
117		// Use this specialization only for unsigned integers
118		typename std::enable_if<std::is_unsigned<T>::value>::type>
119		{
120		typedef uint64_t table_value_type;
121		/** Convert from unsigned integer to uint64_t */
122	42139171	static uint64_t convert(const T& t)
123		{
124		static_assert(sizeof(T) <= sizeof(uint64_t),
125		"Cannot store integer attributes of a bit-width that is "
126		"greater than 64-bits");
127	42139171	return static_cast<uint64_t>(t);
128		}
129		/** Convert from uint64_t to unsigned integer */
130	686928992	static T convertBack(const uint64_t& t) { return static_cast<T>(t); }
131		};
132
133		} // namespace attr
134
135		// ATTRIBUTE HASH TABLES =======================================================
136
137		namespace attr {
138
139		// Returns a 64 bit integer with a single `bit` set when `bit` < 64.
140		// Avoids problems in (1 << x) when sizeof(x) <= sizeof(uint64_t).
141	718427859	inline uint64_t GetBitSet(uint64_t bit)
142		{
143	718427859	constexpr uint64_t kOne = 1;
144	718427859	return kOne << bit;
145		}
146
147		/**
148		* An "AttrHash<value_type>"---the hash table underlying
149		* attributes---is simply a mapping of pair<unique-attribute-id, Node>
150		* to value_type using our specialized hash function for these pairs.
151		*/
152		template <class value_type>
153	76730	class AttrHash :
154		public std::unordered_map<std::pair<uint64_t, NodeValue*>,
155		value_type,
156		AttrHashFunction> {
157		};/* class AttrHash<> */
158
159		/**
160		* In the case of Boolean-valued attributes we have a special
161		* "AttrHash<bool>" to pack bits together in words.
162		*/
163		template <>
164	15346	class AttrHash<bool> :
165		protected std::unordered_map<NodeValue*,
166		uint64_t,
167		AttrBoolHashFunction> {
168
169		/** A "super" type, like in Java, for easy reference below. */
170		typedef std::unordered_map<NodeValue*, uint64_t, AttrBoolHashFunction> super;
171
172		/**
173		* BitAccessor allows us to return a bit "by reference." Of course,
174		* we don't require bit-addressibility supported by the system, we
175		* do it with a complex type.
176		*/
177		class BitAccessor {
178
179		uint64_t& d_word;
180
181		uint64_t d_bit;
182
183		public:
184	41937067	BitAccessor(uint64_t& word, uint64_t bit) : d_word(word), d_bit(bit) {}
185
186	41937067	BitAccessor& operator=(bool b) {
187	41937067	if(b) {
188		// set the bit
189	35192106	d_word \|= GetBitSet(d_bit);
190		} else {
191		// clear the bit
192	6744961	d_word &= ~GetBitSet(d_bit);
193		}
194
195	41937067	return *this;
196		}
197
198		operator bool() const { return (d_word & GetBitSet(d_bit)) ? true : false; }
199		};/* class AttrHash<bool>::BitAccessor */
200
201		/**
202		* A (somewhat degenerate) iterator over boolean-valued attributes.
203		* This iterator doesn't support anything except comparison and
204		* dereference. It's intended just for the result of find() on the
205		* table.
206		*/
207		class BitIterator {
208
209		std::pair<NodeValue* const, uint64_t>* d_entry;
210
211		uint64_t d_bit;
212
213		public:
214
215		BitIterator() :
216		d_entry(NULL),
217		d_bit(0) {
218		}
219
220		BitIterator(std::pair<NodeValue* const, uint64_t>& entry, uint64_t bit)
221		: d_entry(&entry), d_bit(bit)
222		{
223		}
224
225		std::pair<NodeValue* const, BitAccessor> operator*() {
226		return std::make_pair(d_entry->first,
227		BitAccessor(d_entry->second, d_bit));
228		}
229
230		bool operator==(const BitIterator& b) {
231		return d_entry == b.d_entry && d_bit == b.d_bit;
232		}
233		};/* class AttrHash<bool>::BitIterator */
234
235		/**
236		* A (somewhat degenerate) const_iterator over boolean-valued
237		* attributes. This const_iterator doesn't support anything except
238		* comparison and dereference. It's intended just for the result of
239		* find() on the table.
240		*/
241		class ConstBitIterator {
242
243		const std::pair<NodeValue* const, uint64_t>* d_entry;
244
245		uint64_t d_bit;
246
247		public:
248
249	728831092	ConstBitIterator() :
250		d_entry(NULL),
251	728831092	d_bit(0) {
252	728831092	}
253
254	676490792	ConstBitIterator(const std::pair<NodeValue* const, uint64_t>& entry,
255		uint64_t bit)
256	676490792	: d_entry(&entry), d_bit(bit)
257		{
258	676490792	}
259
260	676490792	std::pair<NodeValue* const, bool> operator*()
261		{
262	1352981584	return std::make_pair(
263	2029472376	d_entry->first, (d_entry->second & GetBitSet(d_bit)) ? true : false);
264		}
265
266	702660942	bool operator==(const ConstBitIterator& b) {
267	702660942	return d_entry == b.d_entry && d_bit == b.d_bit;
268		}
269		};/* class AttrHash<bool>::ConstBitIterator */
270
271		public:
272
273		typedef std::pair<uint64_t, NodeValue*> key_type;
274		typedef bool data_type;
275		typedef std::pair<const key_type, data_type> value_type;
276
277		/** an iterator type; see above for limitations */
278		typedef BitIterator iterator;
279		/** a const_iterator type; see above for limitations */
280		typedef ConstBitIterator const_iterator;
281
282		/**
283		* Find the boolean value in the hash table. Returns something ==
284		* end() if not found.
285		*/
286		BitIterator find(const std::pair<uint64_t, NodeValue*>& k) {
287		super::iterator i = super::find(k.second);
288		if(i == super::end()) {
289		return BitIterator();
290		}
291		/*
292		Debug.printf("boolattr",
293		"underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
294		&(*i).second,
295		(uint64_t)((*i).second),
296		uint64_t(k.first));
297		*/
298		return BitIterator(*i, k.first);
299		}
300
301		/** The "off the end" iterator */
302		BitIterator end() {
303		return BitIterator();
304		}
305
306		/**
307		* Find the boolean value in the hash table. Returns something ==
308		* end() if not found.
309		*/
310	702660942	ConstBitIterator find(const std::pair<uint64_t, NodeValue*>& k) const {
311	702660942	super::const_iterator i = super::find(k.second);
312	702660942	if(i == super::end()) {
313	26170150	return ConstBitIterator();
314		}
315		/*
316		Debug.printf("boolattr",
317		"underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
318		&(*i).second,
319		(uint64_t)((*i).second),
320		uint64_t(k.first));
321		*/
322	676490792	return ConstBitIterator(*i, k.first);
323		}
324
325		/** The "off the end" const_iterator */
326	702660942	ConstBitIterator end() const {
327	702660942	return ConstBitIterator();
328		}
329
330		/**
331		* Access the hash table using the underlying operator[]. Inserts
332		* the key into the table (associated to default value) if it's not
333		* already there.
334		*/
335	41937067	BitAccessor operator[](const std::pair<uint64_t, NodeValue*>& k) {
336	41937067	uint64_t& word = super::operator[](k.second);
337	41937067	return BitAccessor(word, k.first);
338		}
339
340		/**
341		* Delete all flags from the given node.
342		*/
343	29475230	void erase(NodeValue* nv) {
344	29475230	super::erase(nv);
345	29475230	}
346
347		/**
348		* Clear the hash table.
349		*/
350	7673	void clear() {
351	7673	super::clear();
352	7673	}
353
354		/** Is the hash table empty? */
355		bool empty() const {
356		return super::empty();
357		}
358
359		/** This is currently very misleading! */
360		size_t size() const {
361		return super::size();
362		}
363		};/* class AttrHash<bool> */
364
365		} // namespace attr
366
367		// ATTRIBUTE IDENTIFIER ASSIGNMENT TEMPLATE ====================================
368
369		namespace attr {
370
371		/**
372		* This is the last-attribute-assigner. IDs are not globally
373		* unique; rather, they are unique for each table_value_type.
374		*/
375		template <class T, bool context_dep>
376		struct LastAttributeId {
377		public:
378	986727	static uint64_t getNextId() {
379	986727	uint64_t* id = raw_id();
380	986727	const uint64_t next_id = *id;
381	986727	++(*id);
382	986727	return next_id;
383		}
384	147376156	static uint64_t getId() {
385	147376156	return *raw_id();
386		}
387		private:
388	148044742	static uint64_t* raw_id()
389		{
390		static uint64_t s_id = 0;
391	148044742	return &s_id;
392		}
393		};
394
395		} // namespace attr
396
397		// ATTRIBUTE DEFINITION ========================================================
398
399		/**
400		* An "attribute type" structure.
401		*
402		* @param T the tag for the attribute kind.
403		*
404		* @param value_t the underlying value_type for the attribute kind
405		*
406		* @param context_dep whether this attribute kind is
407		* context-dependent
408		*/
409		template <class T, class value_t, bool context_dep = false>
410		class Attribute
411		{
412		/**
413		* The unique ID associated to this attribute. Assigned statically,
414		* at load time.
415		*/
416		static const uint64_t s_id;
417
418		public:
419
420		/** The value type for this attribute. */
421		typedef value_t value_type;
422
423		/** Get the unique ID associated to this attribute. */
424	1721793837	static inline uint64_t getId() { return s_id; }
425
426		/**
427		* This attribute does not have a default value: calling
428		* hasAttribute() for a Node that hasn't had this attribute set will
429		* return false, and getAttribute() for the Node will return a
430		* default-constructed value_type.
431		*/
432		static const bool has_default_value = false;
433
434		/**
435		* Expose this setting to the users of this Attribute kind.
436		*/
437		static const bool context_dependent = context_dep;
438
439		/**
440		* Register this attribute kind and check that the ID is a valid ID
441		* for bool-valued attributes. Fail an assert if not. Otherwise
442		* return the id.
443		*/
444	704852	static inline uint64_t registerAttribute() {
445		typedef typename attr::KindValueToTableValueMapping<value_t>::
446		table_value_type table_value_type;
447	704852	return attr::LastAttributeId<table_value_type, context_dep>::getNextId();
448		}
449		};/* class Attribute<> */
450
451		/**
452		* An "attribute type" structure for boolean flags (special).
453		*/
454		template <class T, bool context_dep>
455		class Attribute<T, bool, context_dep>
456		{
457		/** IDs for bool-valued attributes are actually bit assignments. */
458		static const uint64_t s_id;
459
460		public:
461
462		/** The value type for this attribute; here, bool. */
463		typedef bool value_type;
464
465		/** Get the unique ID associated to this attribute. */
466	750768437	static inline uint64_t getId() { return s_id; }
467
468		/**
469		* Such bool-valued attributes ("flags") have a default value: they
470		* are false for all nodes on entry. Calling hasAttribute() for a
471		* Node that hasn't had this attribute set will return true, and
472		* getAttribute() for the Node will return the default_value below.
473		*/
474		static const bool has_default_value = true;
475
476		/**
477		* Default value of the attribute for Nodes without one explicitly
478		* set.
479		*/
480		static const bool default_value = false;
481
482		/**
483		* Expose this setting to the users of this Attribute kind.
484		*/
485		static const bool context_dependent = context_dep;
486
487		/**
488		* Register this attribute kind and check that the ID is a valid ID
489		* for bool-valued attributes. Fail an assert if not. Otherwise
490		* return the id.
491		*/
492	281952	static inline uint64_t registerAttribute() {
493	281952	const uint64_t id = attr::LastAttributeId<bool, context_dep>::getNextId();
494	281952	AlwaysAssert(id <= 63) << "Too many boolean node attributes registered "
495		"during initialization !";
496	281952	return id;
497		}
498		};/* class Attribute<..., bool, ...> */
499
500		// ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
501
502		/** Assign unique IDs to attributes at load time. */
503		template <class T, class value_t, bool context_dep>
504	1278142	const uint64_t Attribute<T, value_t, context_dep>::s_id =
505	704852	Attribute<T, value_t, context_dep>::registerAttribute();
506
507
508		/** Assign unique IDs to attributes at load time. */
509		template <class T, bool context_dep>
510	592093	const uint64_t Attribute<T, bool, context_dep>::s_id =
511	281952	Attribute<T, bool, context_dep>::registerAttribute();
512
513		} // namespace expr
514		} // namespace cvc5
515
516		#endif /* CVC5__EXPR__ATTRIBUTE_INTERNALS_H */