diff options
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 82 |
1 files changed, 4 insertions, 78 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index d113c1458..348200b6e 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -22,8 +22,6 @@ //#include "expr/attribute.h" #include "expr/node.h" #include "expr/type_node.h" -#include "expr/expr.h" -#include "expr/expr_manager.h" #ifndef CVC4__NODE_MANAGER_H #define CVC4__NODE_MANAGER_H @@ -90,9 +88,6 @@ class NodeManager friend class api::Solver; friend class expr::NodeValue; friend class expr::TypeChecker; - // friends so they can access mkVar() here, which is private - friend Expr ExprManager::mkVar(const std::string&, Type); - friend Expr ExprManager::mkVar(Type); template <unsigned nchild_thresh> friend class NodeBuilder; @@ -134,9 +129,6 @@ class NodeManager expr::attr::AttributeManager* d_attrManager; - /** The associated ExprManager */ - ExprManager* d_exprManager; - /** * The node value we're currently freeing. This unique node value * is permitted to have outstanding TNodes to it (in "soft" @@ -292,14 +284,10 @@ class NodeManager // `d_zombies` uses the node id to hash and compare nodes. If `d_zombies` // already contains a node value with the same id as `nv`, but the pointers // are different, then the wrong `NodeManager` was in scope for one of the - // two nodes when it reached refcount zero. This can happen for example if - // you create a node with a `NodeManager` n1 and then call `Node::toExpr()` - // on that node while a different `NodeManager` n2 is in scope. When that - // `Expr` is deleted and the node reaches refcount zero in the `Expr`'s - // destructor, then `markForDeletion()` will be called on n2. + // two nodes when it reached refcount zero. Assert(d_zombies.find(nv) == d_zombies.end() || *d_zombies.find(nv) == nv); - d_zombies.insert(nv); // FIXME multithreading + d_zombies.insert(nv); if(safeToReclaimZombies()) { if(d_zombies.size() > 5000) { @@ -392,8 +380,7 @@ class NodeManager Node* mkVarPtr(const TypeNode& type); public: - - explicit NodeManager(ExprManager* exprManager); + explicit NodeManager(); ~NodeManager(); /** The node manager in the current public-facing CVC4 library context */ @@ -1103,37 +1090,6 @@ class NodeManager */ TypeNode getType(TNode n, bool check = false); - /** - * Convert a node to an expression. Uses the ExprManager - * associated to this NodeManager. - */ - inline Expr toExpr(TNode n); - - /** - * Convert an expression to a node. - */ - static inline Node fromExpr(const Expr& e); - - /** - * Convert a node manager to an expression manager. - */ - inline ExprManager* toExprManager(); - - /** - * Convert an expression manager to a node manager. - */ - static inline NodeManager* fromExprManager(ExprManager* exprManager); - - /** - * Convert a type node to a type. - */ - inline Type toType(const TypeNode& tn); - - /** - * Convert a type to a type node. - */ - static inline TypeNode fromType(Type t); - /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/ void reclaimZombiesUntil(uint32_t k); @@ -1165,8 +1121,7 @@ class NodeManager * public-interface calls into the CVC4 library, where CVC4's notion * of the "current" <code>NodeManager</code> should be set to match * the calling context. See, for example, the implementations of - * public calls in the <code>ExprManager</code> and - * <code>SmtEngine</code> classes. + * public calls in the <code>SmtEngine</code> class. * * The client must be careful to create and destroy * <code>NodeManagerScope</code> objects in a well-nested manner (such @@ -1183,10 +1138,6 @@ class NodeManagerScope { public: NodeManagerScope(NodeManager* nm) : d_oldNodeManager(NodeManager::s_current) { - // There are corner cases where nm can be NULL and it's ok. - // For example, if you write { Expr e; }, then when the null - // Expr is destructed, there's no active node manager. - // Assert(nm != NULL); NodeManager::s_current = nm; Debug("current") << "node manager scope: " << NodeManager::s_current << "\n"; } @@ -1274,31 +1225,6 @@ inline void NodeManager::poolRemove(expr::NodeValue* nv) { d_nodeValuePool.erase(nv);// FIXME multithreading } -inline Expr NodeManager::toExpr(TNode n) { - return Expr(d_exprManager, new Node(n)); -} - -inline Node NodeManager::fromExpr(const Expr& e) { - return e.getNode(); -} - -inline ExprManager* NodeManager::toExprManager() { - return d_exprManager; -} - -inline NodeManager* NodeManager::fromExprManager(ExprManager* exprManager) { - return exprManager->getNodeManager(); -} - -inline Type NodeManager::toType(const TypeNode& tn) -{ - return Type(this, new TypeNode(tn)); -} - -inline TypeNode NodeManager::fromType(Type t) { - return *Type::getTypeNode(t); -} - }/* CVC4 namespace */ #define CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP |