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

2 files changed, 31 insertions, 1 deletions

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;