diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-22 19:24:43 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-22 19:24:43 +0000 |
commit | 09279d722aa6e62e86eb4b34583397db1093051e (patch) | |
tree | 1abb476b99c20c3c8906d8893159923eb0ccce3a /src/expr/attribute.h | |
parent | c96d62d41a178e0f524c39a0f73da9b7730dcf0b (diff) |
Re-committing revision 232 properly:
* Add virtual destructors to CnfStream, Theory, OutputChannel, and
ExplainOutputChannel. Safer and stops a compiler warning.
* node attributes: fix compiler warnings on 64-bit.
* Node: add asserts to make sure the current NodeManager is non-NULL
when it's needed. This can happen when public-facing functions
don't properly set the node manager, and it can look like a bug in
another part of the library. Also some code format cleanup.
* configure.ac, config/cvc4.m4: added --enable-static-binary (see
discussion on bug 33), fixed bad configure lines (bug 19), added
documentation for some things.
* config.h.in: removed; it's auto-generated.
Diffstat (limited to 'src/expr/attribute.h')
-rw-r--r-- | src/expr/attribute.h | 54 |
1 files changed, 31 insertions, 23 deletions
diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 12de9eb5f..1d2705240 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -56,7 +56,7 @@ namespace expr { struct AttrHashFcn { enum { LARGE_PRIME = 1 }; - std::size_t operator()(const std::pair<unsigned, SoftNode>& p) const { + std::size_t operator()(const std::pair<uint64_t, SoftNode>& p) const { return p.first * LARGE_PRIME + p.second.hash(); } }; @@ -122,7 +122,7 @@ struct KindTableMapping { // use a TAG to indicate which table it should be in template <class value_type> -struct AttrHash : public __gnu_cxx::hash_map<std::pair<unsigned, SoftNode>, value_type, AttrHashFcn> {}; +struct AttrHash : public __gnu_cxx::hash_map<std::pair<uint64_t, SoftNode>, value_type, AttrHashFcn> {}; template <> class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> { @@ -215,19 +215,23 @@ class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHas public: - typedef std::pair<unsigned, SoftNode> key_type; + typedef std::pair<uint64_t, SoftNode> key_type; typedef bool data_type; typedef std::pair<const key_type, data_type> value_type; typedef BitIterator iterator; typedef ConstBitIterator const_iterator; - BitIterator find(const std::pair<unsigned, SoftNode>& k) { + BitIterator find(const std::pair<uint64_t, SoftNode>& k) { super::iterator i = super::find(k.second); if(i == super::end()) { return BitIterator(); } - Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (*i).second, k.first); + Debug.printf("boolattr", + "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); } @@ -235,12 +239,16 @@ public: return BitIterator(); } - ConstBitIterator find(const std::pair<unsigned, SoftNode>& k) const { + ConstBitIterator find(const std::pair<uint64_t, SoftNode>& k) const { super::const_iterator i = super::find(k.second); if(i == super::end()) { return ConstBitIterator(); } - Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (*i).second, k.first); + Debug.printf("boolattr", + "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", + &(*i).second, + (unsigned long long)((*i).second), + unsigned(k.first)); return ConstBitIterator(*i, k.first); } @@ -248,7 +256,7 @@ public: return ConstBitIterator(); } - BitAccessor operator[](const std::pair<unsigned, SoftNode>& k) { + BitAccessor operator[](const std::pair<uint64_t, SoftNode>& k) { uint64_t& word = super::operator[](k.second); return BitAccessor(word, k.first); } @@ -268,18 +276,18 @@ struct Attribute { /** cleanup routine when the Node goes away */ static inline void cleanup(const value_t&) {} - static inline unsigned getId() { return s_id; } - static inline unsigned getHashValue() { return s_hashValue; } + static inline uint64_t getId() { return s_id; } + static inline uint64_t getHashValue() { return s_hashValue; } static const bool has_default_value = false; private: /** an id */ - static const unsigned s_id; + static const uint64_t s_id; /** an extra hash value (to avoid same-value-type collisions) */ - static const unsigned s_hashValue; + static const uint64_t s_hashValue; }; /** @@ -294,13 +302,13 @@ struct Attribute<T, bool> { /** cleanup routine when the Node goes away */ static inline void cleanup(const bool&) {} - static inline unsigned getId() { return s_id; } - static inline unsigned getHashValue() { return s_hashValue; } + static inline uint64_t getId() { return s_id; } + static inline uint64_t getHashValue() { return s_hashValue; } static const bool has_default_value = true; static const bool default_value = false; - static inline unsigned checkID(unsigned id) { + static inline uint64_t checkID(uint64_t id) { AlwaysAssert(id <= 63, "Too many boolean node attributes registered during initialization !"); return id; @@ -309,10 +317,10 @@ struct Attribute<T, bool> { private: /** a bit assignment */ - static const unsigned s_id; + static const uint64_t s_id; /** an extra hash value (to avoid same-value-type collisions) */ - static const unsigned s_hashValue; + static const uint64_t s_hashValue; }; // SPECIFIC, GLOBAL ATTRIBUTE DEFINITIONS ====================================== @@ -323,11 +331,11 @@ namespace attr { template <class T> struct LastAttributeId { - static unsigned s_id; + static uint64_t s_id; }; template <class T> - unsigned LastAttributeId<T>::s_id = 0; + uint64_t LastAttributeId<T>::s_id = 0; }/* CVC4::expr::attr namespace */ typedef Attribute<attr::VarName, std::string> VarNameAttr; @@ -336,16 +344,16 @@ typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr; // ATTRIBUTE IDENTIFIER ASSIGNMENT ============================================= template <class T, class value_t> -const unsigned Attribute<T, value_t>::s_id = +const uint64_t Attribute<T, value_t>::s_id = attr::LastAttributeId<typename KindValueToTableValueMapping<value_t>::table_value_type>::s_id++; template <class T, class value_t> -const unsigned Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id; +const uint64_t Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id; template <class T> -const unsigned Attribute<T, bool>::s_id = +const uint64_t Attribute<T, bool>::s_id = Attribute<T, bool>::checkID(attr::LastAttributeId<bool>::s_id++); template <class T> -const unsigned Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id; +const uint64_t Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id; class AttributeManager; |