diff options
Diffstat (limited to 'src/expr/attribute_internals.h')
-rw-r--r-- | src/expr/attribute_internals.h | 224 |
1 files changed, 0 insertions, 224 deletions
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). |