From e45de2ba8a8c34d3212327ed6f021462c149825c Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 15 Apr 2011 22:11:11 +0000 Subject: [PATCH] partial merge from portfolio branch, adding conversions (library-internal-only of course) between Exprs and Nodes, Types and TypeNodes, ExprManagers and NodeManagers. --- src/expr/expr_manager_template.cpp | 14 +++---- src/expr/expr_manager_template.h | 6 ++- src/expr/expr_template.h | 1 + src/expr/node.h | 28 +++++++++++++ src/expr/node_manager.cpp | 17 +++++++- src/expr/node_manager.h | 66 ++++++++++++++++++++++++++++-- src/expr/type.cpp | 4 ++ src/expr/type.h | 6 +++ 8 files changed, 129 insertions(+), 13 deletions(-) diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 5d34fb53c..6e8b6c63c 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -57,7 +57,7 @@ ${includes} } \ ++ *(d_exprStatisticsVars[type]); \ } -#else +#else #define INC_STAT(kind) #define INC_STAT_VAR(type) #endif @@ -70,8 +70,8 @@ namespace CVC4 { ExprManager::ExprManager() : d_ctxt(new Context), - d_nodeManager(new NodeManager(d_ctxt)) { -#ifdef CVC4_STATISTICS_ON + d_nodeManager(new NodeManager(d_ctxt, this)) { +#ifdef CVC4_STATISTICS_ON for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { d_exprStatistics[i] = NULL; } @@ -83,8 +83,8 @@ ExprManager::ExprManager() : ExprManager::ExprManager(const Options& options) : d_ctxt(new Context), - d_nodeManager(new NodeManager(d_ctxt, options)) { -#ifdef CVC4_STATISTICS_ON + d_nodeManager(new NodeManager(d_ctxt, this, options)) { +#ifdef CVC4_STATISTICS_ON for (unsigned i = 0; i <= LAST_TYPE; ++ i) { d_exprStatisticsVars[i] = NULL; } @@ -95,7 +95,7 @@ ExprManager::ExprManager(const Options& options) : } ExprManager::~ExprManager() { -#ifdef CVC4_STATISTICS_ON +#ifdef CVC4_STATISTICS_ON NodeManagerScope nms(d_nodeManager); for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { if (d_exprStatistics[i] != NULL) { @@ -135,7 +135,7 @@ IntegerType ExprManager::integerType() const { } Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { - const unsigned n = 1; + const unsigned n = 1; CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, "Exprs with kind %s must have at least %u children and " "at most %u children (the one under construction has %u)", diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 83d306871..f51d6fa28 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -80,8 +80,12 @@ private: /** ExprManagerScope reaches in to get the NodeManager */ friend class ExprManagerScope; - // undefined, private copy constructor (disallow copy) + /** NodeManager reaches in to get the NodeManager */ + friend class NodeManager; + + // undefined, private copy constructor and assignment op (disallow copy) ExprManager(const ExprManager&) CVC4_UNDEFINED; + ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED; public: diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index ba695355e..1a9722939 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -430,6 +430,7 @@ protected: friend class SmtEngine; friend class smt::SmtEnginePrivate; friend class ExprManager; + friend class NodeManager; friend class TypeCheckingException; friend std::ostream& operator<<(std::ostream& out, const Expr& e); template friend class NodeTemplate; diff --git a/src/expr/node.h b/src/expr/node.h index d67bc2e2b..2509640e0 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -371,6 +371,22 @@ public: // bool containsDecision(); // is "atomic" // bool properlyContainsDecision(); // maybe not atomic but all children are + /** + * Convert this Node into an Expr using the currently-in-scope + * manager. Essentially this is like an "operator Expr()" but we + * don't want it to compete with implicit conversions between e.g. + * Node and TNode, and we want internal-to-external interface + * (Node -> Expr) points to be explicit. We could write an + * explicit Expr(Node) constructor---but that dirties the public + * interface. + */ + inline Expr toExpr(); + + /** + * Convert an Expr into a Node. + */ + static inline Node fromExpr(const Expr& e); + /** * Returns true if this node represents a constant * @return true if const @@ -1176,6 +1192,18 @@ Node NodeTemplate::substitute(Iterator1 nodesBegin, } } +template +inline Expr NodeTemplate::toExpr() { + assertTNodeNotExpired(); + return NodeManager::currentNM()->toExpr(*this); +} + +// intentionally not defined for TNode +template <> +inline Node NodeTemplate::fromExpr(const Expr& e) { + return NodeManager::fromExpr(e); +} + #ifdef CVC4_DEBUG /** * Pretty printer for use within gdb. This is not intended to be used diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 207f1f492..793b701f8 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -84,23 +84,27 @@ struct NVReclaim { } }; -NodeManager::NodeManager(context::Context* ctxt) : +NodeManager::NodeManager(context::Context* ctxt, + ExprManager* exprManager) : d_optionsAllocated(new Options()), d_options(d_optionsAllocated), d_statisticsRegistry(new StatisticsRegistry()), d_attrManager(ctxt), + d_exprManager(exprManager), d_nodeUnderDeletion(NULL), d_inReclaimZombies(false) { init(); } -NodeManager::NodeManager(context::Context* ctxt, +NodeManager::NodeManager(context::Context* ctxt, + ExprManager* exprManager, const Options& options) : d_optionsAllocated(NULL), d_options(&options), d_statisticsRegistry(new StatisticsRegistry()), d_attrManager(ctxt), + d_exprManager(exprManager), d_nodeUnderDeletion(NULL), d_inReclaimZombies(false) { init(); @@ -444,6 +448,15 @@ TypeNode NodeManager::computeType(TNode n, bool check) TypeNode NodeManager::getType(TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { + // Many theories' type checkers call Node::getType() directly. + // This is incorrect, since "this" might not be the caller's + // curent node manager. Rather than force the individual typecheckers + // not to do this (by policy, which would be imperfect and lead + // to hard-to-find bugs, which it has in the past), we just + // set this node manager to be current for the duration of this + // check. + NodeManagerScope nms(this); + TypeNode typeNode; bool hasType = getAttribute(n, TypeAttr(), typeNode); bool needsCheck = check && !getAttribute(n, TypeCheckedAttr()); diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 36720bbb3..1760f48c7 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -25,6 +25,7 @@ #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 @@ -86,6 +87,9 @@ 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" @@ -250,8 +254,8 @@ class NodeManager { public: - explicit NodeManager(context::Context* ctxt); - explicit NodeManager(context::Context* ctxt, const Options& options); + explicit NodeManager(context::Context* ctxt, ExprManager* exprManager); + explicit NodeManager(context::Context* ctxt, ExprManager* exprManager, const Options& options); ~NodeManager(); /** The node manager in the current public-facing CVC4 library context */ @@ -578,7 +582,39 @@ public: */ TypeNode getType(TNode n, bool check = false) throw (TypeCheckingExceptionPrivate, AssertionException); -}; + + /** + * 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(TypeNode tn); + + /** + * Convert a type to a type node. + */ + static inline TypeNode fromType(Type t); + +};/* class NodeManager */ /** * This class changes the "current" thread-global @@ -782,6 +818,30 @@ 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(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 diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 46a456d50..78554f61f 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -117,6 +117,10 @@ Type Type::substitute(const std::vector& types, replacementsNodes.end())); } +ExprManager* Type::getExprManager() const { + return d_nodeManager->toExprManager(); +} + void Type::toStream(std::ostream& out) const { NodeManagerScope nms(d_nodeManager); out << *d_typeNode; diff --git a/src/expr/type.h b/src/expr/type.h index cc1248510..130aa3122 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -72,6 +72,7 @@ class CVC4_PUBLIC Type { friend class SmtEngine; friend class ExprManager; + friend class NodeManager; friend class TypeNode; friend struct TypeHashStrategy; friend std::ostream& operator<<(std::ostream& out, const Type& t); @@ -140,6 +141,11 @@ public: Type substitute(const std::vector& types, const std::vector& replacements) const; + /** + * Get this type's ExprManager. + */ + ExprManager* getExprManager() const; + /** * Assignment operator. * @param t the type to assign to this type -- 2.30.2