diff options
| -rw-r--r-- | src/expr/attribute.h | 17 | ||||
| -rw-r--r-- | src/expr/attribute_internals.h | 34 |
2 files changed, 45 insertions, 6 deletions
diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 46302fc9f..44bf7aae5 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -61,7 +61,7 @@ class AttributeManager { * getTable<> is a helper template that gets the right table from an * AttributeManager given its type. */ - template <class T, bool context_dep> + template <class T, bool context_dep, class Enable> friend struct getTable; bool d_inGarbageCollection; @@ -190,8 +190,13 @@ namespace attr { /** * The getTable<> template provides (static) access to the * AttributeManager field holding the table. + * + * The `Enable` template parameter is used to instantiate the template + * conditionally: If the template substitution of Enable fails (e.g. when using + * `std::enable_if` in the template parameter and the condition is false), the + * instantiation is ignored due to the SFINAE rule. */ -template <class T, bool context_dep> +template <class T, bool context_dep, class Enable = void> struct getTable; /** Access the "d_bools" member of AttributeManager. */ @@ -208,8 +213,12 @@ struct getTable<bool, false> { }; /** Access the "d_ints" member of AttributeManager. */ -template <> -struct getTable<uint64_t, false> { +template <class T> +struct getTable<T, + false, + // Use this specialization only for unsigned integers + typename std::enable_if<std::is_unsigned<T>::value>::type> +{ static const AttrTableId id = AttrTableUInt64; typedef AttrHash<uint64_t> table_type; static inline table_type& get(AttributeManager& am) { diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index bc34324b0..94d51b188 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -91,9 +91,15 @@ namespace attr { * * This general (non-specialized) implementation of the template does * nothing. + * + * The `Enable` template parameter is used to instantiate the template + * conditionally: If the template substitution of Enable fails (e.g. when using + * `std::enable_if` in the template parameter and the condition is false), the + * instantiation is ignored due to the SFINAE rule. */ -template <class T> -struct KindValueToTableValueMapping { +template <class T, class Enable = void> +struct KindValueToTableValueMapping +{ /** Simple case: T == table_value_type */ typedef T table_value_type; /** No conversion necessary */ @@ -102,6 +108,30 @@ struct KindValueToTableValueMapping { inline static T convertBack(const T& t) { return t; } }; +/** + * This converts arbitrary unsigned integers (up to 64-bit) to and from 64-bit + * integers s.t. they can be stored in the hash table for integral-valued + * attributes. + */ +template <class T> +struct KindValueToTableValueMapping< + T, + // Use this specialization only for unsigned integers + typename std::enable_if<std::is_unsigned<T>::value>::type> +{ + typedef uint64_t table_value_type; + /** Convert from unsigned integer to uint64_t */ + static uint64_t convert(const T& t) + { + static_assert(sizeof(T) <= sizeof(uint64_t), + "Cannot store integer attributes of a bit-width that is " + "greater than 64-bits"); + return static_cast<uint64_t>(t); + } + /** Convert from uint64_t to unsigned integer */ + static T convertBack(const uint64_t& t) { return static_cast<T>(t); } +}; + }/* CVC4::expr::attr namespace */ // ATTRIBUTE HASH TABLES ======================================================= |