diff options
Diffstat (limited to 'src/expr/attribute.h')
-rw-r--r-- | src/expr/attribute.h | 173 |
1 files changed, 96 insertions, 77 deletions
diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 0bca760ef..432fbbac9 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -20,6 +20,7 @@ * attributes and nodes due to template use */ #include "expr/node.h" #include "expr/type_node.h" +#include "context/context.h" #ifndef __CVC4__EXPR__ATTRIBUTE_H #define __CVC4__EXPR__ATTRIBUTE_H @@ -34,34 +35,20 @@ #undef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H namespace CVC4 { + +class SmtEngine; + +namespace smt { + extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current; +}/* CVC4::smt namespace */ + namespace expr { namespace attr { // ATTRIBUTE MANAGER =========================================================== -/** - * A container for the main attribute tables of the system. There's a - * one-to-one NodeManager : AttributeManager correspondence. - */ -class AttributeManager { - - // IF YOU ADD ANY TABLES, don't forget to add them also to the - // implementation of deleteAllAttributes(). - - /** Underlying hash table for boolean-valued attributes */ - AttrHash<bool> d_bools; - /** Underlying hash table for integral-valued attributes */ - AttrHash<uint64_t> d_ints; - /** Underlying hash table for node-valued attributes */ - AttrHash<TNode> d_tnodes; - /** Underlying hash table for node-valued attributes */ - AttrHash<Node> d_nodes; - /** Underlying hash table for types attributes */ - 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; +struct SmtAttributes { + SmtAttributes(context::Context*); // IF YOU ADD ANY TABLES, don't forget to add them also to the // implementation of deleteAllAttributes(). @@ -79,12 +66,23 @@ class AttributeManager { /** Underlying hash table for context-dependent pointer-valued attributes */ CDAttrHash<void*> d_cdptrs; - template <class T> - void deleteFromTable(AttrHash<T>& table, NodeValue* nv); + /** Delete all attributes of given node */ + void deleteAllAttributes(TNode n); template <class T> void deleteFromTable(CDAttrHash<T>& table, NodeValue* nv); +};/* struct SmtAttributes */ + +/** + * A container for the main attribute tables of the system. There's a + * one-to-one NodeManager : AttributeManager correspondence. + */ +class AttributeManager { + + template <class T> + void deleteFromTable(AttrHash<T>& table, NodeValue* nv); + template <class T> void deleteAllFromTable(AttrHash<T>& table); @@ -105,10 +103,31 @@ class AttributeManager { void clearDeleteAllAttributesBuffer(); + SmtAttributes& getSmtAttributes(SmtEngine*); + const SmtAttributes& getSmtAttributes(SmtEngine*) const; + public: /** Construct an attribute manager. */ - AttributeManager(context::Context* ctxt); + AttributeManager(); + + // IF YOU ADD ANY TABLES, don't forget to add them also to the + // implementation of deleteAllAttributes(). + + /** Underlying hash table for boolean-valued attributes */ + AttrHash<bool> d_bools; + /** Underlying hash table for integral-valued attributes */ + AttrHash<uint64_t> d_ints; + /** Underlying hash table for node-valued attributes */ + AttrHash<TNode> d_tnodes; + /** Underlying hash table for node-valued attributes */ + AttrHash<Node> d_nodes; + /** Underlying hash table for types attributes */ + 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. @@ -220,10 +239,10 @@ template <> struct getTable<bool, false> { static const AttrTableId id = AttrTableBool; typedef AttrHash<bool> table_type; - static inline table_type& get(AttributeManager& am) { + static inline table_type& get(AttributeManager& am, SmtEngine* smt) { return am.d_bools; } - static inline const table_type& get(const AttributeManager& am) { + static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { return am.d_bools; } }; @@ -233,10 +252,10 @@ template <> struct getTable<uint64_t, false> { static const AttrTableId id = AttrTableUInt64; typedef AttrHash<uint64_t> table_type; - static inline table_type& get(AttributeManager& am) { + static inline table_type& get(AttributeManager& am, SmtEngine* smt) { return am.d_ints; } - static inline const table_type& get(const AttributeManager& am) { + static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { return am.d_ints; } }; @@ -246,10 +265,10 @@ template <> struct getTable<TNode, false> { static const AttrTableId id = AttrTableTNode; typedef AttrHash<TNode> table_type; - static inline table_type& get(AttributeManager& am) { + static inline table_type& get(AttributeManager& am, SmtEngine* smt) { return am.d_tnodes; } - static inline const table_type& get(const AttributeManager& am) { + static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { return am.d_tnodes; } }; @@ -259,10 +278,10 @@ template <> struct getTable<Node, false> { static const AttrTableId id = AttrTableNode; typedef AttrHash<Node> table_type; - static inline table_type& get(AttributeManager& am) { + static inline table_type& get(AttributeManager& am, SmtEngine* smt) { return am.d_nodes; } - static inline const table_type& get(const AttributeManager& am) { + static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { return am.d_nodes; } }; @@ -272,10 +291,10 @@ template <> struct getTable<TypeNode, false> { static const AttrTableId id = AttrTableTypeNode; typedef AttrHash<TypeNode> table_type; - static inline table_type& get(AttributeManager& am) { + static inline table_type& get(AttributeManager& am, SmtEngine* smt) { return am.d_types; } - static inline const table_type& get(const AttributeManager& am) { + static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { return am.d_types; } }; @@ -285,10 +304,10 @@ template <> struct getTable<std::string, false> { static const AttrTableId id = AttrTableString; typedef AttrHash<std::string> table_type; - static inline table_type& get(AttributeManager& am) { + static inline table_type& get(AttributeManager& am, SmtEngine* smt) { return am.d_strings; } - static inline const table_type& get(const AttributeManager& am) { + static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { return am.d_strings; } }; @@ -298,10 +317,10 @@ template <class T> struct getTable<T*, false> { static const AttrTableId id = AttrTablePointer; typedef AttrHash<void*> table_type; - static inline table_type& get(AttributeManager& am) { + static inline table_type& get(AttributeManager& am, SmtEngine* smt) { return am.d_ptrs; } - static inline const table_type& get(const AttributeManager& am) { + static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { return am.d_ptrs; } }; @@ -311,10 +330,10 @@ 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) { + static inline table_type& get(AttributeManager& am, SmtEngine* smt) { return am.d_ptrs; } - static inline const table_type& get(const AttributeManager& am) { + static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { return am.d_ptrs; } }; @@ -324,11 +343,11 @@ template <> struct getTable<bool, true> { static const AttrTableId id = AttrTableCDBool; typedef CDAttrHash<bool> table_type; - static inline table_type& get(AttributeManager& am) { - return am.d_cdbools; + static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + return am.getSmtAttributes(smt).d_cdbools; } - static inline const table_type& get(const AttributeManager& am) { - return am.d_cdbools; + static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + return am.getSmtAttributes(smt).d_cdbools; } }; @@ -337,11 +356,11 @@ template <> struct getTable<uint64_t, true> { static const AttrTableId id = AttrTableCDUInt64; typedef CDAttrHash<uint64_t> table_type; - static inline table_type& get(AttributeManager& am) { - return am.d_cdints; + static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + return am.getSmtAttributes(smt).d_cdints; } - static inline const table_type& get(const AttributeManager& am) { - return am.d_cdints; + static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + return am.getSmtAttributes(smt).d_cdints; } }; @@ -350,11 +369,11 @@ template <> struct getTable<TNode, true> { static const AttrTableId id = AttrTableCDTNode; typedef CDAttrHash<TNode> table_type; - static inline table_type& get(AttributeManager& am) { - return am.d_cdtnodes; + static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + return am.getSmtAttributes(smt).d_cdtnodes; } - static inline const table_type& get(const AttributeManager& am) { - return am.d_cdtnodes; + static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + return am.getSmtAttributes(smt).d_cdtnodes; } }; @@ -363,11 +382,11 @@ template <> struct getTable<Node, true> { static const AttrTableId id = AttrTableCDNode; typedef CDAttrHash<Node> table_type; - static inline table_type& get(AttributeManager& am) { - return am.d_cdnodes; + static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + return am.getSmtAttributes(smt).d_cdnodes; } - static inline const table_type& get(const AttributeManager& am) { - return am.d_cdnodes; + static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + return am.getSmtAttributes(smt).d_cdnodes; } }; @@ -376,11 +395,11 @@ template <> struct getTable<std::string, true> { static const AttrTableId id = AttrTableCDString; typedef CDAttrHash<std::string> table_type; - static inline table_type& get(AttributeManager& am) { - return am.d_cdstrings; + static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + return am.getSmtAttributes(smt).d_cdstrings; } - static inline const table_type& get(const AttributeManager& am) { - return am.d_cdstrings; + static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + return am.getSmtAttributes(smt).d_cdstrings; } }; @@ -389,11 +408,11 @@ template <class T> struct getTable<T*, true> { static const AttrTableId id = AttrTableCDPointer; typedef CDAttrHash<void*> table_type; - static inline table_type& get(AttributeManager& am) { - return am.d_cdptrs; + static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + return am.getSmtAttributes(smt).d_cdptrs; } - static inline const table_type& get(const AttributeManager& am) { - return am.d_cdptrs; + static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + return am.getSmtAttributes(smt).d_cdptrs; } }; @@ -402,11 +421,11 @@ template <class T> struct getTable<const T*, true> { static const AttrTableId id = AttrTableCDPointer; typedef CDAttrHash<void*> table_type; - static inline table_type& get(AttributeManager& am) { - return am.d_cdptrs; + static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + return am.getSmtAttributes(smt).d_cdptrs; } - static inline const table_type& get(const AttributeManager& am) { - return am.d_cdptrs; + static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + return am.getSmtAttributes(smt).d_cdptrs; } }; @@ -426,7 +445,7 @@ AttributeManager::getAttribute(NodeValue* nv, const AttrKind&) const { table_type table_type; const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*this); + getTable<value_type, AttrKind::context_dependent>::get(*this, smt::s_smtEngine_current); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -469,7 +488,7 @@ struct HasAttribute<true, AttrKind> { table_type; const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*am); + getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -497,7 +516,7 @@ struct HasAttribute<false, AttrKind> { table_type table_type; const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*am); + getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -517,7 +536,7 @@ struct HasAttribute<false, AttrKind> { table_type table_type; const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*am); + getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -557,7 +576,7 @@ AttributeManager::setAttribute(NodeValue* nv, table_type table_type; table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*this); + getTable<value_type, AttrKind::context_dependent>::get(*this, smt::s_smtEngine_current); ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value); } @@ -590,8 +609,8 @@ inline void AttributeManager::deleteFromTable(AttrHash<T>& table, * Obliterate a NodeValue from a (context-dependent) attribute table. */ template <class T> -inline void AttributeManager::deleteFromTable(CDAttrHash<T>& table, - NodeValue* nv) { +inline void SmtAttributes::deleteFromTable(CDAttrHash<T>& table, + NodeValue* nv) { for(unsigned id = 0; id < attr::LastAttributeId<T, true>::getId(); ++id) { table.obliterate(std::make_pair(id, nv)); } |