diff options
-rw-r--r-- | src/expr/attribute.h | 55 | ||||
-rw-r--r-- | src/expr/node.h | 9 | ||||
-rw-r--r-- | src/expr/node_manager.h | 8 |
3 files changed, 44 insertions, 28 deletions
diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 54500d0d5..95433688e 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -100,7 +100,7 @@ struct KindValueToTableValueMapping<const T*> { inline static void* convert(const T* const& t) { return reinterpret_cast<void*>(const_cast<T*>(t)); } - inline static const T* convertBack(const void*& t) { + inline static const T* convertBack(const void* const& t) { return reinterpret_cast<const T*>(t); } }; @@ -381,16 +381,16 @@ public: template <class AttrKind> typename AttrKind::value_type getAttribute(const Node& n, - const AttrKind&); + const AttrKind&) const; template <class AttrKind> bool hasAttribute(const Node& n, - const AttrKind&); + const AttrKind&) const; template <class AttrKind> bool hasAttribute(const Node& n, const AttrKind&, - typename AttrKind::value_type*); + typename AttrKind::value_type*) const; template <class AttrKind> void setAttribute(const Node& n, @@ -406,6 +406,9 @@ struct getTable<bool> { static inline table_type& get(AttributeManager& am) { return am.d_bools; } + static inline const table_type& get(const AttributeManager& am) { + return am.d_bools; + } }; template <> @@ -414,6 +417,9 @@ struct getTable<uint64_t> { static inline table_type& get(AttributeManager& am) { return am.d_ints; } + static inline const table_type& get(const AttributeManager& am) { + return am.d_ints; + } }; template <> @@ -422,6 +428,9 @@ struct getTable<Node> { static inline table_type& get(AttributeManager& am) { return am.d_exprs; } + static inline const table_type& get(const AttributeManager& am) { + return am.d_exprs; + } }; template <> @@ -430,28 +439,34 @@ struct getTable<std::string> { static inline table_type& get(AttributeManager& am) { return am.d_strings; } + static inline const table_type& get(const AttributeManager& am) { + return am.d_strings; + } }; template <class T> -struct getTable<T*> { +struct getTable<const T*> { typedef AttrHash<void*> table_type; static inline table_type& get(AttributeManager& am) { return am.d_ptrs; } + static inline const table_type& get(const AttributeManager& am) { + return am.d_ptrs; + } }; // ATTRIBUTE MANAGER IMPLEMENTATIONS =========================================== template <class AttrKind> typename AttrKind::value_type AttributeManager::getAttribute(const Node& n, - const AttrKind&) { + const AttrKind&) const { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping<value_type> mapping; typedef typename getTable<value_type>::table_type table_type; - table_type& ah = getTable<value_type>::get(*this); - typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); + const table_type& ah = getTable<value_type>::get(*this); + typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); if(i == ah.end()) { return typename AttrKind::value_type(); @@ -468,12 +483,12 @@ struct HasAttribute; template <class AttrKind> struct HasAttribute<true, AttrKind> { - static inline bool hasAttribute(AttributeManager* am, + static inline bool hasAttribute(const AttributeManager* am, const Node& n) { return true; } - static inline bool hasAttribute(AttributeManager* am, + static inline bool hasAttribute(const AttributeManager* am, const Node& n, typename AttrKind::value_type* ret) { if(ret != NULL) { @@ -481,8 +496,8 @@ struct HasAttribute<true, AttrKind> { typedef KindValueToTableValueMapping<value_type> mapping; typedef typename getTable<value_type>::table_type table_type; - table_type& ah = getTable<value_type>::get(*am); - typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); + const table_type& ah = getTable<value_type>::get(*am); + typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); if(i == ah.end()) { *ret = AttrKind::default_value; @@ -497,14 +512,14 @@ struct HasAttribute<true, AttrKind> { template <class AttrKind> struct HasAttribute<false, AttrKind> { - static inline bool hasAttribute(AttributeManager* am, + static inline bool hasAttribute(const AttributeManager* am, const Node& n) { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping<value_type> mapping; typedef typename getTable<value_type>::table_type table_type; - table_type& ah = getTable<value_type>::get(*am); - typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); + const table_type& ah = getTable<value_type>::get(*am); + typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); if(i == ah.end()) { return false; @@ -513,15 +528,15 @@ struct HasAttribute<false, AttrKind> { return true; } - static inline bool hasAttribute(AttributeManager* am, + static inline bool hasAttribute(const AttributeManager* am, const Node& n, typename AttrKind::value_type* ret) { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping<value_type> mapping; typedef typename getTable<value_type>::table_type table_type; - table_type& ah = getTable<value_type>::get(*am); - typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); + const table_type& ah = getTable<value_type>::get(*am); + typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); if(i == ah.end()) { return false; @@ -537,14 +552,14 @@ struct HasAttribute<false, AttrKind> { template <class AttrKind> bool AttributeManager::hasAttribute(const Node& n, - const AttrKind&) { + const AttrKind&) const { return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, n); } template <class AttrKind> bool AttributeManager::hasAttribute(const Node& n, const AttrKind&, - typename AttrKind::value_type* ret) { + typename AttrKind::value_type* ret) const { return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, n, ret); } diff --git a/src/expr/node.h b/src/expr/node.h index a39dc5b7e..517a9eb7f 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -25,6 +25,7 @@ #include "cvc4_config.h" #include "expr/kind.h" +#include "expr/type.h" #include "util/Assert.h" namespace CVC4 { @@ -156,11 +157,11 @@ public: bool isAtomic() const; template <class AttrKind> - inline typename AttrKind::value_type getAttribute(const AttrKind&); + inline typename AttrKind::value_type getAttribute(const AttrKind&) const; template <class AttrKind> inline bool hasAttribute(const AttrKind&, - typename AttrKind::value_type* = NULL); + typename AttrKind::value_type* = NULL) const; template <class AttrKind> inline void setAttribute(const AttrKind&, @@ -262,7 +263,7 @@ inline size_t Node::getNumChildren() const { } template <class AttrKind> -inline typename AttrKind::value_type Node::getAttribute(const AttrKind&) { +inline typename AttrKind::value_type Node::getAttribute(const AttrKind&) const { Assert( NodeManager::currentNM() != NULL, "There is no current CVC4::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?" ); @@ -272,7 +273,7 @@ inline typename AttrKind::value_type Node::getAttribute(const AttrKind&) { template <class AttrKind> inline bool Node::hasAttribute(const AttrKind&, - typename AttrKind::value_type* ret) { + typename AttrKind::value_type* ret) const { Assert( NodeManager::currentNM() != NULL, "There is no current CVC4::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?" ); diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 97f5ba9cd..d6d54bd5d 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -79,12 +79,12 @@ public: template <class AttrKind> inline typename AttrKind::value_type getAttribute(const Node& n, - const AttrKind&); + const AttrKind&) const; template <class AttrKind> inline bool hasAttribute(const Node& n, const AttrKind&, - typename AttrKind::value_type* = NULL); + typename AttrKind::value_type* = NULL) const; template <class AttrKind> inline void setAttribute(const Node& n, @@ -110,14 +110,14 @@ public: template <class AttrKind> inline typename AttrKind::value_type NodeManager::getAttribute(const Node& n, - const AttrKind&) { + const AttrKind&) const { return d_am.getAttribute(n, AttrKind()); } template <class AttrKind> inline bool NodeManager::hasAttribute(const Node& n, const AttrKind&, - typename AttrKind::value_type* ret) { + typename AttrKind::value_type* ret) const { return d_am.hasAttribute(n, AttrKind(), ret); } |