Delete Expr layer. (#6117)

1 files changed, 4 insertions, 78 deletions

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index d113c1458..348200b6e 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -22,8 +22,6 @@
 //#include "expr/attribute.h"
 #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
@@ -90,9 +88,6 @@ class NodeManager
   friend class api::Solver;
   friend class expr::NodeValue;
   friend class expr::TypeChecker;
-  // friends so they can access mkVar() here, which is private
-  friend Expr ExprManager::mkVar(const std::string&, Type);
-  friend Expr ExprManager::mkVar(Type);
 
   template <unsigned nchild_thresh>
   friend class NodeBuilder;
@@ -134,9 +129,6 @@ 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"
@@ -292,14 +284,10 @@ class NodeManager
     // `d_zombies` uses the node id to hash and compare nodes. If `d_zombies`
     // already contains a node value with the same id as `nv`, but the pointers
     // are different, then the wrong `NodeManager` was in scope for one of the
-    // two nodes when it reached refcount zero. This can happen for example if
-    // you create a node with a `NodeManager` n1 and then call `Node::toExpr()`
-    // on that node while a different `NodeManager` n2 is in scope. When that
-    // `Expr` is deleted and the node reaches refcount zero in the `Expr`'s
-    // destructor, then `markForDeletion()` will be called on n2.
+    // two nodes when it reached refcount zero.
     Assert(d_zombies.find(nv) == d_zombies.end() || *d_zombies.find(nv) == nv);
 
-    d_zombies.insert(nv);  // FIXME multithreading
+    d_zombies.insert(nv);
 
     if(safeToReclaimZombies()) {
       if(d_zombies.size() > 5000) {
@@ -392,8 +380,7 @@ class NodeManager
   Node* mkVarPtr(const TypeNode& type);
 
  public:
-
-  explicit NodeManager(ExprManager* exprManager);
+  explicit NodeManager();
   ~NodeManager();
 
   /** The node manager in the current public-facing CVC4 library context */
@@ -1103,37 +1090,6 @@ class NodeManager
    */
   TypeNode getType(TNode n, bool check = false);
 
-  /**
-   * 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(const TypeNode& tn);
-
-  /**
-   * Convert a type to a type node.
-   */
-  static inline TypeNode fromType(Type t);
-
   /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/
   void reclaimZombiesUntil(uint32_t k);
 
@@ -1165,8 +1121,7 @@ class NodeManager
  * public-interface calls into the CVC4 library, where CVC4's notion
  * of the "current" <code>NodeManager</code> should be set to match
  * the calling context.  See, for example, the implementations of
- * public calls in the <code>ExprManager</code> and
- * <code>SmtEngine</code> classes.
+ * public calls in the <code>SmtEngine</code> class.
  *
  * The client must be careful to create and destroy
  * <code>NodeManagerScope</code> objects in a well-nested manner (such
@@ -1183,10 +1138,6 @@ class NodeManagerScope {
 public:
  NodeManagerScope(NodeManager* nm) : d_oldNodeManager(NodeManager::s_current)
  {
-   // There are corner cases where nm can be NULL and it's ok.
-   // For example, if you write { Expr e; }, then when the null
-   // Expr is destructed, there's no active node manager.
-   // Assert(nm != NULL);
    NodeManager::s_current = nm;
    Debug("current") << "node manager scope: " << NodeManager::s_current << "\n";
   }
@@ -1274,31 +1225,6 @@ 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(const 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