From 3d8fd1dad54c4057384c99bf6857361f29c23d12 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 22 Feb 2010 20:51:01 +0000 Subject: [PATCH] * src/expr/attribute.h: fixed an issue with "const pointer"-valued attributes. * src/expr/attribute.h, src/expr/node_manager.h, src/expr/node.h: hasAttribute() and getAttribute() are now const member functions. --- src/expr/attribute.h | 55 ++++++++++++++++++++++++++--------------- src/expr/node.h | 9 ++++--- 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 { inline static void* convert(const T* const& t) { return reinterpret_cast(const_cast(t)); } - inline static const T* convertBack(const void*& t) { + inline static const T* convertBack(const void* const& t) { return reinterpret_cast(t); } }; @@ -381,16 +381,16 @@ public: template typename AttrKind::value_type getAttribute(const Node& n, - const AttrKind&); + const AttrKind&) const; template bool hasAttribute(const Node& n, - const AttrKind&); + const AttrKind&) const; template bool hasAttribute(const Node& n, const AttrKind&, - typename AttrKind::value_type*); + typename AttrKind::value_type*) const; template void setAttribute(const Node& n, @@ -406,6 +406,9 @@ struct getTable { 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 { 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 { 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 { 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 -struct getTable { +struct getTable { typedef AttrHash 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 typename AttrKind::value_type AttributeManager::getAttribute(const Node& n, - const AttrKind&) { + const AttrKind&) const { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping mapping; typedef typename getTable::table_type table_type; - table_type& ah = getTable::get(*this); - typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); + const table_type& ah = getTable::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 struct HasAttribute { - 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 { typedef KindValueToTableValueMapping mapping; typedef typename getTable::table_type table_type; - table_type& ah = getTable::get(*am); - typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); + const table_type& ah = getTable::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 { template struct HasAttribute { - 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 mapping; typedef typename getTable::table_type table_type; - table_type& ah = getTable::get(*am); - typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); + const table_type& ah = getTable::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 { 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 mapping; typedef typename getTable::table_type table_type; - table_type& ah = getTable::get(*am); - typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); + const table_type& ah = getTable::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 { template bool AttributeManager::hasAttribute(const Node& n, - const AttrKind&) { + const AttrKind&) const { return HasAttribute::hasAttribute(this, n); } template bool AttributeManager::hasAttribute(const Node& n, const AttrKind&, - typename AttrKind::value_type* ret) { + typename AttrKind::value_type* ret) const { return HasAttribute::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 - inline typename AttrKind::value_type getAttribute(const AttrKind&); + inline typename AttrKind::value_type getAttribute(const AttrKind&) const; template inline bool hasAttribute(const AttrKind&, - typename AttrKind::value_type* = NULL); + typename AttrKind::value_type* = NULL) const; template inline void setAttribute(const AttrKind&, @@ -262,7 +263,7 @@ inline size_t Node::getNumChildren() const { } template -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 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 inline typename AttrKind::value_type getAttribute(const Node& n, - const AttrKind&); + const AttrKind&) const; template inline bool hasAttribute(const Node& n, const AttrKind&, - typename AttrKind::value_type* = NULL); + typename AttrKind::value_type* = NULL) const; template inline void setAttribute(const Node& n, @@ -110,14 +110,14 @@ public: template inline typename AttrKind::value_type NodeManager::getAttribute(const Node& n, - const AttrKind&) { + const AttrKind&) const { return d_am.getAttribute(n, AttrKind()); } template 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); } -- 2.30.2