Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/attribute.h	Lines:	95	125	76.0 %
Date:	2021-05-24	Branches:	555	1196	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 and come in both sat
 * context-dependent and non-context dependent varieties. 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<> and CDAttrHash<>) 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, bool context_dep, 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, bool context_dep, class Enable = void>
struct getTable;

/** Access the "d_bools" member of AttributeManager. */
template <>
struct getTable<bool, false> {
  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,
                false,
                // 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, false> {
  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, false> {
  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, false> {
  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, false> {
  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, AttrKind::context_dependent>::
            table_type table_type;

  const table_type& ah =
    getTable<value_type, AttrKind::context_dependent>::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,
                              AttrKind::context_dependent>::table_type
      table_type;

    const table_type& ah =
      getTable<value_type, AttrKind::context_dependent>::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, AttrKind::context_dependent>::
              table_type table_type;

    const table_type& ah =
      getTable<value_type, AttrKind::context_dependent>::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, AttrKind::context_dependent>::
              table_type table_type;

    const table_type& ah =
      getTable<value_type, AttrKind::context_dependent>::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, AttrKind::context_dependent>::
            table_type table_type;

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