* 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.

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);
 }