diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-22 07:40:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-22 07:40:23 +0000 |
commit | 6bdd652a8511df2f341b30daec60d5402986ed5b (patch) | |
tree | 0f506a4d2993f9d9cae70420af3cb58b3ca6b784 /src | |
parent | 69d6fcbf56ed823461189f2488e5c2b2f44dca02 (diff) |
resolve bug 32; public-facing interface functions in expr package must set current NodeManager
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/expr.cpp | 6 | ||||
-rw-r--r-- | src/expr/expr.h | 4 | ||||
-rw-r--r-- | src/expr/expr_manager.h | 27 | ||||
-rw-r--r-- | src/expr/node_manager.h | 4 |
4 files changed, 36 insertions, 5 deletions
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index 032735ff0..18c0fdbab 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -43,11 +43,13 @@ ExprManager* Expr::getExprManager() const { } Expr::~Expr() { + ExprManagerScope ems(*this); delete d_node; } Expr& Expr::operator=(const Expr& e) { if(this != &e) { + ExprManagerScope ems(*this); delete d_node; d_node = new Node(*e.d_node); d_em = e.d_em; @@ -79,7 +81,7 @@ bool Expr::operator<(const Expr& e) const { size_t Expr::hash() const { Assert(d_node != NULL, "Unexpected NULL expression pointer!"); - return (d_node->isNull()); + return (d_node->hash()); } Kind Expr::getKind() const { @@ -93,6 +95,7 @@ size_t Expr::getNumChildren() const { } std::string Expr::toString() const { + ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); return d_node->toString(); } @@ -107,6 +110,7 @@ Expr::operator bool() const { } void Expr::toStream(std::ostream& out) const { + ExprManagerScope ems(*this); d_node->toStream(out); } diff --git a/src/expr/expr.h b/src/expr/expr.h index 0943c13e4..dd4d0e9d7 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -13,11 +13,13 @@ ** Public-facing expression interface. **/ +// circular dependency: force expr_manager.h first +#include "expr/expr_manager.h" + #ifndef __CVC4__EXPR_H #define __CVC4__EXPR_H #include "cvc4_config.h" -#include "expr/expr_manager.h" #include <string> #include <iostream> diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index 5bfef2aa7..edfc18c8d 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -18,6 +18,7 @@ #include "cvc4_config.h" #include "expr/kind.h" +#include "expr/node_manager.h" #include <vector> namespace CVC4 { @@ -27,7 +28,6 @@ class Type; class BooleanType; class FunctionType; class KindType; -class NodeManager; class SmtEngine; class CVC4_PUBLIC ExprManager { @@ -118,8 +118,31 @@ private: /** SmtEngine will use all the internals, so it will grab the node manager */ friend class SmtEngine; + + /** ExprManagerScope reaches in to get the NodeManager */ + friend class ExprManagerScope; }; -} +}/* CVC4 namespace */ + +#include "expr/expr.h" + +namespace CVC4 { + +/** + * A wrapper (essentially) for NodeManagerScope. Without this, we'd + * need Expr to be a friend of ExprManager. + */ +class ExprManagerScope { + NodeManagerScope d_nms; +public: + inline ExprManagerScope(const Expr& e) : + d_nms(e.getExprManager() == NULL ? + NodeManager::currentNM() : e.getExprManager()->getNodeManager()) { + } +}; + +}/* CVC4 namespace */ #endif /* __CVC4__EXPR_MANAGER_H */ + diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 2862203db..18a95f041 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -13,6 +13,9 @@ ** A manager for Nodes. **/ +/* circular dependency; force node.h first */ +#include "expr/node.h" + #ifndef __CVC4__NODE_MANAGER_H #define __CVC4__NODE_MANAGER_H @@ -20,7 +23,6 @@ #include <string> #include <ext/hash_set> -#include "expr/node.h" #include "expr/kind.h" namespace __gnu_cxx { |