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);
}
};
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,
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 <>
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 <>
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 <>
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();
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) {
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;
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;
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;
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);
}
#include "cvc4_config.h"
#include "expr/kind.h"
+#include "expr/type.h"
#include "util/Assert.h"
namespace CVC4 {
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&,
}
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 ?" );
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 ?" );
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,
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);
}