diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-08 20:16:58 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-14 16:41:17 -0400 |
commit | ef000094d2d6a024c7eac490b241259b38e07225 (patch) | |
tree | 395250d07c9e589b1ba42316516deddfe1486018 /src/expr/expr_manager_template.h | |
parent | 7df24c61c7998e1485ab75219078deaf1455bd71 (diff) |
Context-dependent expr attributes are now attached to a specific SmtEngine, and the SAT context is owned by the SmtEngine.
Diffstat (limited to 'src/expr/expr_manager_template.h')
-rw-r--r-- | src/expr/expr_manager_template.h | 13 |
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; |