Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/attribute.h	Lines:	95	127	74.8 %
Date:	2021-09-07	Branches:	557	1201	46.4 %


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

#include "cvc5_private.h"

/* There are strong constraints on ordering of declarations of
 * attributes and nodes due to template use */
#include "expr/node.h"
#include "expr/type_node.h"

#ifndef CVC5__EXPR__ATTRIBUTE_H
#define CVC5__EXPR__ATTRIBUTE_H

#include <string>
#include "expr/attribute_unique_id.h"

// include supporting templates
#define CVC5_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
#include "expr/attribute_internals.h"
#undef CVC5_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H

namespace cvc5 {
namespace expr {
namespace attr {

/**
 * Attributes are roughly speaking [almost] global hash tables from Nodes
 * (TNodes) to data. Attributes can be thought of as additional fields used to
 * extend NodeValues. Attributes are mutable. Attributes live only as long as
 * the node itself does. If a Node is garbage-collected, Attributes associated
 * with it will automatically be garbage collected. (Being in the domain of an
 * Attribute does not increase a Node's reference count.) To achieve this
 * special relationship with Nodes, Attributes are mapped by hash tables
 * (AttrHash<>) that live in the AttributeManager. The AttributeManager is
 * owned by the NodeManager.
 *
 * Example:
 *
 * Attributes tend to be defined in a fixed pattern:
 *
 * ```
 * struct InstLevelAttributeId {};
 * typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
 * ```
 *
 * To get the value of an Attribute InstLevelAttribute on a Node n, use
 * ```
 * n.getAttribute(InstLevelAttribute());
 * ```
 *
 * To check whether the attribute has been set:
 * ```
 * n.hasAttribute(InstLevelAttribute());
 * ```
 *
 * To separate Attributes of the same type in the same table, each of the
 * structures `struct InstLevelAttributeId {};` is given a different unique
 * value at load time. An example is the empty struct InstLevelAttributeId.
 * These should be unique for each Attribute. Then via some template messiness
 * when InstLevelAttribute() is passed as the argument to getAttribute(...) the
 * load time id is instantiated.
 */
// ATTRIBUTE MANAGER ===========================================================

/**
 * A container for the main attribute tables of the system.  There's a
 * one-to-one NodeManager : AttributeManager correspondence.
 */
class AttributeManager {

  template <class T>
  void deleteFromTable(AttrHash<T>& table, NodeValue* nv);

  template <class T>
  void deleteAllFromTable(AttrHash<T>& table);

  template <class T>
  void deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids);

  template <class T>
  void reconstructTable(AttrHash<T>& table);

  /**
   * getTable<> is a helper template that gets the right table from an
   * AttributeManager given its type.
   */
  template <class T, class Enable>
  friend struct getTable;

  bool d_inGarbageCollection;

  void clearDeleteAllAttributesBuffer();

public:

  /** Construct an attribute manager. */
  AttributeManager();

  // IF YOU ADD ANY TABLES, don't forget to add them also to the
  // implementation of deleteAllAttributes().

  /** Underlying hash table for boolean-valued attributes */
  AttrHash<bool> d_bools;
  /** Underlying hash table for integral-valued attributes */
  AttrHash<uint64_t> d_ints;
  /** Underlying hash table for node-valued attributes */
  AttrHash<TNode> d_tnodes;
  /** Underlying hash table for node-valued attributes */
  AttrHash<Node> d_nodes;
  /** Underlying hash table for types attributes */
  AttrHash<TypeNode> d_types;
  /** Underlying hash table for string-valued attributes */
  AttrHash<std::string> d_strings;

  /**
   * Get a particular attribute on a particular node.
   *
   * @param nv the node about which to inquire
   * @param attr the attribute kind to get
   * @return the attribute value, if set, or a default-constructed
   * AttrKind::value_type if not.
   */
  template <class AttrKind>
  typename AttrKind::value_type getAttribute(NodeValue* nv,
                                             const AttrKind& attr) const;

  /**
   * Determine if a particular attribute exists for a particular node.
   *
   * @param nv the node about which to inquire
   * @param attr the attribute kind to inquire about
   * @return true if the given node has the given attribute
   */
  template <class AttrKind>
  bool hasAttribute(NodeValue* nv,
                    const AttrKind& attr) const;

  /**
   * Determine if a particular attribute exists for a particular node,
   * and get it if it does.
   *
   * @param nv the node about which to inquire
   * @param attr the attribute kind to inquire about
   * @param ret a pointer to a return value, set in case the node has
   * the attribute
   * @return true if the given node has the given attribute
   */
  template <class AttrKind>
  bool getAttribute(NodeValue* nv,
                    const AttrKind& attr,
                    typename AttrKind::value_type& ret) const;

  /**
   * Set a particular attribute on a particular node.
   *
   * @param nv the node for which to set the attribute
   * @param attr the attribute kind to set
   * @param value a pointer to a return value, set in case the node has
   * the attribute
   * @return true if the given node has the given attribute
   */
  template <class AttrKind>
  void setAttribute(NodeValue* nv,
                    const AttrKind& attr,
                    const typename AttrKind::value_type& value);

  /**
   * Remove all attributes associated to the given node.
   *
   * @param nv the node from which to delete attributes
   */
  void deleteAllAttributes(NodeValue* nv);

  /**
   * Remove all attributes from the tables.
   */
  void deleteAllAttributes();

  /**
   * Returns true if a table is currently being deleted.
   */
  bool inGarbageCollection() const ;

  /**
   * Determines the AttrTableId of an attribute.
   *
   * @param attr the attribute
   * @return the id of the attribute table.
   */
  template <class AttrKind>
  static AttributeUniqueId getAttributeId(const AttrKind& attr);

  /** A list of attributes. */
  typedef std::vector< const AttributeUniqueId* > AttrIdVec;

  /** Deletes a list of attributes. */
  void deleteAttributes(const AttrIdVec& attributeIds);

  /**
   * debugHook() is an empty function for the purpose of debugging
   * the AttributeManager without recompiling all of cvc5.
   * Formally this is a nop.
   */
  void debugHook(int debugFlag);
};

}  // namespace attr

// MAPPING OF ATTRIBUTE KINDS TO TABLES IN THE ATTRIBUTE MANAGER ===============

namespace attr {

/**
 * The getTable<> template provides (static) access to the
 * AttributeManager field holding the table.
 *
 * 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 getTable;

/** Access the "d_bools" member of AttributeManager. */
template <>
struct getTable<bool>
{
  static const AttrTableId id = AttrTableBool;
  typedef AttrHash<bool> table_type;
  static inline table_type& get(AttributeManager& am) {
    return am.d_bools;
  }
  static inline const table_type& get(const AttributeManager& am) {
    return am.d_bools;
  }
};

/** Access the "d_ints" member of AttributeManager. */
template <class T>
struct getTable<T,
                // Use this specialization only for unsigned integers
                typename std::enable_if<std::is_unsigned<T>::value>::type>
{
  static const AttrTableId id = AttrTableUInt64;
  typedef AttrHash<uint64_t> table_type;
  static inline table_type& get(AttributeManager& am) {
    return am.d_ints;
  }
  static inline const table_type& get(const AttributeManager& am) {
    return am.d_ints;
  }
};

/** Access the "d_tnodes" member of AttributeManager. */
template <>
struct getTable<TNode>
{
  static const AttrTableId id = AttrTableTNode;
  typedef AttrHash<TNode> table_type;
  static inline table_type& get(AttributeManager& am) {
    return am.d_tnodes;
  }
  static inline const table_type& get(const AttributeManager& am) {
    return am.d_tnodes;
  }
};

/** Access the "d_nodes" member of AttributeManager. */
template <>
struct getTable<Node>
{
  static const AttrTableId id = AttrTableNode;
  typedef AttrHash<Node> table_type;
  static inline table_type& get(AttributeManager& am) {
    return am.d_nodes;
  }
  static inline const table_type& get(const AttributeManager& am) {
    return am.d_nodes;
  }
};

/** Access the "d_types" member of AttributeManager. */
template <>
struct getTable<TypeNode>
{
  static const AttrTableId id = AttrTableTypeNode;
  typedef AttrHash<TypeNode> table_type;
  static inline table_type& get(AttributeManager& am) {
    return am.d_types;
  }
  static inline const table_type& get(const AttributeManager& am) {
    return am.d_types;
  }
};

/** Access the "d_strings" member of AttributeManager. */
template <>
struct getTable<std::string>
{
  static const AttrTableId id = AttrTableString;
  typedef AttrHash<std::string> table_type;
  static inline table_type& get(AttributeManager& am) {
    return am.d_strings;
  }
  static inline const table_type& get(const AttributeManager& am) {
    return am.d_strings;
  }
};

}  // namespace attr

// ATTRIBUTE MANAGER IMPLEMENTATIONS ===========================================

namespace attr {

// implementation for AttributeManager::getAttribute()
template <class AttrKind>
typename AttrKind::value_type
AttributeManager::getAttribute(NodeValue* nv, const AttrKind&) const {
  typedef typename AttrKind::value_type value_type;
  typedef KindValueToTableValueMapping<value_type> mapping;
  typedef typename getTable<value_type>::table_type table_type;

  const table_type& ah = getTable<value_type>::get(*this);
  typename table_type::const_iterator i =
    ah.find(std::make_pair(AttrKind::getId(), nv));

  if(i == ah.end()) {
    return typename AttrKind::value_type();
  }

  return mapping::convertBack((*i).second);
}

/* Helper template class for hasAttribute(), specialized based on
 * whether AttrKind has a "default value" that all Nodes implicitly
 * have or not. */
template <bool has_default, class AttrKind>
struct HasAttribute;

/**
 * Specialization of HasAttribute<> helper template for AttrKinds
 * with a default value.
 */
template <class AttrKind>
struct HasAttribute<true, AttrKind> {
  /** This implementation is simple; it's always true. */
  static inline bool hasAttribute(const AttributeManager* am,
                                  NodeValue* nv) {
    return true;
  }

  /**
   * This implementation returns the AttrKind's default value if the
   * Node doesn't have the given attribute.
   */
  static inline bool getAttribute(const AttributeManager* am,
                                  NodeValue* nv,
                                  typename AttrKind::value_type& ret) {
    typedef typename AttrKind::value_type value_type;
    typedef KindValueToTableValueMapping<value_type> mapping;
    typedef typename getTable<value_type>::table_type table_type;

    const table_type& ah = getTable<value_type>::get(*am);
    typename table_type::const_iterator i =
      ah.find(std::make_pair(AttrKind::getId(), nv));

    if(i == ah.end()) {
      ret = AttrKind::default_value;
    } else {
      ret = mapping::convertBack((*i).second);
    }

    return true;
  }
};

/**
 * Specialization of HasAttribute<> helper template for AttrKinds
 * without a default value.
 */
template <class AttrKind>
struct HasAttribute<false, AttrKind> {
  static inline bool hasAttribute(const AttributeManager* am,
                                  NodeValue* nv) {
    typedef typename AttrKind::value_type value_type;
    //typedef KindValueToTableValueMapping<value_type> mapping;
    typedef typename getTable<value_type>::table_type table_type;

    const table_type& ah = getTable<value_type>::get(*am);
    typename table_type::const_iterator i =
      ah.find(std::make_pair(AttrKind::getId(), nv));

    if(i == ah.end()) {
      return false;
    }

    return true;
  }

  static inline bool getAttribute(const AttributeManager* am,
                                  NodeValue* nv,
                                  typename AttrKind::value_type& ret) {
    typedef typename AttrKind::value_type value_type;
    typedef KindValueToTableValueMapping<value_type> mapping;
    typedef typename getTable<value_type>::table_type table_type;

    const table_type& ah = getTable<value_type>::get(*am);
    typename table_type::const_iterator i =
      ah.find(std::make_pair(AttrKind::getId(), nv));

    if(i == ah.end()) {
      return false;
    }

    ret = mapping::convertBack((*i).second);

    return true;
  }
};

template <class AttrKind>
bool AttributeManager::hasAttribute(NodeValue* nv,
                                    const AttrKind&) const {
  return HasAttribute<AttrKind::has_default_value, AttrKind>::
           hasAttribute(this, nv);
}

template <class AttrKind>
bool AttributeManager::getAttribute(NodeValue* nv,
                                    const AttrKind&,
                                    typename AttrKind::value_type& ret) const {
  return HasAttribute<AttrKind::has_default_value, AttrKind>::
           getAttribute(this, nv, ret);
}

template <class AttrKind>
inline void
AttributeManager::setAttribute(NodeValue* nv,
                               const AttrKind&,
                               const typename AttrKind::value_type& value) {
  typedef typename AttrKind::value_type value_type;
  typedef KindValueToTableValueMapping<value_type> mapping;
  typedef typename getTable<value_type>::table_type table_type;

  table_type& ah = getTable<value_type>::get(*this);
  ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value);
}

/** Search for the NodeValue in all attribute tables and remove it. */
template <class T>
inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
                                              NodeValue* nv) {
  // This cannot use nv as anything other than a pointer!
  const uint64_t last = attr::LastAttributeId<T>::getId();
  for (uint64_t id = 0; id < last; ++id)
  {
    table.erase(std::make_pair(id, nv));
  }
}

/** Remove all attributes from the table. */
template <class T>
inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
  Assert(!d_inGarbageCollection);
  d_inGarbageCollection = true;
  table.clear();
  d_inGarbageCollection = false;
  Assert(!d_inGarbageCollection);
}

template <class AttrKind>
AttributeUniqueId AttributeManager::getAttributeId(const AttrKind& attr){
  typedef typename AttrKind::value_type value_type;
  AttrTableId tableId = getTable<value_type>::id;
  return AttributeUniqueId(tableId, attr.getId());
}

template <class T>
void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids){
  d_inGarbageCollection = true;
  typedef AttrHash<T> hash_t;

  typename hash_t::iterator it = table.begin();
  typename hash_t::iterator tmp;
  typename hash_t::iterator it_end = table.end();

  std::vector<uint64_t>::const_iterator begin_ids = ids.begin();
  std::vector<uint64_t>::const_iterator end_ids = ids.end();

  size_t initialSize = table.size();
  while (it != it_end){
    uint64_t id = (*it).first.first;

    if(std::binary_search(begin_ids, end_ids, id)){
      tmp = it;
      ++it;
      table.erase(tmp);
    }else{
      ++it;
    }
  }
  d_inGarbageCollection = false;
  static const size_t ReconstructShrinkRatio = 8;
  if(initialSize/ReconstructShrinkRatio > table.size()){
    reconstructTable(table);
  }
}

template <class T>
void AttributeManager::reconstructTable(AttrHash<T>& table){
  d_inGarbageCollection = true;
  typedef AttrHash<T> hash_t;
  hash_t cpy;
  cpy.insert(table.begin(), table.end());
  cpy.swap(table);
  d_inGarbageCollection = false;
}

}  // namespace attr
}  // namespace expr

template <class AttrKind>
inline typename AttrKind::value_type
NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&) const {
  return d_attrManager->getAttribute(nv, AttrKind());
}

template <class AttrKind>
inline bool NodeManager::hasAttribute(expr::NodeValue* nv,
                                      const AttrKind&) const {
  return d_attrManager->hasAttribute(nv, AttrKind());
}

template <class AttrKind>
inline bool
NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&,
                          typename AttrKind::value_type& ret) const {
  return d_attrManager->getAttribute(nv, AttrKind(), ret);
}

template <class AttrKind>
inline void
NodeManager::setAttribute(expr::NodeValue* nv, const AttrKind&,
                          const typename AttrKind::value_type& value) {
  d_attrManager->setAttribute(nv, AttrKind(), value);
}

template <class AttrKind>
inline typename AttrKind::value_type
NodeManager::getAttribute(TNode n, const AttrKind&) const {
  return d_attrManager->getAttribute(n.d_nv, AttrKind());
}

template <class AttrKind>
inline bool
NodeManager::hasAttribute(TNode n, const AttrKind&) const {
  return d_attrManager->hasAttribute(n.d_nv, AttrKind());
}

template <class AttrKind>
inline bool
NodeManager::getAttribute(TNode n, const AttrKind&,
                          typename AttrKind::value_type& ret) const {
  return d_attrManager->getAttribute(n.d_nv, AttrKind(), ret);
}

template <class AttrKind>
inline void
NodeManager::setAttribute(TNode n, const AttrKind&,
                          const typename AttrKind::value_type& value) {
  d_attrManager->setAttribute(n.d_nv, AttrKind(), value);
}

template <class AttrKind>
inline typename AttrKind::value_type
NodeManager::getAttribute(TypeNode n, const AttrKind&) const {
  return d_attrManager->getAttribute(n.d_nv, AttrKind());
}

template <class AttrKind>
inline bool
NodeManager::hasAttribute(TypeNode n, const AttrKind&) const {
  return d_attrManager->hasAttribute(n.d_nv, AttrKind());
}

template <class AttrKind>
inline bool
NodeManager::getAttribute(TypeNode n, const AttrKind&,
                          typename AttrKind::value_type& ret) const {
  return d_attrManager->getAttribute(n.d_nv, AttrKind(), ret);
}

template <class AttrKind>
inline void
NodeManager::setAttribute(TypeNode n, const AttrKind&,
                          const typename AttrKind::value_type& value) {
  d_attrManager->setAttribute(n.d_nv, AttrKind(), value);
}

}  // namespace cvc5

#endif /* CVC5__EXPR__ATTRIBUTE_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters, Tim King, 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		* Node attributes.
14		*/
15
16		#include "cvc5_private.h"
17
18		/* There are strong constraints on ordering of declarations of
19		* attributes and nodes due to template use */
20		#include "expr/node.h"
21		#include "expr/type_node.h"
22
23		#ifndef CVC5__EXPR__ATTRIBUTE_H
24		#define CVC5__EXPR__ATTRIBUTE_H
25
26		#include <string>
27		#include "expr/attribute_unique_id.h"
28
29		// include supporting templates
30		#define CVC5_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
31		#include "expr/attribute_internals.h"
32		#undef CVC5_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
33
34		namespace cvc5 {
35		namespace expr {
36		namespace attr {
37
38		/**
39		* Attributes are roughly speaking [almost] global hash tables from Nodes
40		* (TNodes) to data. Attributes can be thought of as additional fields used to
41		* extend NodeValues. Attributes are mutable. Attributes live only as long as
42		* the node itself does. If a Node is garbage-collected, Attributes associated
43		* with it will automatically be garbage collected. (Being in the domain of an
44		* Attribute does not increase a Node's reference count.) To achieve this
45		* special relationship with Nodes, Attributes are mapped by hash tables
46		* (AttrHash<>) that live in the AttributeManager. The AttributeManager is
47		* owned by the NodeManager.
48		*
49		* Example:
50		*
51		* Attributes tend to be defined in a fixed pattern:
52		*
53		* ```
54		* struct InstLevelAttributeId {};
55		* typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
56		* ```
57		*
58		* To get the value of an Attribute InstLevelAttribute on a Node n, use
59		* ```
60		* n.getAttribute(InstLevelAttribute());
61		* ```
62		*
63		* To check whether the attribute has been set:
64		* ```
65		* n.hasAttribute(InstLevelAttribute());
66		* ```
67		*
68		* To separate Attributes of the same type in the same table, each of the
69		* structures `struct InstLevelAttributeId {};` is given a different unique
70		* value at load time. An example is the empty struct InstLevelAttributeId.
71		* These should be unique for each Attribute. Then via some template messiness
72		* when InstLevelAttribute() is passed as the argument to getAttribute(...) the
73		* load time id is instantiated.
74		*/
75		// ATTRIBUTE MANAGER ===========================================================
76
77		/**
78		* A container for the main attribute tables of the system. There's a
79		* one-to-one NodeManager : AttributeManager correspondence.
80		*/
81	8003	class AttributeManager {
82
83		template <class T>
84		void deleteFromTable(AttrHash<T>& table, NodeValue* nv);
85
86		template <class T>
87		void deleteAllFromTable(AttrHash<T>& table);
88
89		template <class T>
90		void deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids);
91
92		template <class T>
93		void reconstructTable(AttrHash<T>& table);
94
95		/**
96		* getTable<> is a helper template that gets the right table from an
97		* AttributeManager given its type.
98		*/
99		template <class T, class Enable>
100		friend struct getTable;
101
102		bool d_inGarbageCollection;
103
104		void clearDeleteAllAttributesBuffer();
105
106		public:
107
108		/** Construct an attribute manager. */
109		AttributeManager();
110
111		// IF YOU ADD ANY TABLES, don't forget to add them also to the
112		// implementation of deleteAllAttributes().
113
114		/** Underlying hash table for boolean-valued attributes */
115		AttrHash<bool> d_bools;
116		/** Underlying hash table for integral-valued attributes */
117		AttrHash<uint64_t> d_ints;
118		/** Underlying hash table for node-valued attributes */
119		AttrHash<TNode> d_tnodes;
120		/** Underlying hash table for node-valued attributes */
121		AttrHash<Node> d_nodes;
122		/** Underlying hash table for types attributes */
123		AttrHash<TypeNode> d_types;
124		/** Underlying hash table for string-valued attributes */
125		AttrHash<std::string> d_strings;
126
127		/**
128		* Get a particular attribute on a particular node.
129		*
130		* @param nv the node about which to inquire
131		* @param attr the attribute kind to get
132		* @return the attribute value, if set, or a default-constructed
133		* AttrKind::value_type if not.
134		*/
135		template <class AttrKind>
136		typename AttrKind::value_type getAttribute(NodeValue* nv,
137		const AttrKind& attr) const;
138
139		/**
140		* Determine if a particular attribute exists for a particular node.
141		*
142		* @param nv the node about which to inquire
143		* @param attr the attribute kind to inquire about
144		* @return true if the given node has the given attribute
145		*/
146		template <class AttrKind>
147		bool hasAttribute(NodeValue* nv,
148		const AttrKind& attr) const;
149
150		/**
151		* Determine if a particular attribute exists for a particular node,
152		* and get it if it does.
153		*
154		* @param nv the node about which to inquire
155		* @param attr the attribute kind to inquire about
156		* @param ret a pointer to a return value, set in case the node has
157		* the attribute
158		* @return true if the given node has the given attribute
159		*/
160		template <class AttrKind>
161		bool getAttribute(NodeValue* nv,
162		const AttrKind& attr,
163		typename AttrKind::value_type& ret) const;
164
165		/**
166		* Set a particular attribute on a particular node.
167		*
168		* @param nv the node for which to set the attribute
169		* @param attr the attribute kind to set
170		* @param value a pointer to a return value, set in case the node has
171		* the attribute
172		* @return true if the given node has the given attribute
173		*/
174		template <class AttrKind>
175		void setAttribute(NodeValue* nv,
176		const AttrKind& attr,
177		const typename AttrKind::value_type& value);
178
179		/**
180		* Remove all attributes associated to the given node.
181		*
182		* @param nv the node from which to delete attributes
183		*/
184		void deleteAllAttributes(NodeValue* nv);
185
186		/**
187		* Remove all attributes from the tables.
188		*/
189		void deleteAllAttributes();
190
191		/**
192		* Returns true if a table is currently being deleted.
193		*/
194		bool inGarbageCollection() const ;
195
196		/**
197		* Determines the AttrTableId of an attribute.
198		*
199		* @param attr the attribute
200		* @return the id of the attribute table.
201		*/
202		template <class AttrKind>
203		static AttributeUniqueId getAttributeId(const AttrKind& attr);
204
205		/** A list of attributes. */
206		typedef std::vector< const AttributeUniqueId* > AttrIdVec;
207
208		/** Deletes a list of attributes. */
209		void deleteAttributes(const AttrIdVec& attributeIds);
210
211		/**
212		* debugHook() is an empty function for the purpose of debugging
213		* the AttributeManager without recompiling all of cvc5.
214		* Formally this is a nop.
215		*/
216		void debugHook(int debugFlag);
217		};
218
219		} // namespace attr
220
221		// MAPPING OF ATTRIBUTE KINDS TO TABLES IN THE ATTRIBUTE MANAGER ===============
222
223		namespace attr {
224
225		/**
226		* The getTable<> template provides (static) access to the
227		* AttributeManager field holding the table.
228		*
229		* The `Enable` template parameter is used to instantiate the template
230		* conditionally: If the template substitution of Enable fails (e.g. when using
231		* `std::enable_if` in the template parameter and the condition is false), the
232		* instantiation is ignored due to the SFINAE rule.
233		*/
234		template <class T, class Enable = void>
235		struct getTable;
236
237		/** Access the "d_bools" member of AttributeManager. */
238		template <>
239		struct getTable<bool>
240		{
241		static const AttrTableId id = AttrTableBool;
242		typedef AttrHash<bool> table_type;
243	47986288	static inline table_type& get(AttributeManager& am) {
244	47986288	return am.d_bools;
245		}
246	814961651	static inline const table_type& get(const AttributeManager& am) {
247	814961651	return am.d_bools;
248		}
249		};
250
251		/** Access the "d_ints" member of AttributeManager. */
252		template <class T>
253		struct getTable<T,
254		// Use this specialization only for unsigned integers
255		typename std::enable_if<std::is_unsigned<T>::value>::type>
256		{
257		static const AttrTableId id = AttrTableUInt64;
258		typedef AttrHash<uint64_t> table_type;
259	208520	static inline table_type& get(AttributeManager& am) {
260	208520	return am.d_ints;
261		}
262	22610241	static inline const table_type& get(const AttributeManager& am) {
263	22610241	return am.d_ints;
264		}
265		};
266
267		/** Access the "d_tnodes" member of AttributeManager. */
268		template <>
269		struct getTable<TNode>
270		{
271		static const AttrTableId id = AttrTableTNode;
272		typedef AttrHash<TNode> table_type;
273	2	static inline table_type& get(AttributeManager& am) {
274	2	return am.d_tnodes;
275		}
276	4	static inline const table_type& get(const AttributeManager& am) {
277	4	return am.d_tnodes;
278		}
279		};
280
281		/** Access the "d_nodes" member of AttributeManager. */
282		template <>
283		struct getTable<Node>
284		{
285		static const AttrTableId id = AttrTableNode;
286		typedef AttrHash<Node> table_type;
287	25200512	static inline table_type& get(AttributeManager& am) {
288	25200512	return am.d_nodes;
289		}
290	268941410	static inline const table_type& get(const AttributeManager& am) {
291	268941410	return am.d_nodes;
292		}
293		};
294
295		/** Access the "d_types" member of AttributeManager. */
296		template <>
297		struct getTable<TypeNode>
298		{
299		static const AttrTableId id = AttrTableTypeNode;
300		typedef AttrHash<TypeNode> table_type;
301	29025774	static inline table_type& get(AttributeManager& am) {
302	29025774	return am.d_types;
303		}
304	1525275391	static inline const table_type& get(const AttributeManager& am) {
305	1525275391	return am.d_types;
306		}
307		};
308
309		/** Access the "d_strings" member of AttributeManager. */
310		template <>
311		struct getTable<std::string>
312		{
313		static const AttrTableId id = AttrTableString;
314		typedef AttrHash<std::string> table_type;
315	1040412	static inline table_type& get(AttributeManager& am) {
316	1040412	return am.d_strings;
317		}
318	1246293	static inline const table_type& get(const AttributeManager& am) {
319	1246293	return am.d_strings;
320		}
321		};
322
323		} // namespace attr
324
325		// ATTRIBUTE MANAGER IMPLEMENTATIONS ===========================================
326
327		namespace attr {
328
329		// implementation for AttributeManager::getAttribute()
330		template <class AttrKind>
331		typename AttrKind::value_type
332	840702824	AttributeManager::getAttribute(NodeValue* nv, const AttrKind&) const {
333		typedef typename AttrKind::value_type value_type;
334		typedef KindValueToTableValueMapping<value_type> mapping;
335		typedef typename getTable<value_type>::table_type table_type;
336
337	840702824	const table_type& ah = getTable<value_type>::get(*this);
338	866444041	typename table_type::const_iterator i =
339	1681405648	ah.find(std::make_pair(AttrKind::getId(), nv));
340
341	840702824	if(i == ah.end()) {
342	27937547	return typename AttrKind::value_type();
343		}
344
345	812765277	return mapping::convertBack((*i).second);
346		}
347
348		/* Helper template class for hasAttribute(), specialized based on
349		* whether AttrKind has a "default value" that all Nodes implicitly
350		* have or not. */
351		template <bool has_default, class AttrKind>
352		struct HasAttribute;
353
354		/**
355		* Specialization of HasAttribute<> helper template for AttrKinds
356		* with a default value.
357		*/
358		template <class AttrKind>
359		struct HasAttribute<true, AttrKind> {
360		/** This implementation is simple; it's always true. */
361	40	static inline bool hasAttribute(const AttributeManager* am,
362		NodeValue* nv) {
363	40	return true;
364		}
365
366		/**
367		* This implementation returns the AttrKind's default value if the
368		* Node doesn't have the given attribute.
369		*/
370	44	static inline bool getAttribute(const AttributeManager* am,
371		NodeValue* nv,
372		typename AttrKind::value_type& ret) {
373		typedef typename AttrKind::value_type value_type;
374		typedef KindValueToTableValueMapping<value_type> mapping;
375		typedef typename getTable<value_type>::table_type table_type;
376
377	44	const table_type& ah = getTable<value_type>::get(*am);
378	44	typename table_type::const_iterator i =
379	88	ah.find(std::make_pair(AttrKind::getId(), nv));
380
381	44	if(i == ah.end()) {
382		ret = AttrKind::default_value;
383		} else {
384	44	ret = mapping::convertBack((*i).second);
385		}
386
387	44	return true;
388		}
389		};
390
391		/**
392		* Specialization of HasAttribute<> helper template for AttrKinds
393		* without a default value.
394		*/
395		template <class AttrKind>
396		struct HasAttribute<false, AttrKind> {
397	940403473	static inline bool hasAttribute(const AttributeManager* am,
398		NodeValue* nv) {
399		typedef typename AttrKind::value_type value_type;
400		//typedef KindValueToTableValueMapping<value_type> mapping;
401		typedef typename getTable<value_type>::table_type table_type;
402
403	940403473	const table_type& ah = getTable<value_type>::get(*am);
404	1880806946	typename table_type::const_iterator i =
405	1880806946	ah.find(std::make_pair(AttrKind::getId(), nv));
406
407	940403473	if(i == ah.end()) {
408	64969236	return false;
409		}
410
411	875434237	return true;
412		}
413
414	851928649	static inline bool getAttribute(const AttributeManager* am,
415		NodeValue* nv,
416		typename AttrKind::value_type& ret) {
417		typedef typename AttrKind::value_type value_type;
418		typedef KindValueToTableValueMapping<value_type> mapping;
419		typedef typename getTable<value_type>::table_type table_type;
420
421	851928649	const table_type& ah = getTable<value_type>::get(*am);
422	1703857298	typename table_type::const_iterator i =
423	1703857298	ah.find(std::make_pair(AttrKind::getId(), nv));
424
425	851928649	if(i == ah.end()) {
426	27878089	return false;
427		}
428
429	824050560	ret = mapping::convertBack((*i).second);
430
431	824050560	return true;
432		}
433		};
434
435		template <class AttrKind>
436	940403513	bool AttributeManager::hasAttribute(NodeValue* nv,
437		const AttrKind&) const {
438		return HasAttribute<AttrKind::has_default_value, AttrKind>::
439	940403513	hasAttribute(this, nv);
440		}
441
442		template <class AttrKind>
443	851928693	bool AttributeManager::getAttribute(NodeValue* nv,
444		const AttrKind&,
445		typename AttrKind::value_type& ret) const {
446		return HasAttribute<AttrKind::has_default_value, AttrKind>::
447	851928693	getAttribute(this, nv, ret);
448		}
449
450		template <class AttrKind>
451		inline void
452	103461508	AttributeManager::setAttribute(NodeValue* nv,
453		const AttrKind&,
454		const typename AttrKind::value_type& value) {
455		typedef typename AttrKind::value_type value_type;
456		typedef KindValueToTableValueMapping<value_type> mapping;
457		typedef typename getTable<value_type>::table_type table_type;
458
459	103461508	table_type& ah = getTable<value_type>::get(*this);
460	103461508	ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value);
461	103461508	}
462
463		/** Search for the NodeValue in all attribute tables and remove it. */
464		template <class T>
465	157154390	inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
466		NodeValue* nv) {
467		// This cannot use nv as anything other than a pointer!
468	157154390	const uint64_t last = attr::LastAttributeId<T>::getId();
469	2640202662	for (uint64_t id = 0; id < last; ++id)
470		{
471	4966096544	table.erase(std::make_pair(id, nv));
472		}
473	157154390	}
474
475		/** Remove all attributes from the table. */
476		template <class T>
477	40015	inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
478	40015	Assert(!d_inGarbageCollection);
479	40015	d_inGarbageCollection = true;
480	40015	table.clear();
481	40015	d_inGarbageCollection = false;
482	40015	Assert(!d_inGarbageCollection);
483	40015	}
484
485		template <class AttrKind>
486		AttributeUniqueId AttributeManager::getAttributeId(const AttrKind& attr){
487		typedef typename AttrKind::value_type value_type;
488		AttrTableId tableId = getTable<value_type>::id;
489		return AttributeUniqueId(tableId, attr.getId());
490		}
491
492		template <class T>
493		void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids){
494		d_inGarbageCollection = true;
495		typedef AttrHash<T> hash_t;
496
497		typename hash_t::iterator it = table.begin();
498		typename hash_t::iterator tmp;
499		typename hash_t::iterator it_end = table.end();
500
501		std::vector<uint64_t>::const_iterator begin_ids = ids.begin();
502		std::vector<uint64_t>::const_iterator end_ids = ids.end();
503
504		size_t initialSize = table.size();
505		while (it != it_end){
506		uint64_t id = (*it).first.first;
507
508		if(std::binary_search(begin_ids, end_ids, id)){
509		tmp = it;
510		++it;
511		table.erase(tmp);
512		}else{
513		++it;
514		}
515		}
516		d_inGarbageCollection = false;
517		static const size_t ReconstructShrinkRatio = 8;
518		if(initialSize/ReconstructShrinkRatio > table.size()){
519		reconstructTable(table);
520		}
521		}
522
523		template <class T>
524		void AttributeManager::reconstructTable(AttrHash<T>& table){
525		d_inGarbageCollection = true;
526		typedef AttrHash<T> hash_t;
527		hash_t cpy;
528		cpy.insert(table.begin(), table.end());
529		cpy.swap(table);
530		d_inGarbageCollection = false;
531		}
532
533		} // namespace attr
534		} // namespace expr
535
536		template <class AttrKind>
537		inline typename AttrKind::value_type
538	7744745	NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&) const {
539	7744745	return d_attrManager->getAttribute(nv, AttrKind());
540		}
541
542		template <class AttrKind>
543	8232792	inline bool NodeManager::hasAttribute(expr::NodeValue* nv,
544		const AttrKind&) const {
545	8232792	return d_attrManager->hasAttribute(nv, AttrKind());
546		}
547
548		template <class AttrKind>
549		inline bool
550		NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&,
551		typename AttrKind::value_type& ret) const {
552		return d_attrManager->getAttribute(nv, AttrKind(), ret);
553		}
554
555		template <class AttrKind>
556		inline void
557	26043	NodeManager::setAttribute(expr::NodeValue* nv, const AttrKind&,
558		const typename AttrKind::value_type& value) {
559	26043	d_attrManager->setAttribute(nv, AttrKind(), value);
560	26043	}
561
562		template <class AttrKind>
563		inline typename AttrKind::value_type
564	832958079	NodeManager::getAttribute(TNode n, const AttrKind&) const {
565	832958079	return d_attrManager->getAttribute(n.d_nv, AttrKind());
566		}
567
568		template <class AttrKind>
569		inline bool
570	932170721	NodeManager::hasAttribute(TNode n, const AttrKind&) const {
571	932170721	return d_attrManager->hasAttribute(n.d_nv, AttrKind());
572		}
573
574		template <class AttrKind>
575		inline bool
576	851928693	NodeManager::getAttribute(TNode n, const AttrKind&,
577		typename AttrKind::value_type& ret) const {
578	851928693	return d_attrManager->getAttribute(n.d_nv, AttrKind(), ret);
579		}
580
581		template <class AttrKind>
582		inline void
583	103426912	NodeManager::setAttribute(TNode n, const AttrKind&,
584		const typename AttrKind::value_type& value) {
585	103426912	d_attrManager->setAttribute(n.d_nv, AttrKind(), value);
586	103426912	}
587
588		template <class AttrKind>
589		inline typename AttrKind::value_type
590		NodeManager::getAttribute(TypeNode n, const AttrKind&) const {
591		return d_attrManager->getAttribute(n.d_nv, AttrKind());
592		}
593
594		template <class AttrKind>
595		inline bool
596		NodeManager::hasAttribute(TypeNode n, const AttrKind&) const {
597		return d_attrManager->hasAttribute(n.d_nv, AttrKind());
598		}
599
600		template <class AttrKind>
601		inline bool
602		NodeManager::getAttribute(TypeNode n, const AttrKind&,
603		typename AttrKind::value_type& ret) const {
604		return d_attrManager->getAttribute(n.d_nv, AttrKind(), ret);
605		}
606
607		template <class AttrKind>
608		inline void
609	8553	NodeManager::setAttribute(TypeNode n, const AttrKind&,
610		const typename AttrKind::value_type& value) {
611	8553	d_attrManager->setAttribute(n.d_nv, AttrKind(), value);
612	8553	}
613
614		} // namespace cvc5
615
616		#endif /* CVC5__EXPR__ATTRIBUTE_H */