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

1 files changed, 18 insertions, 0 deletions

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;