diff options
Diffstat (limited to 'src/expr/attribute_internals.h')
-rw-r--r-- | src/expr/attribute_internals.h | 231 |
1 files changed, 225 insertions, 6 deletions
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index a77d09c4d..3bbab17a4 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -153,11 +153,11 @@ namespace attr { * to value_type using our specialized hash function for these pairs. */ template <class value_type> -struct AttrHash : +class AttrHash : public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>, value_type, AttrHashStrategy> { -}; +};/* class AttrHash<> */ /** * In the case of Boolean-valued attributes we have a special @@ -205,7 +205,7 @@ class AttrHash<bool> : operator bool() const { return (d_word & (1 << d_bit)) ? true : false; } - }; + };/* class AttrHash<bool>::BitAccessor */ /** * A (somewhat degenerate) iterator over boolean-valued attributes. @@ -239,7 +239,7 @@ class AttrHash<bool> : bool operator==(const BitIterator& b) { return d_entry == b.d_entry && d_bit == b.d_bit; } - }; + };/* class AttrHash<bool>::BitIterator */ /** * A (somewhat degenerate) const_iterator over boolean-valued @@ -274,7 +274,7 @@ class AttrHash<bool> : bool operator==(const ConstBitIterator& b) { return d_entry == b.d_entry && d_bit == b.d_bit; } - }; + };/* class AttrHash<bool>::ConstBitIterator */ public: @@ -374,7 +374,226 @@ public: value_type, AttrHashStrategy>(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::CDMap<NodeValue*, + uint64_t, + AttrHashBoolStrategy> { + + /** A "super" type, like in Java, for easy reference below. */ + typedef context::CDMap<NodeValue*, uint64_t, AttrHashBoolStrategy> 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, %lx, %u)\n", &map, key, 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, %lx, %u)\n", &d_map, d_key, 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, %lx, %u)\n", &d_map, d_key, d_word, d_bit); + } + + return *this; + } + + operator bool() const { + Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor::toBool(%p, %p, %lx, %u)\n", &d_map, d_key, d_word, d_bit); + return (d_word & (1 << d_bit)) ? true : false; + } + };/* class CDAttrHash<bool>::BitAccessor */ + + /** + * A (somewhat degenerate) iterator over boolean-valued attributes. + * This iterator doesn't support anything except comparison and + * dereference. It's intended just for the result of find() on the + * table. + */ + class BitIterator { + + super* d_map; + + std::pair<NodeValue* const, uint64_t>* d_entry; + + unsigned d_bit; + + public: + + BitIterator() : + d_map(NULL), + d_entry(NULL), + d_bit(0) { + } + + BitIterator(super& map, std::pair<NodeValue* const, uint64_t>& entry, unsigned bit) : + d_map(&map), + d_entry(&entry), + d_bit(bit) { + } + + std::pair<NodeValue* const, BitAccessor> operator*() { + return std::make_pair(d_entry->first, + BitAccessor(*d_map, d_entry->first, d_entry->second, d_bit)); + } + + bool operator==(const BitIterator& b) { + return d_entry == b.d_entry && d_bit == b.d_bit; + } + };/* class CDAttrHash<bool>::BitIterator */ + + /** + * 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 BitIterator 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. + */ + /*BitIterator find(const std::pair<uint64_t, NodeValue*>& k) { + super::iterator i = super::find(k.second); + if(i == super::end()) { + return BitIterator(); + } + Debug.printf("cdboolattr", + "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", + &(*i).second, + (unsigned long long)((*i).second), + unsigned(k.first)); + return BitIterator(*i, k.first); + }*/ + + /** The "off the end" iterator */ + BitIterator end() { + return BitIterator(); + } + + /** + * 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. + */ + void erase(NodeValue* nv) { + super::obliterate(nv); + } + + /** + * Clear the hash table. + */ + void clear() { + super::clear(); + } + +};/* class CDAttrHash<bool> */ }/* CVC4::expr::attr namespace */ |