From b1db68565a42bc22744cf38e95da6cbe8368c19b Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 21 Jun 2021 12:41:00 -0700 Subject: [PATCH] [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. --- src/expr/attribute.h | 81 +++++++++++++----------------- src/expr/attribute_internals.h | 41 ++++++--------- test/unit/node/attribute_white.cpp | 6 +-- 3 files changed, 53 insertions(+), 75 deletions(-) diff --git a/src/expr/attribute.h b/src/expr/attribute.h index b58cd45a9..e41b63191 100644 --- 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 + template 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 +template struct getTable; /** Access the "d_bools" member of AttributeManager. */ template <> -struct getTable { +struct getTable +{ static const AttrTableId id = AttrTableBool; typedef AttrHash table_type; static inline table_type& get(AttributeManager& am) { @@ -251,7 +251,6 @@ struct getTable { /** Access the "d_ints" member of AttributeManager. */ template struct getTable::value>::type> { @@ -267,7 +266,8 @@ struct getTable -struct getTable { +struct getTable +{ static const AttrTableId id = AttrTableTNode; typedef AttrHash table_type; static inline table_type& get(AttributeManager& am) { @@ -280,7 +280,8 @@ struct getTable { /** Access the "d_nodes" member of AttributeManager. */ template <> -struct getTable { +struct getTable +{ static const AttrTableId id = AttrTableNode; typedef AttrHash table_type; static inline table_type& get(AttributeManager& am) { @@ -293,7 +294,8 @@ struct getTable { /** Access the "d_types" member of AttributeManager. */ template <> -struct getTable { +struct getTable +{ static const AttrTableId id = AttrTableTypeNode; typedef AttrHash table_type; static inline table_type& get(AttributeManager& am) { @@ -306,7 +308,8 @@ struct getTable { /** Access the "d_strings" member of AttributeManager. */ template <> -struct getTable { +struct getTable +{ static const AttrTableId id = AttrTableString; typedef AttrHash 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 mapping; - typedef typename getTable:: - table_type table_type; + typedef typename getTable::table_type table_type; - const table_type& ah = - getTable::get(*this); + const table_type& ah = getTable::get(*this); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -371,12 +372,9 @@ struct HasAttribute { typename AttrKind::value_type& ret) { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping mapping; - typedef typename getTable::table_type - table_type; + typedef typename getTable::table_type table_type; - const table_type& ah = - getTable::get(*am); + const table_type& ah = getTable::get(*am); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -400,11 +398,9 @@ struct HasAttribute { NodeValue* nv) { typedef typename AttrKind::value_type value_type; //typedef KindValueToTableValueMapping mapping; - typedef typename getTable:: - table_type table_type; + typedef typename getTable::table_type table_type; - const table_type& ah = - getTable::get(*am); + const table_type& ah = getTable::get(*am); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -420,11 +416,9 @@ struct HasAttribute { typename AttrKind::value_type& ret) { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping mapping; - typedef typename getTable:: - table_type table_type; + typedef typename getTable::table_type table_type; - const table_type& ah = - getTable::get(*am); + const table_type& ah = getTable::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 mapping; - typedef typename getTable:: - table_type table_type; + typedef typename getTable::table_type table_type; - table_type& ah = - getTable::get(*this); + table_type& ah = getTable::get(*this); ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value); } @@ -473,7 +465,7 @@ template inline void AttributeManager::deleteFromTable(AttrHash& table, NodeValue* nv) { // This cannot use nv as anything other than a pointer! - const uint64_t last = attr::LastAttributeId::getId(); + const uint64_t last = attr::LastAttributeId::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& table) { template AttributeUniqueId AttributeManager::getAttributeId(const AttrKind& attr){ typedef typename AttrKind::value_type value_type; - AttrTableId tableId = getTable::id; + AttrTableId tableId = getTable::id; return AttributeUniqueId(tableId, attr.getId()); } diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index c82e62836..2ae216d3c 100644 --- 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 -struct LastAttributeId { +template +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 +template 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:: table_value_type table_value_type; - return attr::LastAttributeId::getNextId(); + return attr::LastAttributeId::getNextId(); } };/* class Attribute<> */ /** * An "attribute type" structure for boolean flags (special). */ -template -class Attribute +template +class Attribute { /** 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::getNextId(); + const uint64_t id = attr::LastAttributeId::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 -const uint64_t Attribute::s_id = - Attribute::registerAttribute(); - +template +const uint64_t Attribute::s_id = + Attribute::registerAttribute(); /** Assign unique IDs to attributes at load time. */ -template -const uint64_t Attribute::s_id = - Attribute::registerAttribute(); +template +const uint64_t Attribute::s_id = + Attribute::registerAttribute(); } // namespace expr } // namespace cvc5 diff --git a/test/unit/node/attribute_white.cpp b/test/unit/node/attribute_white.cpp index fe74130d1..4b0f1892f 100644 --- 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::getId(); + unsigned lastId = attr::LastAttributeId::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::getId(); + lastId = attr::LastAttributeId::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::getId(); + lastId = attr::LastAttributeId::getId(); ASSERT_LT(TypeAttr::s_id, lastId); } -- 2.30.2