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

1 files changed, 28 insertions, 0 deletions

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