summaryrefslogtreecommitdiff
path: root/src/expr/attribute_internals.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/attribute_internals.h')
-rw-r--r--src/expr/attribute_internals.h695
1 files changed, 695 insertions, 0 deletions
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
new file mode 100644
index 000000000..d50c2284d
--- /dev/null
+++ b/src/expr/attribute_internals.h
@@ -0,0 +1,695 @@
+/********************* */
+/** attribute_internals.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Node attributes' internals.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
+# error expr/attribute_internals.h should only be included by expr/attribute.h
+#endif /* CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H */
+
+#ifndef __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
+#define __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
+
+namespace CVC4 {
+namespace expr {
+
+// ATTRIBUTE HASH FUNCTIONS ====================================================
+
+namespace attr {
+
+/**
+ * A hash function for attribute table keys. Attribute table keys are
+ * pairs, (unique-attribute-id, Node).
+ */
+struct AttrHashStrategy {
+ enum { LARGE_PRIME = 32452843ul };
+ std::size_t operator()(const std::pair<uint64_t, NodeValue*>& p) const {
+ return p.first * LARGE_PRIME + p.second->getId();
+ }
+};
+
+/**
+ * A hash function for boolean-valued attribute table keys; here we
+ * don't have to store a pair as the key, because we use a known bit
+ * in [0..63] for each attribute
+ */
+struct AttrHashBoolStrategy {
+ std::size_t operator()(NodeValue* nv) const {
+ return (size_t)nv->getId();
+ }
+};
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE TYPE MAPPINGS =====================================================
+
+namespace attr {
+
+/**
+ * KindValueToTableValueMapping is a compile-time-only mechanism to
+ * convert "attribute value types" into "table value types" and back
+ * again.
+ *
+ * Each instantiation <T> is expected to have three members:
+ *
+ * typename table_value_type
+ *
+ * A type representing the underlying table's value_type for
+ * attribute value type (T). It may be different from T, e.g. T
+ * could be a pointer-to-Foo, but the underlying table value_type
+ * might be pointer-to-void.
+ *
+ * static [convertible-to-table_value_type] convert([convertible-from-T])
+ *
+ * Converts a T into a table_value_type. Used to convert an
+ * attribute value on setting it (and assigning it into the
+ * underlying table). See notes on specializations of
+ * KindValueToTableValueMapping, below.
+ *
+ * static [convertible-to-T] convertBack([convertible-from-table_value_type])
+ *
+ * Converts a table_value_type back into a T. Used to convert an
+ * underlying table value back into the attribute's expected type
+ * when retrieving it from the table. See notes on
+ * specializations of KindValueToTableValueMapping, below.
+ *
+ * This general (non-specialized) implementation of the template does
+ * nothing.
+ */
+template <class T>
+struct KindValueToTableValueMapping {
+ /** Simple case: T == table_value_type */
+ typedef T table_value_type;
+ /** No conversion necessary */
+ inline static T convert(const T& t) { return t; }
+ /** No conversion necessary */
+ 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 =======================================================
+
+namespace attr {
+
+/**
+ * An "AttrHash<value_type>"---the hash table underlying
+ * attributes---is simply a mapping of pair<unique-attribute-id, Node>
+ * to value_type using our specialized hash function for these pairs.
+ */
+template <class value_type>
+struct AttrHash :
+ public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>,
+ value_type,
+ AttrHashStrategy> {
+};
+
+/**
+ * In the case of Boolean-valued attributes we have a special
+ * "AttrHash<bool>" to pack bits together in words.
+ */
+template <>
+class AttrHash<bool> :
+ protected __gnu_cxx::hash_map<NodeValue*,
+ uint64_t,
+ AttrHashBoolStrategy> {
+
+ /** A "super" type, like in Java, for easy reference below. */
+ typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrHashBoolStrategy> super;
+
+ /**
+ * BitAccessor allows us to return a bit "by reference." Of course,
+ * we don't require bit-addressibility supported by the system, we
+ * do it with a complex type.
+ */
+ class BitAccessor {
+
+ uint64_t& d_word;
+
+ unsigned d_bit;
+
+ public:
+
+ BitAccessor(uint64_t& word, unsigned bit) :
+ d_word(word),
+ d_bit(bit) {
+ }
+
+ BitAccessor& operator=(bool b) {
+ if(b) {
+ // set the bit
+ d_word |= (1 << d_bit);
+ } else {
+ // clear the bit
+ d_word &= ~(1 << d_bit);
+ }
+
+ return *this;
+ }
+
+ operator bool() const {
+ return (d_word & (1 << d_bit)) ? true : false;
+ }
+ };
+
+ /**
+ * A (somewhat degenerate) iterator over boolean-valued attributes.
+ * This iterator doesn't support anything except comparison and
+ * dereference. It's intended just for the result of find() on the
+ * table.
+ */
+ class BitIterator {
+
+ std::pair<NodeValue* const, uint64_t>* d_entry;
+
+ unsigned d_bit;
+
+ public:
+
+ BitIterator() :
+ d_entry(NULL),
+ d_bit(0) {
+ }
+
+ BitIterator(std::pair<NodeValue* const, uint64_t>& entry, unsigned bit) :
+ d_entry(&entry),
+ d_bit(bit) {
+ }
+
+ std::pair<NodeValue* const, BitAccessor> operator*() {
+ return std::make_pair(d_entry->first,
+ BitAccessor(d_entry->second, d_bit));
+ }
+
+ bool operator==(const BitIterator& b) {
+ return d_entry == b.d_entry && d_bit == b.d_bit;
+ }
+ };
+
+ /**
+ * A (somewhat degenerate) const_iterator over boolean-valued
+ * attributes. This const_iterator doesn't support anything except
+ * comparison and dereference. It's intended just for the result of
+ * find() on the table.
+ */
+ class ConstBitIterator {
+
+ const std::pair<NodeValue* const, uint64_t>* d_entry;
+
+ unsigned d_bit;
+
+ public:
+
+ ConstBitIterator() :
+ d_entry(NULL),
+ d_bit(0) {
+ }
+
+ ConstBitIterator(const std::pair<NodeValue* const, uint64_t>& entry,
+ unsigned bit) :
+ d_entry(&entry),
+ d_bit(bit) {
+ }
+
+ std::pair<NodeValue* const, bool> operator*() {
+ return std::make_pair(d_entry->first,
+ (d_entry->second & (1 << d_bit)) ? true : false);
+ }
+
+ bool operator==(const ConstBitIterator& b) {
+ return d_entry == b.d_entry && d_bit == b.d_bit;
+ }
+ };
+
+public:
+
+ typedef std::pair<uint64_t, NodeValue*> key_type;
+ typedef bool data_type;
+ typedef std::pair<const key_type, data_type> value_type;
+
+ /** an iterator type; see above for limitations */
+ typedef BitIterator iterator;
+ /** a const_iterator type; see above for limitations */
+ typedef ConstBitIterator const_iterator;
+
+ /**
+ * Find the boolean value in the hash table. Returns something ==
+ * end() if not found.
+ */
+ BitIterator find(const std::pair<uint64_t, NodeValue*>& k) {
+ super::iterator i = super::find(k.second);
+ if(i == super::end()) {
+ return BitIterator();
+ }
+ Debug.printf("boolattr",
+ "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
+ &(*i).second,
+ (unsigned long long)((*i).second),
+ unsigned(k.first));
+ return BitIterator(*i, k.first);
+ }
+
+ /** The "off the end" iterator */
+ BitIterator end() {
+ return BitIterator();
+ }
+
+ /**
+ * Find the boolean value in the hash table. Returns something ==
+ * end() if not found.
+ */
+ ConstBitIterator find(const std::pair<uint64_t, NodeValue*>& k) const {
+ super::const_iterator i = super::find(k.second);
+ if(i == super::end()) {
+ return ConstBitIterator();
+ }
+ Debug.printf("boolattr",
+ "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
+ &(*i).second,
+ (unsigned long long)((*i).second),
+ unsigned(k.first));
+ return ConstBitIterator(*i, k.first);
+ }
+
+ /** The "off the end" const_iterator */
+ ConstBitIterator end() const {
+ return ConstBitIterator();
+ }
+
+ /**
+ * Access the hash table using the underlying operator[]. Inserts
+ * the key into the table (associated to default value) if it's not
+ * already there.
+ */
+ BitAccessor operator[](const std::pair<uint64_t, NodeValue*>& k) {
+ uint64_t& word = super::operator[](k.second);
+ return BitAccessor(word, k.first);
+ }
+
+ /**
+ * Delete all flags from the given node.
+ */
+ void erase(NodeValue* nv) {
+ super::erase(nv);
+ }
+
+};/* class AttrHash<bool> */
+
+/**
+ * A "CDAttrHash<value_type>"---the hash table underlying
+ * attributes---is simply a context-dependent mapping of
+ * pair<unique-attribute-id, Node> to value_type using our specialized
+ * hash function for these pairs.
+ */
+template <class value_type>
+class CDAttrHash :
+ public context::CDMap<std::pair<uint64_t, NodeValue*>,
+ value_type,
+ AttrHashStrategy> {
+public:
+ CDAttrHash(context::Context* ctxt) :
+ context::CDMap<std::pair<uint64_t, NodeValue*>,
+ value_type,
+ AttrHashStrategy>(ctxt) {
+ }
+};
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE CLEANUP FUNCTIONS =================================================
+
+namespace attr {
+
+/** Default cleanup for unmanaged Attribute<> */
+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.
+ */
+template <class T, class C>
+struct getCleanupStrategy {
+ typedef T value_type;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ static void fn(typename mapping::table_value_type t) {
+ C::cleanup(mapping::convertBack(t));
+ }
+};/* struct getCleanupStrategy<> */
+
+/**
+ * Specialization for NullCleanupStrategy.
+ */
+template <class T>
+struct getCleanupStrategy<T, NullCleanupStrategy> {
+ typedef T value_type;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ static void (*const fn)(typename mapping::table_value_type);
+};/* struct getCleanupStrategy<T, NullCleanupStrategy> */
+
+// out-of-class initialization required (because it's a non-integral type)
+template <class T>
+void (*const getCleanupStrategy<T, NullCleanupStrategy>::fn)
+ (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 ====================================
+
+namespace attr {
+
+/**
+ * This is the last-attribute-assigner. IDs are not globally
+ * unique; rather, they are unique for each table_value_type.
+ */
+template <class T, bool context_dep>
+struct LastAttributeId {
+ static uint64_t s_id;
+};
+
+/** Initially zero. */
+template <class T, bool context_dep>
+uint64_t LastAttributeId<T, context_dep>::s_id = 0;
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE TRAITS ============================================================
+
+namespace attr {
+
+/**
+ * This is the last-attribute-assigner. IDs are not globally
+ * unique; rather, they are unique for each table_value_type.
+ */
+template <class T, bool context_dep>
+struct AttributeTraits {
+ typedef void (*cleanup_t)(T);
+ static std::vector<cleanup_t> cleanup;
+};
+
+template <class T, bool context_dep>
+std::vector<typename AttributeTraits<T, context_dep>::cleanup_t>
+ AttributeTraits<T, context_dep>::cleanup;
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE DEFINITION ========================================================
+
+/**
+ * An "attribute type" structure.
+ *
+ * @param T the tag for the attribute kind.
+ *
+ * @param value_t the underlying value_type for the attribute kind
+ *
+ * @param CleanupStrategy Clean-up routine for associated values when the
+ * Node goes away. Useful, e.g., for pointer-valued attributes when
+ * the values are "owned" by the table.
+ *
+ * @param context_dep whether this attribute kind is
+ * context-dependent
+ */
+template <class T,
+ class value_t,
+ class CleanupStrategy = attr::NullCleanupStrategy,
+ bool context_dep = false>
+class Attribute {
+ /**
+ * The unique ID associated to this attribute. Assigned statically,
+ * at load time.
+ */
+ static const uint64_t s_id;
+
+public:
+
+ /** The value type for this attribute. */
+ typedef value_t value_type;
+
+ /** Get the unique ID associated to this attribute. */
+ static inline uint64_t getId() { return s_id; }
+
+ /**
+ * This attribute does not have a default value: calling
+ * hasAttribute() for a Node that hasn't had this attribute set will
+ * return false, and getAttribute() for the Node will return a
+ * default-constructed value_type.
+ */
+ static const bool has_default_value = false;
+
+ /**
+ * Expose this setting to the users of this Attribute kind.
+ */
+ static const bool context_dependent = context_dep;
+
+ /**
+ * Register this attribute kind and check that the ID is a valid ID
+ * for bool-valued attributes. Fail an assert if not. Otherwise
+ * return the id.
+ */
+ static inline uint64_t registerAttribute() {
+ typedef typename attr::KindValueToTableValueMapping<value_t>::
+ table_value_type table_value_type;
+ typedef attr::AttributeTraits<table_value_type, context_dep> traits;
+ uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::s_id++;
+ Assert(traits::cleanup.size() == id);// sanity check
+ traits::cleanup.push_back(attr::getCleanupStrategy<value_t,
+ CleanupStrategy>::fn);
+ return id;
+ }
+};/* class Attribute<> */
+
+/**
+ * An "attribute type" structure for boolean flags (special). The
+ * full one is below; the existence of this one disallows for boolean
+ * flag attributes with a specialized cleanup function.
+ */
+/* -- doesn't work; other specialization is "more specific" ??
+template <class T, class CleanupStrategy, bool context_dep>
+class Attribute<T, bool, CleanupStrategy, context_dep> {
+ template <bool> struct ERROR_bool_attributes_cannot_have_cleanup_functions;
+ ERROR_bool_attributes_cannot_have_cleanup_functions<true> blah;
+};
+*/
+
+/**
+ * An "attribute type" structure for boolean flags (special).
+ */
+template <class T, bool context_dep>
+class Attribute<T, bool, attr::NullCleanupStrategy, context_dep> {
+ /** IDs for bool-valued attributes are actually bit assignments. */
+ static const uint64_t s_id;
+
+public:
+
+ /** The value type for this attribute; here, bool. */
+ typedef bool value_type;
+
+ /** Get the unique ID associated to this attribute. */
+ static inline uint64_t getId() { return s_id; }
+
+ /**
+ * Such bool-valued attributes ("flags") have a default value: they
+ * are false for all nodes on entry. Calling hasAttribute() for a
+ * Node that hasn't had this attribute set will return true, and
+ * getAttribute() for the Node will return the default_value below.
+ */
+ static const bool has_default_value = true;
+
+ /**
+ * Default value of the attribute for Nodes without one explicitly
+ * set.
+ */
+ static const bool default_value = false;
+
+ /**
+ * Expose this setting to the users of this Attribute kind.
+ */
+ static const bool context_dependent = context_dep;
+
+ /**
+ * Register this attribute kind and check that the ID is a valid ID
+ * for bool-valued attributes. Fail an assert if not. Otherwise
+ * return the id.
+ */
+ static inline uint64_t registerAttribute() {
+ uint64_t id = attr::LastAttributeId<bool, context_dep>::s_id++;
+ AlwaysAssert( id <= 63,
+ "Too many boolean node attributes registered "
+ "during initialization !" );
+ return id;
+ }
+};/* class Attribute<..., bool, ...> */
+
+/**
+ * This is a context-dependent attribute kind (the only difference
+ * between CDAttribute<> and Attribute<> (with the fourth argument
+ * "true") is that you cannot supply a cleanup function (a no-op one
+ * is used).
+ */
+template <class T,
+ class value_type>
+struct CDAttribute :
+ public Attribute<T, value_type, attr::NullCleanupStrategy, true> {};
+
+/**
+ * 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. */
+// Use of the comma-operator here forces instantiation (and
+// initialization) of the AttributeTraits<> structure and its
+// "cleanup" vector before registerAttribute() is called. This is
+// important because otherwise the vector is initialized later,
+// clearing the first-pushed cleanup function.
+template <class T, class value_t, class CleanupStrategy, bool context_dep>
+const uint64_t Attribute<T, value_t, CleanupStrategy, context_dep>::s_id =
+ ( attr::AttributeTraits<typename attr::KindValueToTableValueMapping<value_t>::
+ table_value_type,
+ context_dep>::cleanup.size(),
+ Attribute<T, value_t, CleanupStrategy, context_dep>::registerAttribute() );
+
+/** Assign unique IDs to attributes at load time. */
+template <class T, bool context_dep>
+const uint64_t Attribute<T,
+ bool,
+ attr::NullCleanupStrategy, context_dep>::s_id =
+ Attribute<T, bool, attr::NullCleanupStrategy, context_dep>::
+ registerAttribute();
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR__ATTRIBUTE_INTERNALS_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback