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 | |
parent | 7fd11d0df4c257a916e93c3f44238f1d3f70f721 (diff) |
Removing the unused CDAttribute. This makes CDHashMap::obliterate unused. Removing it as well.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/attribute.cpp | 33 | ||||
-rw-r--r-- | src/expr/attribute.h | 182 | ||||
-rw-r--r-- | src/expr/attribute_internals.h | 224 |
3 files changed, 23 insertions, 416 deletions
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index 2f938736e..f221c7c7e 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -13,12 +13,12 @@ ** ** AttributeManager implementation. **/ +#include "expr/attribute.h" + #include <utility> #include "base/output.h" -#include "expr/attribute.h" #include "expr/node_value.h" -#include "smt/smt_engine.h" using namespace std; @@ -26,15 +26,6 @@ namespace CVC4 { namespace expr { namespace attr { -SmtAttributes::SmtAttributes(context::Context* ctxt) : - d_cdbools(ctxt), - d_cdints(ctxt), - d_cdtnodes(ctxt), - d_cdnodes(ctxt), - d_cdstrings(ctxt), - d_cdptrs(ctxt) { -} - AttributeManager::AttributeManager() : d_inGarbageCollection(false) {} @@ -43,15 +34,6 @@ bool AttributeManager::inGarbageCollection() const { return d_inGarbageCollection; } -SmtAttributes& AttributeManager::getSmtAttributes(SmtEngine* smt) { - Assert(smt != NULL); - return *smt->d_smtAttributes; -} - -const SmtAttributes& AttributeManager::getSmtAttributes(SmtEngine* smt) const { - return *smt->d_smtAttributes; -} - void AttributeManager::debugHook(int debugFlag) { /* DO NOT CHECK IN ANY CODE INTO THE DEBUG HOOKS! * debugHook() is an empty function for the purpose of debugging @@ -71,17 +53,6 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) { deleteFromTable(d_ptrs, nv); } -void SmtAttributes::deleteAllAttributes(TNode n) { - NodeValue* nv = n.d_nv; - - d_cdbools.erase(nv); - deleteFromTable(d_cdints, nv); - deleteFromTable(d_cdtnodes, nv); - deleteFromTable(d_cdnodes, nv); - deleteFromTable(d_cdstrings, nv); - deleteFromTable(d_cdptrs, nv); -} - void AttributeManager::deleteAllAttributes() { d_bools.clear(); deleteAllFromTable(d_ints); 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. */ diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index 861739932..28c618cb0 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -25,8 +25,6 @@ #include <ext/hash_map> -#include "context/cdhashmap.h" - namespace CVC4 { namespace expr { @@ -368,217 +366,6 @@ public: } };/* class AttrHash<bool> */ -/** - * A "CDAttrHash<value_type>"---the hash table underlying - * attributes---is simply a context-dependent mapping of - * pair<unique-attribute-id, Node> to value_type using our specialized - * hash function for these pairs. - */ -template <class value_type> -class CDAttrHash : - public context::CDHashMap<std::pair<uint64_t, NodeValue*>, - value_type, - AttrHashFunction> { -public: - CDAttrHash(context::Context* ctxt) : - context::CDHashMap<std::pair<uint64_t, NodeValue*>, - value_type, - AttrHashFunction>(ctxt) { - } -};/* class CDAttrHash<> */ - -/** - * In the case of Boolean-valued attributes we have a special - * "CDAttrHash<bool>" to pack bits together in words. - */ -template <> -class CDAttrHash<bool> : - protected context::CDHashMap<NodeValue*, - uint64_t, - AttrBoolHashFunction> { - - /** A "super" type, like in Java, for easy reference below. */ - typedef context::CDHashMap<NodeValue*, uint64_t, AttrBoolHashFunction> super; - - /** - * BitAccessor allows us to return a bit "by reference." Of course, - * we don't require bit-addressibility supported by the system, we - * do it with a complex type. - */ - class BitAccessor { - - super& d_map; - - NodeValue* d_key; - - uint64_t d_word; - - unsigned d_bit; - - public: - - BitAccessor(super& map, NodeValue* key, uint64_t word, unsigned bit) : - d_map(map), - d_key(key), - d_word(word), - d_bit(bit) { - /* - Debug.printf("cdboolattr", - "CDAttrHash<bool>::BitAccessor(%p, %p, %016llx, %u)\n", - &map, key, (unsigned long long) word, bit); - */ - } - - BitAccessor& operator=(bool b) { - if(b) { - // set the bit - d_word |= (1 << d_bit); - d_map.insert(d_key, d_word); - /* - Debug.printf("cdboolattr", - "CDAttrHash<bool>::BitAccessor::set(%p, %p, %016llx, %u)\n", - &d_map, d_key, (unsigned long long) d_word, d_bit); - */ - } else { - // clear the bit - d_word &= ~(1 << d_bit); - d_map.insert(d_key, d_word); - /* - Debug.printf("cdboolattr", - "CDAttrHash<bool>::BitAccessor::clr(%p, %p, %016llx, %u)\n", - &d_map, d_key, (unsigned long long) d_word, d_bit); - */ - } - - return *this; - } - - operator bool() const { - /* - Debug.printf("cdboolattr", - "CDAttrHash<bool>::BitAccessor::toBool(%p, %p, %016llx, %u)\n", - &d_map, d_key, (unsigned long long) d_word, d_bit); - */ - return (d_word & (1 << d_bit)) ? true : false; - } - };/* class CDAttrHash<bool>::BitAccessor */ - - /** - * A (somewhat degenerate) const_iterator over boolean-valued - * attributes. This const_iterator doesn't support anything except - * comparison and dereference. It's intended just for the result of - * find() on the table. - */ - class ConstBitIterator { - - const std::pair<NodeValue* const, uint64_t> d_entry; - - unsigned d_bit; - - public: - - ConstBitIterator() : - d_entry(), - d_bit(0) { - } - - ConstBitIterator(const std::pair<NodeValue* const, uint64_t>& entry, - unsigned bit) : - d_entry(entry), - d_bit(bit) { - } - - std::pair<NodeValue* const, bool> operator*() { - return std::make_pair(d_entry.first, - (d_entry.second & (1 << d_bit)) ? true : false); - } - - bool operator==(const ConstBitIterator& b) { - return d_entry == b.d_entry && d_bit == b.d_bit; - } - };/* class CDAttrHash<bool>::ConstBitIterator */ - - /* remove non-permitted operations */ - CDAttrHash(const CDAttrHash<bool>&) CVC4_UNDEFINED; - CDAttrHash<bool>& operator=(const CDAttrHash<bool>&) CVC4_UNDEFINED; - -public: - - CDAttrHash(context::Context* context) : super(context) { } - - typedef std::pair<uint64_t, NodeValue*> key_type; - typedef bool data_type; - typedef std::pair<const key_type, data_type> value_type; - - /** an iterator type; see above for limitations */ - typedef ConstBitIterator iterator; - /** a const_iterator type; see above for limitations */ - typedef ConstBitIterator const_iterator; - - /** - * Find the boolean value in the hash table. Returns something == - * end() if not found. - */ - ConstBitIterator find(const std::pair<uint64_t, NodeValue*>& k) const { - super::const_iterator i = super::find(k.second); - if(i == super::end()) { - return ConstBitIterator(); - } - /* - Debug.printf("cdboolattr", - "underlying word at address looks like 0x%016llx, bit is %u\n", - (unsigned long long)((*i).second), - unsigned(k.first)); - */ - return ConstBitIterator(*i, k.first); - } - - /** The "off the end" const_iterator */ - ConstBitIterator end() const { - return ConstBitIterator(); - } - - /** - * Access the hash table using the underlying operator[]. Inserts - * the key into the table (associated to default value) if it's not - * already there. - */ - BitAccessor operator[](const std::pair<uint64_t, NodeValue*>& k) { - uint64_t word = super::operator[](k.second); - return BitAccessor(*this, k.second, word, k.first); - } - - /** - * Delete all flags from the given node. Simply calls superclass's - * obliterate(). Note this removes all attributes at all context - * levels for this NodeValue! This is important when the NodeValue - * is no longer referenced and is being collected, but otherwise - * it probably isn't useful to do this. - */ - void erase(NodeValue* nv) { - super::obliterate(nv); - } - - /** - * Clear the hash table. This simply exposes the protected superclass - * version of clear() to clients. - */ - void clear() { - super::clear(); - } - - /** Is the hash table empty? */ - bool empty() const { - return super::empty(); - } - - /** This is currently very misleading! */ - size_t size() const { - return super::size(); - } - -};/* class CDAttrHash<bool> */ - }/* CVC4::expr::attr namespace */ // ATTRIBUTE CLEANUP FUNCTIONS ================================================= @@ -853,17 +640,6 @@ public: };/* class Attribute<..., bool, ...> */ /** - * This is a context-dependent attribute kind (the only difference - * between CDAttribute<> and Attribute<> (with the fourth argument - * "true") is that you cannot supply a cleanup function (a no-op one - * is used). - */ -template <class T, - class value_type> -struct CDAttribute : - public Attribute<T, value_type, attr::NullCleanupStrategy, true> {}; - -/** * This is a managed attribute kind (the only difference between * ManagedAttribute<> and Attribute<> is the default cleanup function * and the fact that ManagedAttributes cannot be context-dependent). |