[Attributes] Remove parameter `context_dependent` (#6772)

After commit d70a63324c95210f1d78c2efc46395d2369d2e2b, context-dependent
attributes have not been supported and, as a result, the template
parameter `context_dependent` of `Attribute` has not been used.
Context-dependent attributes also do not fit with our current design of
sharing attributes across different solvers, so it is unlikely that we
will add that feature back in the future. This commit removes the unused
template parameter.

diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index b58cd45a95fa78840e763fbca5d597d938ca00a5..e41b63191b4c59521be823b5e438463233c7d221 100644 (file)
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -38,14 +38,13 @@ 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.
+ * 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:
  *
@@ -67,11 +66,11 @@ namespace attr {
  * ```
  *
  * 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.
+ * 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 ===========================================================
 
@@ -97,7 +96,7 @@ class AttributeManager {
    * getTable<> is a helper template that gets the right table from an
    * AttributeManager given its type.
    */
-  template <class T, bool context_dep, class Enable>
+  template <class T, class Enable>
   friend struct getTable;
 
   bool d_inGarbageCollection;
@@ -232,12 +231,13 @@ namespace attr {
  * `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>
+template <class T, class Enable = void>
 struct getTable;
 
 /** Access the "d_bools" member of AttributeManager. */
 template <>
-struct getTable<bool, false> {
+struct getTable<bool>
+{
   static const AttrTableId id = AttrTableBool;
   typedef AttrHash<bool> table_type;
   static inline table_type& get(AttributeManager& am) {
@@ -251,7 +251,6 @@ struct getTable<bool, false> {
 /** 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>
 {
@@ -267,7 +266,8 @@ struct getTable<T,
 
 /** Access the "d_tnodes" member of AttributeManager. */
 template <>
-struct getTable<TNode, false> {
+struct getTable<TNode>
+{
   static const AttrTableId id = AttrTableTNode;
   typedef AttrHash<TNode> table_type;
   static inline table_type& get(AttributeManager& am) {
@@ -280,7 +280,8 @@ struct getTable<TNode, false> {
 
 /** Access the "d_nodes" member of AttributeManager. */
 template <>
-struct getTable<Node, false> {
+struct getTable<Node>
+{
   static const AttrTableId id = AttrTableNode;
   typedef AttrHash<Node> table_type;
   static inline table_type& get(AttributeManager& am) {
@@ -293,7 +294,8 @@ struct getTable<Node, false> {
 
 /** Access the "d_types" member of AttributeManager. */
 template <>
-struct getTable<TypeNode, false> {
+struct getTable<TypeNode>
+{
   static const AttrTableId id = AttrTableTypeNode;
   typedef AttrHash<TypeNode> table_type;
   static inline table_type& get(AttributeManager& am) {
@@ -306,7 +308,8 @@ struct getTable<TypeNode, false> {
 
 /** Access the "d_strings" member of AttributeManager. */
 template <>
-struct getTable<std::string, false> {
+struct getTable<std::string>
+{
   static const AttrTableId id = AttrTableString;
   typedef AttrHash<std::string> table_type;
   static inline table_type& get(AttributeManager& am) {
@@ -329,11 +332,9 @@ 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;
+  typedef typename getTable<value_type>::table_type table_type;
 
-  const table_type& ah =
-    getTable<value_type, AttrKind::context_dependent>::get(*this);
+  const table_type& ah = getTable<value_type>::get(*this);
   typename table_type::const_iterator i =
     ah.find(std::make_pair(AttrKind::getId(), nv));
 
@@ -371,12 +372,9 @@ struct HasAttribute<true, AttrKind> {
                                   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;
+    typedef typename getTable<value_type>::table_type table_type;
 
-    const table_type& ah =
-      getTable<value_type, AttrKind::context_dependent>::get(*am);
+    const table_type& ah = getTable<value_type>::get(*am);
     typename table_type::const_iterator i =
       ah.find(std::make_pair(AttrKind::getId(), nv));
 
@@ -400,11 +398,9 @@ struct HasAttribute<false, AttrKind> {
                                   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;
+    typedef typename getTable<value_type>::table_type table_type;
 
-    const table_type& ah =
-      getTable<value_type, AttrKind::context_dependent>::get(*am);
+    const table_type& ah = getTable<value_type>::get(*am);
     typename table_type::const_iterator i =
       ah.find(std::make_pair(AttrKind::getId(), nv));
 
@@ -420,11 +416,9 @@ struct HasAttribute<false, AttrKind> {
                                   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;
+    typedef typename getTable<value_type>::table_type table_type;
 
-    const table_type& ah =
-      getTable<value_type, AttrKind::context_dependent>::get(*am);
+    const table_type& ah = getTable<value_type>::get(*am);
     typename table_type::const_iterator i =
       ah.find(std::make_pair(AttrKind::getId(), nv));
 
@@ -460,11 +454,9 @@ AttributeManager::setAttribute(NodeValue* nv,
                                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;
+  typedef typename getTable<value_type>::table_type table_type;
 
-  table_type& ah =
-      getTable<value_type, AttrKind::context_dependent>::get(*this);
+  table_type& ah = getTable<value_type>::get(*this);
   ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value);
 }
 
@@ -473,7 +465,7 @@ 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();
+  const uint64_t last = attr::LastAttributeId<T>::getId();
   for (uint64_t id = 0; id < last; ++id)
   {
     table.erase(std::make_pair(id, nv));
@@ -493,8 +485,7 @@ inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
 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;
+  AttrTableId tableId = getTable<value_type>::id;
   return AttributeUniqueId(tableId, attr.getId());
 }
 

diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index c82e62836accb80ba1aff3473fad2ab541dde195..2ae216d3ced8bbb18e8be1f74caea40505a5a078 100644 (file)
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -372,8 +372,9 @@ 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 {
+template <class T>
+struct LastAttributeId
+{
  public:
   static uint64_t getNextId() {
     uint64_t* id = raw_id();
@@ -402,11 +403,8 @@ struct LastAttributeId {
  * @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>
+template <class T, class value_t>
 class Attribute
 {
   /**
@@ -431,11 +429,6 @@ public:
    */
   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
@@ -444,15 +437,15 @@ public:
   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();
+    return attr::LastAttributeId<table_value_type>::getNextId();
   }
 };/* class Attribute<> */
 
 /**
  * An "attribute type" structure for boolean flags (special).
  */
-template <class T, bool context_dep>
-class Attribute<T, bool, context_dep>
+template <class T>
+class Attribute<T, bool>
 {
   /** IDs for bool-valued attributes are actually bit assignments. */
   static const uint64_t s_id;
@@ -479,18 +472,13 @@ public:
    */
   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();
+    const uint64_t id = attr::LastAttributeId<bool>::getNextId();
     AlwaysAssert(id <= 63) << "Too many boolean node attributes registered "
                               "during initialization !";
     return id;
@@ -500,15 +488,14 @@ public:
 // 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();
-
+template <class T, class value_t>
+const uint64_t Attribute<T, value_t>::s_id =
+    Attribute<T, value_t>::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();
+template <class T>
+const uint64_t Attribute<T, bool>::s_id =
+    Attribute<T, bool>::registerAttribute();
 
 }  // namespace expr
 }  // namespace cvc5

diff --git a/test/unit/node/attribute_white.cpp b/test/unit/node/attribute_white.cpp
index fe74130d14024c3f51166a1671429c6ce69f4ff2..4b0f1892fe9d9df2b2b92877aa2db939cc93b02f 100644 (file)
--- a/test/unit/node/attribute_white.cpp
+++ b/test/unit/node/attribute_white.cpp
@@ -78,7 +78,7 @@ TEST_F(TestNodeWhiteAttribute, attribute_ids)
   // and that the next ID to be assigned is strictly greater than
   // those that have already been assigned.
 
-  unsigned lastId = attr::LastAttributeId<std::string, false>::getId();
+  unsigned lastId = attr::LastAttributeId<std::string>::getId();
   ASSERT_LT(VarNameAttr::s_id, lastId);
   ASSERT_LT(TestStringAttr1::s_id, lastId);
   ASSERT_LT(TestStringAttr2::s_id, lastId);
@@ -87,7 +87,7 @@ TEST_F(TestNodeWhiteAttribute, attribute_ids)
   ASSERT_NE(VarNameAttr::s_id, TestStringAttr2::s_id);
   ASSERT_NE(TestStringAttr1::s_id, TestStringAttr2::s_id);
 
-  lastId = attr::LastAttributeId<bool, false>::getId();
+  lastId = attr::LastAttributeId<bool>::getId();
   ASSERT_LT(TestFlag1::s_id, lastId);
   ASSERT_LT(TestFlag2::s_id, lastId);
   ASSERT_LT(TestFlag3::s_id, lastId);
@@ -104,7 +104,7 @@ TEST_F(TestNodeWhiteAttribute, attribute_ids)
   ASSERT_NE(TestFlag3::s_id, TestFlag5::s_id);
   ASSERT_NE(TestFlag4::s_id, TestFlag5::s_id);
 
-  lastId = attr::LastAttributeId<TypeNode, false>::getId();
+  lastId = attr::LastAttributeId<TypeNode>::getId();
   ASSERT_LT(TypeAttr::s_id, lastId);
 }