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

1 files changed, 0 insertions, 13 deletions

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;