Context-dependent expr attributes are now attached to a specific SmtEngine, and the...

diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 2cd884bbaa118146cdb5dc9d3a8ecf493454bc68..63ea770ca2cdbd79427e71b481425831a35b347c 100644 (file)
--- 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 0bca760ef8a2a167cfa865bf81d932a37da4adcd..432fbbac9dbf3e35e62c0aefb87aaf21276b785d 100644 (file)
--- 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 8bcfd58ba7003b5d2a907ba87eb0f54f3e2d1d5e..fb9da3e3729416445b5e0f92e5cdb84ff384ce8e 100644 (file)
--- 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 49094c5937f720ba2e318ace74fbbf60da313438..deb2f69182cc255d2e12eb906813a126c9669102 100644 (file)
--- 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 35f94b9e3d86009677a9395b45d266c8c746ef71..9f0eaf3cddb76ab3fd7316d98668d43c3cfe239e 100644 (file)
--- 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 fb1284d0dfd262acb2224d8e883c5320296cd11e..31b17ccdaa19f86a8bea524aa3f89f8a9f65be74 100644 (file)
--- 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 0aa22229405a3d772263ff59e45ad913513e7de6..d4d89109c0978bfde87716e090ed9d6f9a428716 100644 (file)
--- 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 ea48cb3d03db992266d17ff169ec3e5a40b97e3c..a699528855931f596efa1158b298bfa81da5a25d 100644 (file)
--- 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 7effa521ac441645461a044723992117db0c16fd..30f84346a79dc0367a0c538b6c76efb291822f79 100644 (file)
--- 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 df60bbc33b0eb235dea3ed80e0b925456216e249..5435fba34ff917136573d742eceb5bb8b3ba2039 100644 (file)
--- 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 7321e22b4ab8d427b662118e1f540a2b5ab8e3b5..81cd5948a9ae2bfea3d3cbf97475c4c2ca58e5b1 100644 (file)
--- 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 91e12a25e8e3fe399916b54f88fb7d46b854c3cc..4daab5cce5cdf838a5f8d93a121db9399169cce5 100644 (file)
--- 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<TNode, TNode, TNodeHashFunction>(d_ctxt);
 

diff --git a/test/unit/context/stacking_vector_black.h b/test/unit/context/stacking_vector_black.h
index c7e185735d11326c9fd8dbcaf330a570066e9cf9..35305e469c394e6a7eab277007be434ffe63cfe1 100644 (file)
--- 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<TNode>(d_ctxt);
 

diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index 8fee6571d801b7749b9df6bdc0959d5e1c28c0fd..5f9a7ebce6d1ebf280663290e3932847a4a234e3 100644 (file)
--- 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 11063cd1bcb66c3af56fe51518d0105a117c767c..00ebc8b8d4e4a51e6377ca2fad021ce4121a617c 100644 (file)
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -18,7 +18,6 @@
 
 #include <string>
 
-#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<Test2, bool> 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<TypeNode, false>::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 9f8ecb69e5736f6fead9edb5361357dcbec4a1b3..7d6ee523aebf7edcbe5ffc643754228ac1632efd 100644 (file)
--- 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 c71ba48c5937d88d6186cac1ac64853b5c4c6251..9bac0d818dc4352a6c2291b4419a65c34e835346 100644 (file)
--- 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 9ca086d062b2b68fcc2fe46e526fb27e1aa0d018..b94e6a691876d23f6c7aa2ed6e017c777b6f0f27 100644 (file)
--- 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 7bc279f472fc75c9d2df0a97bd354300ede87f9f..aaa3256dda6ea0b8ae15c8bf134689ca0438ea86 100644 (file)
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -19,33 +19,28 @@
 #include <string>
 
 #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 9f90bd1b0bc81d7569b7ec3a78888f61d2b82f57..7240deed5a71d906b79364538666391e2be6c323 100644 (file)
--- a/test/unit/expr/node_self_iterator_black.h
+++ b/test/unit/expr/node_self_iterator_black.h
@@ -16,14 +16,12 @@
 
 #include <cxxtest/TestSuite.h>
 
-#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 bcb3155e1d6f26ed659c25bff388bf8048451c28..8a68db2696503e3826722bc297ce93fd8b7bc4b3 100644 (file)
--- 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 e2937ccb2f68beb6362e5925e1aff0532efac10e..db02ce20762564dd93866922e480a658d13584f9 100644 (file)
--- 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 <set>
 
 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() {