diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-08 20:16:58 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-14 16:41:17 -0400 |
commit | ef000094d2d6a024c7eac490b241259b38e07225 (patch) | |
tree | 395250d07c9e589b1ba42316516deddfe1486018 /src/expr | |
parent | 7df24c61c7998e1485ab75219078deaf1455bd71 (diff) |
Context-dependent expr attributes are now attached to a specific SmtEngine, and the SAT context is owned by the SmtEngine.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/attribute.cpp | 37 | ||||
-rw-r--r-- | src/expr/attribute.h | 173 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 16 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 13 | ||||
-rw-r--r-- | src/expr/node.h | 2 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 24 | ||||
-rw-r--r-- | src/expr/node_manager.h | 10 |
7 files changed, 150 insertions, 125 deletions
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index 2cd884bba..63ea770ca 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -17,6 +17,7 @@ #include "expr/attribute.h" #include "expr/node_value.h" #include "util/output.h" +#include "smt/smt_engine.h" #include <utility> @@ -26,13 +27,16 @@ namespace CVC4 { namespace expr { namespace attr { -AttributeManager::AttributeManager(context::Context* ctxt) : +SmtAttributes::SmtAttributes(context::Context* ctxt) : d_cdbools(ctxt), d_cdints(ctxt), d_cdtnodes(ctxt), d_cdnodes(ctxt), d_cdstrings(ctxt), - d_cdptrs(ctxt), + d_cdptrs(ctxt) { +} + +AttributeManager::AttributeManager() : d_inGarbageCollection(false) {} @@ -40,6 +44,15 @@ bool AttributeManager::inGarbageCollection() const { return d_inGarbageCollection; } +SmtAttributes& AttributeManager::getSmtAttributes(SmtEngine* smt) { + Assert(smt != NULL); + return *smt->d_smtAttributes; +} + +const SmtAttributes& AttributeManager::getSmtAttributes(SmtEngine* smt) const { + return *smt->d_smtAttributes; +} + void AttributeManager::debugHook(int debugFlag) { /* DO NOT CHECK IN ANY CODE INTO THE DEBUG HOOKS! * debugHook() is an empty function for the purpose of debugging @@ -57,6 +70,10 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) { deleteFromTable(d_types, nv); deleteFromTable(d_strings, nv); deleteFromTable(d_ptrs, nv); +} + +void SmtAttributes::deleteAllAttributes(TNode n) { + NodeValue* nv = n.d_nv; d_cdbools.erase(nv); deleteFromTable(d_cdints, nv); @@ -74,32 +91,25 @@ void AttributeManager::deleteAllAttributes() { deleteAllFromTable(d_types); deleteAllFromTable(d_strings); deleteAllFromTable(d_ptrs); - - d_cdbools.clear(); - d_cdints.clear(); - d_cdtnodes.clear(); - d_cdnodes.clear(); - d_cdstrings.clear(); - d_cdptrs.clear(); } -void AttributeManager::deleteAttributes(const AttrIdVec& atids){ +void AttributeManager::deleteAttributes(const AttrIdVec& atids) { typedef std::map<uint64_t, std::vector< uint64_t> > AttrToVecMap; AttrToVecMap perTableIds; - for(AttrIdVec::const_iterator it = atids.begin(), it_end = atids.end(); it != it_end; ++it){ + for(AttrIdVec::const_iterator it = atids.begin(), it_end = atids.end(); it != it_end; ++it) { const AttributeUniqueId& pair = *(*it); std::vector< uint64_t>& inTable = perTableIds[pair.getTableId()]; inTable.push_back(pair.getWithinTypeId()); } AttrToVecMap::iterator it = perTableIds.begin(), it_end = perTableIds.end(); - for(; it != it_end; ++it){ + for(; it != it_end; ++it) { Assert(((*it).first) <= LastAttrTable); AttrTableId tableId = (AttrTableId) ((*it).first); std::vector< uint64_t>& ids = (*it).second; std::sort(ids.begin(), ids.end()); - switch(tableId){ + switch(tableId) { case AttrTableBool: Unimplemented("delete attributes is unimplemented for bools"); break; @@ -130,6 +140,7 @@ void AttributeManager::deleteAttributes(const AttrIdVec& atids){ case AttrTableCDPointer: Unimplemented("CDAttributes cannot be deleted. Contact Tim/Morgan if this behavior is desired."); break; + case LastAttrTable: default: Unreachable(); 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)); } diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 8bcfd58ba..fb9da3e37 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -17,7 +17,6 @@ #include "expr/node_manager.h" #include "expr/expr_manager.h" #include "expr/variable_type_map.h" -#include "context/context.h" #include "options/options.h" #include "util/statistics_registry.h" @@ -29,7 +28,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 33 "${template}" +#line 32 "${template}" #ifdef CVC4_STATISTICS_ON #define INC_STAT(kind) \ @@ -64,14 +63,12 @@ ${includes} #endif using namespace std; -using namespace CVC4::context; using namespace CVC4::kind; namespace CVC4 { ExprManager::ExprManager() : - d_ctxt(new Context()), - d_nodeManager(new NodeManager(d_ctxt, this)) { + d_nodeManager(new NodeManager(this)) { #ifdef CVC4_STATISTICS_ON for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { d_exprStatistics[i] = NULL; @@ -83,8 +80,7 @@ ExprManager::ExprManager() : } ExprManager::ExprManager(const Options& options) : - d_ctxt(new Context()), - d_nodeManager(new NodeManager(d_ctxt, this, options)) { + d_nodeManager(new NodeManager(this, options)) { #ifdef CVC4_STATISTICS_ON for (unsigned i = 0; i < LAST_TYPE; ++ i) { d_exprStatisticsVars[i] = NULL; @@ -119,8 +115,6 @@ ExprManager::~ExprManager() throw() { delete d_nodeManager; d_nodeManager = NULL; - delete d_ctxt; - d_ctxt = NULL; } catch(Exception& e) { Warning() << "CVC4 threw an exception during cleanup." << std::endl @@ -962,10 +956,6 @@ NodeManager* ExprManager::getNodeManager() const { return d_nodeManager; } -Context* ExprManager::getContext() const { - return d_ctxt; -} - Statistics ExprManager::getStatistics() const throw() { return Statistics(*d_nodeManager->getStatisticsRegistry()); } diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 49094c593..deb2f6918 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -52,19 +52,12 @@ namespace expr { }/* CVC4::expr::pickle namespace */ }/* CVC4::expr namespace */ -namespace context { - class Context; -}/* CVC4::context namespace */ - namespace stats { StatisticsRegistry* getStatisticsRegistry(ExprManager*); }/* CVC4::stats namespace */ class CVC4_PUBLIC ExprManager { private: - /** The context */ - context::Context* d_ctxt; - /** The internal node manager */ NodeManager* d_nodeManager; @@ -79,12 +72,6 @@ private: NodeManager* getNodeManager() const; /** - * Returns the internal Context. Used by internal users, i.e. the - * friend classes. - */ - context::Context* getContext() const; - - /** * Check some things about a newly-created DatatypeType. */ void checkResolvedDatatype(DatatypeType dtt) const; diff --git a/src/expr/node.h b/src/expr/node.h index 35f94b9e3..9f0eaf3cd 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -149,6 +149,7 @@ class NodeValue; namespace attr { class AttributeManager; + class SmtAttributes; }/* CVC4::expr::attr namespace */ class ExprSetDepth; @@ -214,6 +215,7 @@ class NodeTemplate { friend class NodeBuilder; friend class ::CVC4::expr::attr::AttributeManager; + friend class ::CVC4::expr::attr::SmtAttributes; friend struct ::CVC4::kind::metakind::NodeValueConstPrinter; diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index fb1284d0d..31b17ccda 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -80,12 +80,11 @@ struct NVReclaim { } }; -NodeManager::NodeManager(context::Context* ctxt, - ExprManager* exprManager) : +NodeManager::NodeManager(ExprManager* exprManager) : d_options(new Options()), d_statisticsRegistry(new StatisticsRegistry()), next_id(0), - d_attrManager(new expr::attr::AttributeManager(ctxt)), + d_attrManager(new expr::attr::AttributeManager()), d_exprManager(exprManager), d_nodeUnderDeletion(NULL), d_inReclaimZombies(false), @@ -94,13 +93,12 @@ NodeManager::NodeManager(context::Context* ctxt, init(); } -NodeManager::NodeManager(context::Context* ctxt, - ExprManager* exprManager, +NodeManager::NodeManager(ExprManager* exprManager, const Options& options) : d_options(new Options(options)), d_statisticsRegistry(new StatisticsRegistry()), next_id(0), - d_attrManager(new expr::attr::AttributeManager(ctxt)), + d_attrManager(new expr::attr::AttributeManager()), d_exprManager(exprManager), d_nodeUnderDeletion(NULL), d_inReclaimZombies(false), @@ -129,6 +127,8 @@ NodeManager::~NodeManager() { { ScopedBool dontGC(d_inReclaimZombies); + // hopefully by this point all SmtEngines have been deleted + // already, along with all their attributes d_attrManager->deleteAllAttributes(); } @@ -229,6 +229,18 @@ void NodeManager::reclaimZombies() { d_nodeUnderDeletion = nv; // remove attributes + { // notify listeners of deleted node + TNode n; + n.d_nv = nv; + nv->d_rc = 1; // so that TNode doesn't assert-fail + for(vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { + (*i)->nmNotifyDeleteNode(n); + } + // this would mean that one of the listeners stowed away + // a reference to this node! + Assert(nv->d_rc == 1); + } + nv->d_rc = 0; d_attrManager->deleteAllAttributes(nv); // decr ref counts of children diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 0aa222294..d4d89109c 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -35,7 +35,6 @@ #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node_value.h" -#include "context/context.h" #include "util/subrange_bound.h" #include "util/tls.h" #include "options/options.h" @@ -66,6 +65,11 @@ public: virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes) { } virtual void nmNotifyNewVar(TNode n, uint32_t flags) { } virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) { } + /** + * Notify a listener of a Node that's being GCed. If this function stores a reference + * to the Node somewhere, very bad things will happen. + */ + virtual void nmNotifyDeleteNode(TNode n) { } };/* class NodeManagerListener */ class NodeManager { @@ -307,8 +311,8 @@ class NodeManager { public: - explicit NodeManager(context::Context* ctxt, ExprManager* exprManager); - explicit NodeManager(context::Context* ctxt, ExprManager* exprManager, const Options& options); + explicit NodeManager(ExprManager* exprManager); + explicit NodeManager(ExprManager* exprManager, const Options& options); ~NodeManager(); /** The node manager in the current public-facing CVC4 library context */ |