diff options
author | Tim King <taking@google.com> | 2017-07-14 16:56:11 -0700 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2017-07-19 18:25:13 -0700 |
commit | d70a63324c95210f1d78c2efc46395d2369d2e2b (patch) | |
tree | 5f1ce222cb3940eb427e3c80544b405479ac02ab /src/expr/attribute.h | |
parent | 7fd11d0df4c257a916e93c3f44238f1d3f70f721 (diff) |
Removing the unused CDAttribute. This makes CDHashMap::obliterate unused. Removing it as well.
Diffstat (limited to 'src/expr/attribute.h')
-rw-r--r-- | src/expr/attribute.h | 182 |
1 files changed, 21 insertions, 161 deletions
diff --git a/src/expr/attribute.h b/src/expr/attribute.h index b5897ac51..5aea4a4d1 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -20,7 +20,6 @@ * attributes and nodes due to template use */ #include "expr/node.h" #include "expr/type_node.h" -#include "context/context.h" #ifndef __CVC4__EXPR__ATTRIBUTE_H #define __CVC4__EXPR__ATTRIBUTE_H @@ -35,45 +34,11 @@ #undef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H namespace CVC4 { - -class SmtEngine; - -namespace smt { - extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current; -}/* CVC4::smt namespace */ - namespace expr { namespace attr { // ATTRIBUTE MANAGER =========================================================== -struct SmtAttributes { - SmtAttributes(context::Context*); - - // IF YOU ADD ANY TABLES, don't forget to add them also to the - // implementation of deleteAllAttributes(). - - /** Underlying hash table for context-dependent boolean-valued attributes */ - CDAttrHash<bool> d_cdbools; - /** Underlying hash table for context-dependent integral-valued attributes */ - CDAttrHash<uint64_t> d_cdints; - /** Underlying hash table for context-dependent node-valued attributes */ - CDAttrHash<TNode> d_cdtnodes; - /** Underlying hash table for context-dependent node-valued attributes */ - CDAttrHash<Node> d_cdnodes; - /** Underlying hash table for context-dependent string-valued attributes */ - CDAttrHash<std::string> d_cdstrings; - /** Underlying hash table for context-dependent pointer-valued attributes */ - CDAttrHash<void*> d_cdptrs; - - /** Delete all attributes of given node */ - void deleteAllAttributes(TNode n); - - template <class T> - void deleteFromTable(CDAttrHash<T>& table, NodeValue* nv); - -};/* struct SmtAttributes */ - /** * A container for the main attribute tables of the system. There's a * one-to-one NodeManager : AttributeManager correspondence. @@ -103,9 +68,6 @@ class AttributeManager { void clearDeleteAllAttributesBuffer(); - SmtAttributes& getSmtAttributes(SmtEngine*); - const SmtAttributes& getSmtAttributes(SmtEngine*) const; - public: /** Construct an attribute manager. */ @@ -239,10 +201,10 @@ template <> struct getTable<bool, false> { static const AttrTableId id = AttrTableBool; typedef AttrHash<bool> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_bools; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_bools; } }; @@ -252,10 +214,10 @@ template <> struct getTable<uint64_t, false> { static const AttrTableId id = AttrTableUInt64; typedef AttrHash<uint64_t> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_ints; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_ints; } }; @@ -265,10 +227,10 @@ template <> struct getTable<TNode, false> { static const AttrTableId id = AttrTableTNode; typedef AttrHash<TNode> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_tnodes; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_tnodes; } }; @@ -278,10 +240,10 @@ template <> struct getTable<Node, false> { static const AttrTableId id = AttrTableNode; typedef AttrHash<Node> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_nodes; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_nodes; } }; @@ -291,10 +253,10 @@ template <> struct getTable<TypeNode, false> { static const AttrTableId id = AttrTableTypeNode; typedef AttrHash<TypeNode> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_types; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_types; } }; @@ -304,10 +266,10 @@ template <> struct getTable<std::string, false> { static const AttrTableId id = AttrTableString; typedef AttrHash<std::string> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_strings; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_strings; } }; @@ -317,10 +279,10 @@ template <class T> struct getTable<T*, false> { static const AttrTableId id = AttrTablePointer; typedef AttrHash<void*> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_ptrs; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_ptrs; } }; @@ -330,105 +292,14 @@ template <class T> struct getTable<const T*, false> { static const AttrTableId id = AttrTablePointer; typedef AttrHash<void*> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_ptrs; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_ptrs; } }; -/** Access the "d_cdbools" member of AttributeManager. */ -template <> -struct getTable<bool, true> { - static const AttrTableId id = AttrTableCDBool; - typedef CDAttrHash<bool> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdbools; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdbools; - } -}; - -/** Access the "d_cdints" member of AttributeManager. */ -template <> -struct getTable<uint64_t, true> { - static const AttrTableId id = AttrTableCDUInt64; - typedef CDAttrHash<uint64_t> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdints; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdints; - } -}; - -/** Access the "d_tnodes" member of AttributeManager. */ -template <> -struct getTable<TNode, true> { - static const AttrTableId id = AttrTableCDTNode; - typedef CDAttrHash<TNode> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdtnodes; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdtnodes; - } -}; - -/** Access the "d_cdnodes" member of AttributeManager. */ -template <> -struct getTable<Node, true> { - static const AttrTableId id = AttrTableCDNode; - typedef CDAttrHash<Node> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdnodes; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdnodes; - } -}; - -/** Access the "d_cdstrings" member of AttributeManager. */ -template <> -struct getTable<std::string, true> { - static const AttrTableId id = AttrTableCDString; - typedef CDAttrHash<std::string> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdstrings; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdstrings; - } -}; - -/** Access the "d_cdptrs" member of AttributeManager. */ -template <class T> -struct getTable<T*, true> { - static const AttrTableId id = AttrTableCDPointer; - typedef CDAttrHash<void*> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdptrs; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdptrs; - } -}; - -/** Access the "d_cdptrs" member of AttributeManager. */ -template <class T> -struct getTable<const T*, true> { - static const AttrTableId id = AttrTableCDPointer; - typedef CDAttrHash<void*> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdptrs; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdptrs; - } -}; - }/* CVC4::expr::attr namespace */ // ATTRIBUTE MANAGER IMPLEMENTATIONS =========================================== @@ -445,7 +316,7 @@ AttributeManager::getAttribute(NodeValue* nv, const AttrKind&) const { table_type table_type; const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*this, smt::s_smtEngine_current); + getTable<value_type, AttrKind::context_dependent>::get(*this); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -488,7 +359,7 @@ struct HasAttribute<true, AttrKind> { table_type; const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current); + getTable<value_type, AttrKind::context_dependent>::get(*am); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -516,7 +387,7 @@ struct HasAttribute<false, AttrKind> { table_type table_type; const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current); + getTable<value_type, AttrKind::context_dependent>::get(*am); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -536,7 +407,7 @@ struct HasAttribute<false, AttrKind> { table_type table_type; const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current); + getTable<value_type, AttrKind::context_dependent>::get(*am); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -576,7 +447,7 @@ AttributeManager::setAttribute(NodeValue* nv, table_type table_type; table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*this, smt::s_smtEngine_current); + getTable<value_type, AttrKind::context_dependent>::get(*this); ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value); } @@ -606,17 +477,6 @@ inline void AttributeManager::deleteFromTable(AttrHash<T>& table, } /** - * Obliterate a NodeValue from a (context-dependent) attribute table. - */ -template <class T> -inline void SmtAttributes::deleteFromTable(CDAttrHash<T>& table, - NodeValue* nv) { - for(unsigned id = 0; id < attr::LastAttributeId<T, true>::getId(); ++id) { - table.obliterate(std::make_pair(id, nv)); - } -} - -/** * Remove all attributes from the table calling the cleanup function * if one is defined. */ |