Delete Expr layer. (#6117)

1 files changed, 1 insertions, 52 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index 7e6324822..bb8c5618c 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -23,6 +23,7 @@
 #define CVC4__NODE_H
 
 #include <iostream>
+#include <map>
 #include <string>
 #include <unordered_map>
 #include <unordered_set>
@@ -32,7 +33,6 @@
 #include "base/check.h"
 #include "base/exception.h"
 #include "base/output.h"
-#include "expr/expr.h"
 #include "expr/expr_iomanip.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
@@ -170,8 +170,6 @@ class NodeTemplate {
    */
   friend class expr::NodeValue;
 
-  friend class expr::ExportPrivate;
-
   /** A convenient null-valued encapsulated pointer */
   static NodeTemplate s_null;
 
@@ -269,14 +267,6 @@ public:
   NodeTemplate(const NodeTemplate& node);
 
   /**
-   * Allow Exprs to become Nodes.  This permits flexible translation of
-   * Exprs -> Nodes inside the CVC4 library without exposing a toNode()
-   * function in the public interface, or requiring lots of "friend"
-   * relationships.
-   */
-  NodeTemplate(const Expr& e);
-
-  /**
    * Assignment operator for nodes, copies the relevant information from node
    * to this node.
    * @param node the node to copy
@@ -415,23 +405,6 @@ 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() const;
-
-  /**
-   * 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
@@ -1104,18 +1077,6 @@ NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate& e) {
 }
 
 template <bool ref_count>
-NodeTemplate<ref_count>::NodeTemplate(const Expr& e) {
-  Assert(e.d_node != NULL) << "Expecting a non-NULL expression value!";
-  Assert(e.d_node->d_nv != NULL) << "Expecting a non-NULL expression value!";
-  d_nv = e.d_node->d_nv;
-  // shouldn't ever fail
-  Assert(d_nv->d_rc > 0) << "Node constructed from Expr with rc == 0";
-  if(ref_count) {
-    d_nv->inc();
-  }
-}
-
-template <bool ref_count>
 NodeTemplate<ref_count>::~NodeTemplate() {
   Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
   if(ref_count) {
@@ -1459,18 +1420,6 @@ NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
   }
 }
 
-template <bool ref_count>
-inline Expr NodeTemplate<ref_count>::toExpr() const {
-  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