Context-dependent expr attributes are now attached to a specific SmtEngine, and the SAT context is owned by the SmtEngine.

11 files changed, 181 insertions, 128 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 */
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<Node> & 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 ){