From ef000094d2d6a024c7eac490b241259b38e07225 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 8 Oct 2014 20:16:58 -0400 Subject: [PATCH] Context-dependent expr attributes are now attached to a specific SmtEngine, and the SAT context is owned by the SmtEngine. --- src/expr/attribute.cpp | 37 ++-- src/expr/attribute.h | 173 ++++++++++-------- src/expr/expr_manager_template.cpp | 16 +- src/expr/expr_manager_template.h | 13 -- src/expr/node.h | 2 + src/expr/node_manager.cpp | 24 ++- src/expr/node_manager.h | 10 +- src/smt/smt_engine.cpp | 14 +- src/smt/smt_engine.h | 18 ++ .../quantifiers/first_order_reasoning.cpp | 1 - src/theory/quantifiers/macros.cpp | 1 - test/unit/context/stacking_map_black.h | 4 +- test/unit/context/stacking_vector_black.h | 4 +- test/unit/expr/attribute_black.h | 20 +- test/unit/expr/attribute_white.h | 41 ++--- test/unit/expr/node_black.h | 6 +- test/unit/expr/node_builder_black.h | 7 +- test/unit/expr/node_manager_black.h | 7 +- test/unit/expr/node_manager_white.h | 7 +- test/unit/expr/node_self_iterator_black.h | 7 +- test/unit/expr/node_white.h | 7 +- test/unit/util/boolean_simplification_black.h | 7 +- 22 files changed, 224 insertions(+), 202 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 @@ -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 > 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 d_bools; - /** Underlying hash table for integral-valued attributes */ - AttrHash d_ints; - /** Underlying hash table for node-valued attributes */ - AttrHash d_tnodes; - /** Underlying hash table for node-valued attributes */ - AttrHash d_nodes; - /** Underlying hash table for types attributes */ - AttrHash d_types; - /** Underlying hash table for string-valued attributes */ - AttrHash d_strings; - /** Underlying hash table for pointer-valued attributes */ - AttrHash 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 d_cdptrs; - template - void deleteFromTable(AttrHash& table, NodeValue* nv); + /** Delete all attributes of given node */ + void deleteAllAttributes(TNode n); template void deleteFromTable(CDAttrHash& 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 + void deleteFromTable(AttrHash& table, NodeValue* nv); + template void deleteAllFromTable(AttrHash& 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 d_bools; + /** Underlying hash table for integral-valued attributes */ + AttrHash d_ints; + /** Underlying hash table for node-valued attributes */ + AttrHash d_tnodes; + /** Underlying hash table for node-valued attributes */ + AttrHash d_nodes; + /** Underlying hash table for types attributes */ + AttrHash d_types; + /** Underlying hash table for string-valued attributes */ + AttrHash d_strings; + /** Underlying hash table for pointer-valued attributes */ + AttrHash d_ptrs; /** * Get a particular attribute on a particular node. @@ -220,10 +239,10 @@ template <> struct getTable { static const AttrTableId id = AttrTableBool; typedef AttrHash 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 { static const AttrTableId id = AttrTableUInt64; typedef AttrHash 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 { static const AttrTableId id = AttrTableTNode; typedef AttrHash 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 { static const AttrTableId id = AttrTableNode; typedef AttrHash 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 { static const AttrTableId id = AttrTableTypeNode; typedef AttrHash 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 { static const AttrTableId id = AttrTableString; typedef AttrHash 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 struct getTable { static const AttrTableId id = AttrTablePointer; typedef AttrHash 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 struct getTable { static const AttrTableId id = AttrTablePointer; typedef AttrHash 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 { static const AttrTableId id = AttrTableCDBool; typedef CDAttrHash 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 { static const AttrTableId id = AttrTableCDUInt64; typedef CDAttrHash 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 { static const AttrTableId id = AttrTableCDTNode; typedef CDAttrHash 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 { static const AttrTableId id = AttrTableCDNode; typedef CDAttrHash 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 { static const AttrTableId id = AttrTableCDString; typedef CDAttrHash 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 struct getTable { static const AttrTableId id = AttrTableCDPointer; typedef CDAttrHash 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 struct getTable { static const AttrTableId id = AttrTableCDPointer; typedef CDAttrHash 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::get(*this); + getTable::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 { table_type; const table_type& ah = - getTable::get(*am); + getTable::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 { table_type table_type; const table_type& ah = - getTable::get(*am); + getTable::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 { table_type table_type; const table_type& ah = - getTable::get(*am); + getTable::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::get(*this); + getTable::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& table, * Obliterate a NodeValue from a (context-dependent) attribute table. */ template -inline void AttributeManager::deleteFromTable(CDAttrHash& table, - NodeValue* nv) { +inline void SmtAttributes::deleteFromTable(CDAttrHash& table, + NodeValue* nv) { for(unsigned id = 0; id < attr::LastAttributeId::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; @@ -78,12 +71,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. */ 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::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& 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 */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ea48cb3d0..a69952885 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -37,6 +37,7 @@ #include "expr/node_builder.h" #include "expr/node.h" #include "expr/node_self_iterator.h" +#include "expr/attribute.h" #include "prop/prop_engine.h" #include "proof/theory_proof.h" #include "smt/modal_exception.h" @@ -521,6 +522,10 @@ public: } } + void nmNotifyDeleteNode(TNode n) { + d_smt.d_smtAttributes->deleteAllAttributes(n); + } + Node applySubstitutions(TNode node) const { return Rewriter::rewrite(d_topLevelSubstitutions.apply(node)); } @@ -654,7 +659,7 @@ public: }/* namespace CVC4::smt */ SmtEngine::SmtEngine(ExprManager* em) throw() : - d_context(em->getContext()), + d_context(new Context()), d_userLevels(), d_userContext(new UserContext()), d_exprManager(em), @@ -684,10 +689,12 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_cumulativeResourceUsed(0), d_status(), d_private(NULL), + d_smtAttributes(NULL), d_statisticsRegistry(NULL), d_stats(NULL) { SmtScope smts(this); + d_smtAttributes = new expr::attr::SmtAttributes(d_context); d_private = new smt::SmtEnginePrivate(*this); d_statisticsRegistry = new StatisticsRegistry(); d_stats = new SmtEngineStatistics(); @@ -862,8 +869,13 @@ SmtEngine::~SmtEngine() throw() { delete d_private; d_private = NULL; + delete d_smtAttributes; + d_smtAttributes = NULL; + delete d_userContext; d_userContext = NULL; + delete d_context; + d_context = NULL; } catch(Exception& e) { Warning() << "CVC4 threw an exception during cleanup." << endl diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 7effa521a..30f84346a 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -71,6 +71,13 @@ namespace prop { class PropEngine; }/* CVC4::prop namespace */ +namespace expr { + namespace attr { + class AttributeManager; + struct SmtAttributes; + }/* CVC4::expr::attr namespace */ +}/* CVC4::expr namespace */ + namespace smt { /** * Representation of a defined function. We keep these around in @@ -342,9 +349,20 @@ class CVC4_PUBLIC SmtEngine { // to access d_modelCommands friend class ::CVC4::Model; friend class ::CVC4::theory::TheoryModel; + // to access SmtAttributes + friend class expr::attr::AttributeManager; // to access getModel(), which is private (for now) friend class GetModelCommand; + /** + * There's something of a handshake between the expr package's + * AttributeManager and the SmtEngine because the expr package + * doesn't have a Context on its own (that's owned by the + * SmtEngine). Thus all context-dependent attributes are stored + * here. + */ + expr::attr::SmtAttributes* d_smtAttributes; + StatisticsRegistry* d_statisticsRegistry; smt::SmtEngineStatistics* d_stats; diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp index df60bbc33..5435fba34 100644 --- a/src/theory/quantifiers/first_order_reasoning.cpp +++ b/src/theory/quantifiers/first_order_reasoning.cpp @@ -23,7 +23,6 @@ using namespace std; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; using namespace CVC4::kind; -using namespace CVC4::context; void FirstOrderPropagation::collectLits( Node n, std::vector & lits ){ diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 7321e22b4..81cd5948a 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -24,7 +24,6 @@ using namespace std; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; using namespace CVC4::kind; -using namespace CVC4::context; bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){ diff --git a/test/unit/context/stacking_map_black.h b/test/unit/context/stacking_map_black.h index 91e12a25e..4daab5cce 100644 --- a/test/unit/context/stacking_map_black.h +++ b/test/unit/context/stacking_map_black.h @@ -39,8 +39,8 @@ class StackingMapBlack : public CxxTest::TestSuite { public: void setUp() { - d_ctxt = new Context; - d_nm = new NodeManager(d_ctxt, NULL); + d_ctxt = new Context(); + d_nm = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nm); d_mapPtr = new StackingMap(d_ctxt); diff --git a/test/unit/context/stacking_vector_black.h b/test/unit/context/stacking_vector_black.h index c7e185735..35305e469 100644 --- a/test/unit/context/stacking_vector_black.h +++ b/test/unit/context/stacking_vector_black.h @@ -39,8 +39,8 @@ class StackingVectorBlack : public CxxTest::TestSuite { public: void setUp() { - d_ctxt = new Context; - d_nm = new NodeManager(d_ctxt, NULL); + d_ctxt = new Context(); + d_nm = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nm); d_vectorPtr = new StackingVector(d_ctxt); diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index 8fee6571d..5f9a7ebce 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -26,31 +26,35 @@ #include "expr/node_manager.h" #include "expr/node.h" #include "expr/attribute.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::context; +using namespace CVC4::smt; using namespace std; class AttributeBlack : public CxxTest::TestSuite { private: - Context* d_ctxt; + ExprManager* d_exprManager; NodeManager* d_nodeManager; - NodeManagerScope* d_scope; + SmtEngine* d_smtEngine; + SmtScope* d_scope; public: void setUp() { - d_ctxt = new Context; - d_nodeManager = new NodeManager(d_ctxt, NULL); - d_scope = new NodeManagerScope(d_nodeManager); + d_exprManager = new ExprManager(); + d_nodeManager = NodeManager::fromExprManager(d_exprManager); + d_smtEngine = new SmtEngine(d_exprManager); + d_scope = new SmtScope(d_smtEngine); } void tearDown() { delete d_scope; - delete d_nodeManager; - delete d_ctxt; + delete d_smtEngine; + delete d_exprManager; } class MyData { diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index 11063cd1b..00ebc8b8d 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -18,7 +18,6 @@ #include -#include "context/context.h" #include "expr/node_value.h" #include "expr/node_builder.h" #include "expr/node_manager.h" @@ -29,10 +28,12 @@ #include "theory/theory_engine.h" #include "theory/uf/theory_uf.h" #include "util/cvc4_assert.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::context; +using namespace CVC4::smt; using namespace CVC4::expr; using namespace CVC4::expr::attr; using namespace std; @@ -60,26 +61,27 @@ typedef CDAttribute TestFlag2cd; class AttributeWhite : public CxxTest::TestSuite { - Context* d_ctxt; + ExprManager* d_em; NodeManager* d_nm; - NodeManagerScope* d_scope; + SmtScope* d_scope; TypeNode* d_booleanType; + SmtEngine* d_smtEngine; public: void setUp() { - d_ctxt = new Context; - d_nm = new NodeManager(d_ctxt, NULL); - d_scope = new NodeManagerScope(d_nm); - + d_em = new ExprManager(); + d_nm = NodeManager::fromExprManager(d_em); + d_smtEngine = new SmtEngine(d_em); + d_scope = new SmtScope(d_smtEngine); d_booleanType = new TypeNode(d_nm->booleanType()); } void tearDown() { delete d_booleanType; delete d_scope; - delete d_nm; - delete d_ctxt; + delete d_smtEngine; + delete d_em; } void testAttributeIds() { @@ -145,7 +147,6 @@ public: lastId = attr::LastAttributeId::getId(); TS_ASSERT_LESS_THAN(TypeAttr::s_id, lastId); - } void testCDAttributes() { @@ -162,7 +163,7 @@ public: Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); - d_ctxt->push(); // level 1 + d_smtEngine->push(); // level 1 // test that all boolean flags are FALSE to start Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; @@ -204,7 +205,7 @@ public: Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); - d_ctxt->push(); // level 2 + d_smtEngine->push(); // level 2 Debug("cdboolattr") << "get flag 1 on a (should be T)\n"; TS_ASSERT(a.getAttribute(TestFlag1cd())); @@ -225,7 +226,7 @@ public: Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); - d_ctxt->push(); // level 3 + d_smtEngine->push(); // level 3 Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; TS_ASSERT(! a.getAttribute(TestFlag1cd())); @@ -244,7 +245,7 @@ public: Debug("cdboolattr") << "get flag 1 on c (should be T)\n"; TS_ASSERT(c.getAttribute(TestFlag1cd())); - d_ctxt->pop(); // level 2 + d_smtEngine->pop(); // level 2 Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; TS_ASSERT(! a.getAttribute(TestFlag1cd())); @@ -253,7 +254,7 @@ public: Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); - d_ctxt->pop(); // level 1 + d_smtEngine->pop(); // level 1 Debug("cdboolattr") << "get flag 1 on a (should be T)\n"; TS_ASSERT(a.getAttribute(TestFlag1cd())); @@ -262,7 +263,7 @@ public: Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); - d_ctxt->pop(); // level 0 + d_smtEngine->pop(); // level 0 Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; TS_ASSERT(! a.getAttribute(TestFlag1cd())); @@ -271,13 +272,11 @@ public: Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); -#ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( d_ctxt->pop(), AssertionException ); -#endif /* CVC4_ASSERTIONS */ + TS_ASSERT_THROWS( d_smtEngine->pop(), ModalException ); } void testAttributes() { - //Debug.on("bootattr"); + //Debug.on("boolattr"); Node a = d_nm->mkVar(*d_booleanType); Node b = d_nm->mkVar(*d_booleanType); diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 9f8ecb69e..7d6ee523a 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -28,14 +28,12 @@ using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::context; using namespace std; class NodeBlack : public CxxTest::TestSuite { private: Options opts; - Context* d_ctxt; NodeManager* d_nodeManager; NodeManagerScope* d_scope; TypeNode* d_booleanType; @@ -51,8 +49,7 @@ public: free(argv[0]); free(argv[1]); - d_ctxt = new Context(); - d_nodeManager = new NodeManager(d_ctxt, NULL, opts); + d_nodeManager = new NodeManager(NULL, opts); d_scope = new NodeManagerScope(d_nodeManager); d_booleanType = new TypeNode(d_nodeManager->booleanType()); d_realType = new TypeNode(d_nodeManager->realType()); @@ -62,7 +59,6 @@ public: delete d_booleanType; delete d_scope; delete d_nodeManager; - delete d_ctxt; } bool imp(bool a, bool b) const { diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index c71ba48c5..9bac0d818 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -25,19 +25,16 @@ #include "expr/node_manager.h" #include "expr/node.h" #include "expr/kind.h" -#include "context/context.h" #include "util/cvc4_assert.h" #include "util/rational.h" using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::context; using namespace std; class NodeBuilderBlack : public CxxTest::TestSuite { private: - Context* d_ctxt; NodeManager* d_nm; NodeManagerScope* d_scope; TypeNode* d_booleanType; @@ -47,8 +44,7 @@ private: public: void setUp() { - d_ctxt = new Context; - d_nm = new NodeManager(d_ctxt, NULL); + d_nm = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nm); specKind = AND; @@ -63,7 +59,6 @@ public: delete d_realType; delete d_scope; delete d_nm; - delete d_ctxt; } diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index 9ca086d06..b94e6a691 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -21,7 +21,6 @@ #include "expr/node_manager.h" #include "expr/node_manager_attributes.h" -#include "context/context.h" #include "util/rational.h" #include "util/integer.h" @@ -29,26 +28,22 @@ using namespace CVC4; using namespace CVC4::expr; using namespace CVC4::kind; -using namespace CVC4::context; class NodeManagerBlack : public CxxTest::TestSuite { - Context* d_context; NodeManager* d_nodeManager; NodeManagerScope* d_scope; public: void setUp() { - d_context = new Context; - d_nodeManager = new NodeManager(d_context, NULL); + d_nodeManager = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nodeManager); } void tearDown() { delete d_scope; delete d_nodeManager; - delete d_context; } void testMkNodeNot() { diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h index 7bc279f47..aaa3256dd 100644 --- a/test/unit/expr/node_manager_white.h +++ b/test/unit/expr/node_manager_white.h @@ -19,33 +19,28 @@ #include #include "expr/node_manager.h" -#include "context/context.h" #include "util/rational.h" #include "util/integer.h" using namespace CVC4; using namespace CVC4::expr; -using namespace CVC4::context; class NodeManagerWhite : public CxxTest::TestSuite { - Context* d_ctxt; NodeManager* d_nm; NodeManagerScope* d_scope; public: void setUp() { - d_ctxt = new Context(); - d_nm = new NodeManager(d_ctxt, NULL); + d_nm = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nm); } void tearDown() { delete d_scope; delete d_nm; - delete d_ctxt; } void testMkConstRational() { diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h index 9f90bd1b0..7240deed5 100644 --- a/test/unit/expr/node_self_iterator_black.h +++ b/test/unit/expr/node_self_iterator_black.h @@ -16,14 +16,12 @@ #include -#include "context/context.h" #include "expr/node.h" #include "expr/node_self_iterator.h" #include "expr/node_builder.h" #include "expr/convenience_node_builders.h" using namespace CVC4; -using namespace CVC4::context; using namespace CVC4::kind; using namespace CVC4::expr; using namespace std; @@ -31,7 +29,6 @@ using namespace std; class NodeSelfIteratorBlack : public CxxTest::TestSuite { private: - Context* d_ctxt; NodeManager* d_nodeManager; NodeManagerScope* d_scope; TypeNode* d_booleanType; @@ -40,8 +37,7 @@ private: public: void setUp() { - d_ctxt = new Context; - d_nodeManager = new NodeManager(d_ctxt, NULL); + d_nodeManager = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nodeManager); d_booleanType = new TypeNode(d_nodeManager->booleanType()); d_realType = new TypeNode(d_nodeManager->realType()); @@ -51,7 +47,6 @@ public: delete d_booleanType; delete d_scope; delete d_nodeManager; - delete d_ctxt; } void testSelfIteration() { diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index bcb3155e1..8a68db269 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -22,33 +22,28 @@ #include "expr/node_builder.h" #include "expr/node_manager.h" #include "expr/node.h" -#include "context/context.h" #include "util/cvc4_assert.h" using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::context; using namespace CVC4::expr; using namespace std; class NodeWhite : public CxxTest::TestSuite { - Context* d_ctxt; NodeManager* d_nm; NodeManagerScope* d_scope; public: void setUp() { - d_ctxt = new Context(); - d_nm = new NodeManager(d_ctxt, NULL); + d_nm = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nm); } void tearDown() { delete d_scope; delete d_nm; - delete d_ctxt; } void testNull() { diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h index e2937ccb2..db02ce207 100644 --- a/test/unit/util/boolean_simplification_black.h +++ b/test/unit/util/boolean_simplification_black.h @@ -14,7 +14,6 @@ ** Black box testing of CVC4::BooleanSimplification. **/ -#include "context/context.h" #include "util/language.h" #include "expr/node.h" #include "expr/kind.h" @@ -26,12 +25,10 @@ #include using namespace CVC4; -using namespace CVC4::context; using namespace std; class BooleanSimplificationBlack : public CxxTest::TestSuite { - Context* d_context; NodeManager* d_nm; NodeManagerScope* d_scope; @@ -70,8 +67,7 @@ class BooleanSimplificationBlack : public CxxTest::TestSuite { public: void setUp() { - d_context = new Context(); - d_nm = new NodeManager(d_context, NULL); + d_nm = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nm); a = d_nm->mkSkolem("a", d_nm->booleanType()); @@ -116,7 +112,6 @@ public: delete d_scope; delete d_nm; - delete d_context; } void testNegate() { -- 2.30.2