partial merge from portfolio branch, adding conversions (library-internal-only of course) between Exprs and Nodes, Types and TypeNodes, ExprManagers and NodeManagers.

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 <bool ref_count> 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
@@ -372,6 +372,22 @@ public:
   // 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<ref_count>::substitute(Iterator1 nodesBegin,
   }
 }
 
+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
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<Type>& 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);
@@ -141,6 +142,11 @@ public:
                   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
    * @return this type after assignment.