} \
++ *(d_exprStatisticsVars[type]); \
}
-#else
+#else
#define INC_STAT(kind)
#define INC_STAT_VAR(type)
#endif
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;
}
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;
}
}
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) {
}
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)",
/** 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:
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 <bool ref_count> friend class NodeTemplate;
// 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
}
}
+template <bool ref_count>
+inline Expr NodeTemplate<ref_count>::toExpr() {
+ assertTNodeNotExpired();
+ return NodeManager::currentNM()->toExpr(*this);
+}
+
+// intentionally not defined for TNode
+template <>
+inline Node NodeTemplate<true>::fromExpr(const Expr& e) {
+ return NodeManager::fromExpr(e);
+}
+
#ifdef CVC4_DEBUG
/**
* Pretty printer for use within gdb. This is not intended to be used
}
};
-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();
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());
#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
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"
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 */
*/
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
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
replacementsNodes.end()));
}
+ExprManager* Type::getExprManager() const {
+ return d_nodeManager->toExprManager();
+}
+
void Type::toStream(std::ostream& out) const {
NodeManagerScope nms(d_nodeManager);
out << *d_typeNode;
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);
Type substitute(const std::vector<Type>& types,
const std::vector<Type>& replacements) const;
+ /**
+ * Get this type's ExprManager.
+ */
+ ExprManager* getExprManager() const;
+
/**
* Assignment operator.
* @param t the type to assign to this type
projects / cvc5.git / commitdiff