AttrHash<TypeNode> d_types;
/** Underlying hash table for string-valued attributes */
AttrHash<std::string> d_strings;
- /** Underlying hash table for pointer-valued attributes */
- AttrHash<void*> d_ptrs;
/**
* Get a particular attribute on a particular node.
}
};
-/** Access the "d_ptrs" member of AttributeManager. */
-template <class T>
-struct getTable<T*, false> {
- static const AttrTableId id = AttrTablePointer;
- 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;
- }
-};
-
-/** Access the "d_ptrs" member of AttributeManager. */
-template <class T>
-struct getTable<const T*, false> {
- static const AttrTableId id = AttrTablePointer;
- 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;
- }
-};
-
}/* CVC4::expr::attr namespace */
// ATTRIBUTE MANAGER IMPLEMENTATIONS ===========================================
inline static T convertBack(const T& t) { return t; }
};
-/**
- * Specialization of KindValueToTableValueMapping<> for pointer-valued
- * attributes.
- */
-template <class T>
-struct KindValueToTableValueMapping<T*> {
- /** Table's value type is void* */
- typedef void* table_value_type;
- /** A simple reinterpret_cast<>() conversion from T* to void* */
- inline static void* convert(const T* const& t) {
- return reinterpret_cast<void*>(const_cast<T*>(t));
- }
- /** A simple reinterpret_cast<>() conversion from void* to T* */
- inline static T* convertBack(void* const& t) {
- return reinterpret_cast<T*>(t);
- }
-};
-
-/**
- * Specialization of KindValueToTableValueMapping<> for const
- * pointer-valued attributes.
- */
-template <class T>
-struct KindValueToTableValueMapping<const T*> {
- /** Table's value type is void* */
- typedef void* table_value_type;
- /** A simple reinterpret_cast<>() conversion from const T* const to void* */
- inline static void* convert(const T* const& t) {
- return reinterpret_cast<void*>(const_cast<T*>(t));
- }
- /** A simple reinterpret_cast<>() conversion from const void* const to T* */
- inline static const T* convertBack(const void* const& t) {
- return reinterpret_cast<const T*>(t);
- }
-};
-
}/* CVC4::expr::attr namespace */
// ATTRIBUTE HASH TABLES =======================================================
struct NullCleanupStrategy {
};/* struct NullCleanupStrategy */
-/** Default cleanup for ManagedAttribute<> */
-template <class T>
-struct ManagedAttributeCleanupStrategy {
-};/* struct ManagedAttributeCleanupStrategy<> */
-
-/** Specialization for T* */
-template <class T>
-struct ManagedAttributeCleanupStrategy<T*> {
- static inline void cleanup(T* p) { delete p; }
-};/* struct ManagedAttributeCleanupStrategy<T*> */
-
-/** Specialization for const T* */
-template <class T>
-struct ManagedAttributeCleanupStrategy<const T*> {
- static inline void cleanup(const T* p) { delete p; }
-};/* struct ManagedAttributeCleanupStrategy<const T*> */
-
/**
* Helper for Attribute<> class below to determine whether a cleanup
* is defined or not.
(typename getCleanupStrategy<T, NullCleanupStrategy>::
mapping::table_value_type) = NULL;
-/**
- * Specialization for ManagedAttributeCleanupStrategy<T>.
- */
-template <class T>
-struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> > {
- typedef T value_type;
- typedef KindValueToTableValueMapping<value_type> mapping;
- static void (*const fn)(typename mapping::table_value_type);
-};/* struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> > */
-
-// out-of-class initialization required (because it's a non-integral type)
-template <class T>
-void (*const getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> >::fn)
- (typename getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> >::
- mapping::table_value_type) = NULL;
-
-/**
- * Specialization for ManagedAttributeCleanupStrategy<T*>.
- */
-template <class T>
-struct getCleanupStrategy<T*, ManagedAttributeCleanupStrategy<T*> > {
- typedef T* value_type;
- typedef ManagedAttributeCleanupStrategy<value_type> C;
- typedef KindValueToTableValueMapping<value_type> mapping;
- static void fn(typename mapping::table_value_type t) {
- C::cleanup(mapping::convertBack(t));
- }
-};/* struct getCleanupStrategy<T*, ManagedAttributeCleanupStrategy<T*> > */
-
-/**
- * Specialization for ManagedAttributeCleanupStrategy<const T*>.
- */
-template <class T>
-struct getCleanupStrategy<const T*,
- ManagedAttributeCleanupStrategy<const T*> > {
- typedef const T* value_type;
- typedef ManagedAttributeCleanupStrategy<value_type> C;
- typedef KindValueToTableValueMapping<value_type> mapping;
- static void fn(typename mapping::table_value_type t) {
- C::cleanup(mapping::convertBack(t));
- }
-};/* struct getCleanupStrategy<const T*,
- ManagedAttributeCleanupStrategy<const T*> > */
-
-/**
- * Cause compile-time error for improperly-instantiated
- * getCleanupStrategy<>.
- */
-template <class T, class U>
-struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<U> >;
-
}/* CVC4::expr::attr namespace */
// ATTRIBUTE IDENTIFIER ASSIGNMENT TEMPLATE ====================================
}
};/* class Attribute<..., bool, ...> */
-/**
- * This is a managed attribute kind (the only difference between
- * ManagedAttribute<> and Attribute<> is the default cleanup function
- * and the fact that ManagedAttributes cannot be context-dependent).
- * In the default ManagedAttribute cleanup function, the value is
- * destroyed with the delete operator. If the value is allocated with
- * the array version of new[], an alternate cleanup function should be
- * provided that uses array delete[]. It is an error to create a
- * ManagedAttribute<> kind with a non-pointer value_type if you don't
- * also supply a custom cleanup function.
- */
-template <class T,
- class value_type,
- class CleanupStrategy =
- attr::ManagedAttributeCleanupStrategy<value_type> >
-struct ManagedAttribute :
- public Attribute<T, value_type, CleanupStrategy, false> {};
-
// ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
/** Assign unique IDs to attributes at load time. */
delete d_exprManager;
}
- class MyData {
- public:
- static int count;
- MyData() { count ++; }
- ~MyData() { count --; }
- };
-
- struct MyDataAttributeId {};
-
- struct MyDataCleanupFunction {
- static void cleanup(MyData* myData){
- delete myData;
- }
- };
-
- typedef expr::Attribute<MyDataAttributeId, MyData*, MyDataCleanupFunction> MyDataAttribute;
-
- void testDeallocation() {
- TypeNode booleanType = d_nodeManager->booleanType();
- Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
- MyData* data;
- MyData* data1;
- MyDataAttribute attr;
- TS_ASSERT(!node->getAttribute(attr, data));
- node->setAttribute(attr, new MyData());
- TS_ASSERT(node->getAttribute(attr, data1));
- TS_ASSERT(MyData::count == 1);
- delete node;
- }
-
struct PrimitiveIntAttributeId {};
typedef expr::Attribute<PrimitiveIntAttributeId,uint64_t> PrimitiveIntAttribute;
void testInts(){
delete node;
}
- class Foo {
- int d_bar;
- public:
- Foo(int b) : d_bar(b) {}
- int getBar() const { return d_bar; }
- };
-
- struct PtrAttributeId {};
-
- typedef expr::Attribute<PtrAttributeId, Foo*> PtrAttribute;
- void testPtrs(){
- TypeNode booleanType = d_nodeManager->booleanType();
- Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
-
- Foo* val = new Foo(63489);
- Foo* data0 = NULL;
- Foo* data1 = NULL;
-
- PtrAttribute attr;
- TS_ASSERT(!node->getAttribute(attr, data0));
- node->setAttribute(attr, val);
- TS_ASSERT(node->getAttribute(attr, data1));
- TS_ASSERT_EQUALS(data1, val);
-
- delete node;
- delete val;
- }
-
-
- struct ConstPtrAttributeId {};
-
- typedef expr::Attribute<ConstPtrAttributeId, const Foo*> ConstPtrAttribute;
- void testConstPtrs(){
- TypeNode booleanType = d_nodeManager->booleanType();
- Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
-
- const Foo* val = new Foo(63489);
- const Foo* data0 = NULL;
- const Foo* data1 = NULL;
-
- ConstPtrAttribute attr;
- TS_ASSERT(!node->getAttribute(attr, data0));
- node->setAttribute(attr, val);
- TS_ASSERT(node->getAttribute(attr, data1));
- TS_ASSERT_EQUALS(data1, val);
-
- delete node;
- delete val;
- }
-
struct StringAttributeId {};
typedef expr::Attribute<StringAttributeId, std::string> StringAttribute;
void testStrings(){
}
};
-
-int AttributeBlack::MyData::count = 0;
projects / cvc5.git / commitdiff