Remove unused methods from `NodeManager` (#6578)

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 780fda9abd3eb4bfc0a99d412afed1e98f985138..5d37a6db4520bb02b2f447daec97408142c9e9b5 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -930,31 +930,12 @@ Node NodeManager::mkVar(const std::string& name, const TypeNode& type)
   return n;
 }
 
-Node* NodeManager::mkVarPtr(const std::string& name, const TypeNode& type)
-{
-  Node* n = NodeBuilder(this, kind::VARIABLE).constructNodePtr();
-  setAttribute(*n, TypeAttr(), type);
-  setAttribute(*n, TypeCheckedAttr(), true);
-  setAttribute(*n, expr::VarNameAttr(), name);
-  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(*n);
-  }
-  return n;
-}
-
 Node NodeManager::mkBoundVar(const std::string& name, const TypeNode& type) {
   Node n = mkBoundVar(type);
   setAttribute(n, expr::VarNameAttr(), name);
   return n;
 }
 
-Node* NodeManager::mkBoundVarPtr(const std::string& name,
-                                 const TypeNode& type) {
-  Node* n = mkBoundVarPtr(type);
-  setAttribute(*n, expr::VarNameAttr(), name);
-  return n;
-}
-
 Node NodeManager::getBoundVarListForFunctionType( TypeNode tn ) {
   Assert(tn.isFunction());
   Node bvl = tn.getAttribute(LambdaBoundVarListAttr());
@@ -1072,17 +1053,6 @@ Node NodeManager::mkVar(const TypeNode& type)
   return n;
 }
 
-Node* NodeManager::mkVarPtr(const TypeNode& type)
-{
-  Node* n = NodeBuilder(this, kind::VARIABLE).constructNodePtr();
-  setAttribute(*n, TypeAttr(), type);
-  setAttribute(*n, TypeCheckedAttr(), true);
-  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(*n);
-  }
-  return n;
-}
-
 Node NodeManager::mkBoundVar(const TypeNode& type) {
   Node n = NodeBuilder(this, kind::BOUND_VARIABLE);
   setAttribute(n, TypeAttr(), type);
@@ -1090,13 +1060,6 @@ Node NodeManager::mkBoundVar(const TypeNode& type) {
   return n;
 }
 
-Node* NodeManager::mkBoundVarPtr(const TypeNode& type) {
-  Node* n = NodeBuilder(this, kind::BOUND_VARIABLE).constructNodePtr();
-  setAttribute(*n, TypeAttr(), type);
-  setAttribute(*n, TypeCheckedAttr(), true);
-  return n;
-}
-
 Node NodeManager::mkInstConstant(const TypeNode& type) {
   Node n = NodeBuilder(this, kind::INST_CONSTANT);
   n.setAttribute(TypeAttr(), type);

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 9952baf898dd049c29d8402c7bcaa1197356087a..64db0130093833115156a2501cbeddf56b75b79f 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -355,11 +355,9 @@ class NodeManager
    * within cvc5.  Such uses should employ SkolemManager::mkSkolem() instead.
    */
   Node mkVar(const std::string& name, const TypeNode& type);
-  Node* mkVarPtr(const std::string& name, const TypeNode& type);
 
   /** Create a variable with the given type. */
   Node mkVar(const TypeNode& type);
-  Node* mkVarPtr(const TypeNode& type);
 
   /**
    * Create a skolem constant with the given name, type, and comment. For
@@ -433,33 +431,24 @@ class NodeManager
 
   /** Create a node with one child. */
   Node mkNode(Kind kind, TNode child1);
-  Node* mkNodePtr(Kind kind, TNode child1);
 
   /** Create a node with two children. */
   Node mkNode(Kind kind, TNode child1, TNode child2);
-  Node* mkNodePtr(Kind kind, TNode child1, TNode child2);
 
   /** Create a node with three children. */
   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3);
-  Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3);
 
   /** Create a node with four children. */
   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
               TNode child4);
-  Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
-              TNode child4);
 
   /** Create a node with five children. */
   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
               TNode child4, TNode child5);
-  Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
-              TNode child4, TNode child5);
 
   /** Create a node with an arbitrary number of children. */
   template <bool ref_count>
   Node mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
-  template <bool ref_count>
-  Node* mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
 
   /**
    * Create an AND node with arbitrary number of children. This returns the
@@ -485,43 +474,31 @@ class NodeManager
 
   /** Create a node (with no children) by operator. */
   Node mkNode(TNode opNode);
-  Node* mkNodePtr(TNode opNode);
 
   /** Create a node with one child by operator. */
   Node mkNode(TNode opNode, TNode child1);
-  Node* mkNodePtr(TNode opNode, TNode child1);
 
   /** Create a node with two children by operator. */
   Node mkNode(TNode opNode, TNode child1, TNode child2);
-  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2);
 
   /** Create a node with three children by operator. */
   Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3);
-  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3);
 
   /** Create a node with four children by operator. */
   Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
               TNode child4);
-  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
-              TNode child4);
 
   /** Create a node with five children by operator. */
   Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
               TNode child4, TNode child5);
-  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
-              TNode child4, TNode child5);
 
   /** Create a node by applying an operator to the children. */
   template <bool ref_count>
   Node mkNode(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
-  template <bool ref_count>
-  Node* mkNodePtr(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
 
   Node mkBoundVar(const std::string& name, const TypeNode& type);
-  Node* mkBoundVarPtr(const std::string& name, const TypeNode& type);
 
   Node mkBoundVar(const TypeNode& type);
-  Node* mkBoundVarPtr(const TypeNode& type);
 
   /** get the canonical bound variable list for function type tn */
   Node getBoundVarListForFunctionType( TypeNode tn );
@@ -1199,24 +1176,12 @@ inline Node NodeManager::mkNode(Kind kind, TNode child1) {
   return nb.constructNode();
 }
 
-inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1) {
-  NodeBuilder nb(this, kind);
-  nb << child1;
-  return nb.constructNodePtr();
-}
-
 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) {
   NodeBuilder nb(this, kind);
   nb << child1 << child2;
   return nb.constructNode();
 }
 
-inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2) {
-  NodeBuilder nb(this, kind);
-  nb << child1 << child2;
-  return nb.constructNodePtr();
-}
-
 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
                                 TNode child3) {
   NodeBuilder nb(this, kind);
@@ -1224,13 +1189,6 @@ inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
   return nb.constructNode();
 }
 
-inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
-                                TNode child3) {
-  NodeBuilder nb(this, kind);
-  nb << child1 << child2 << child3;
-  return nb.constructNodePtr();
-}
-
 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
                                 TNode child3, TNode child4) {
   NodeBuilder nb(this, kind);
@@ -1238,13 +1196,6 @@ inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
   return nb.constructNode();
 }
 
-inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
-                                TNode child3, TNode child4) {
-  NodeBuilder nb(this, kind);
-  nb << child1 << child2 << child3 << child4;
-  return nb.constructNodePtr();
-}
-
 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
                                 TNode child3, TNode child4, TNode child5) {
   NodeBuilder nb(this, kind);
@@ -1252,13 +1203,6 @@ inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
   return nb.constructNode();
 }
 
-inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
-                                    TNode child3, TNode child4, TNode child5) {
-  NodeBuilder nb(this, kind);
-  nb << child1 << child2 << child3 << child4 << child5;
-  return nb.constructNodePtr();
-}
-
 // N-ary version
 template <bool ref_count>
 inline Node NodeManager::mkNode(Kind kind,
@@ -1297,15 +1241,6 @@ Node NodeManager::mkOr(const std::vector<NodeTemplate<ref_count> >& children)
   return mkNode(kind::OR, children);
 }
 
-template <bool ref_count>
-inline Node* NodeManager::mkNodePtr(Kind kind,
-                                const std::vector<NodeTemplate<ref_count> >&
-                                children) {
-  NodeBuilder nb(this, kind);
-  nb.append(children);
-  return nb.constructNodePtr();
-}
-
 // for operators
 inline Node NodeManager::mkNode(TNode opNode) {
   NodeBuilder nb(this, operatorToKind(opNode));
@@ -1315,14 +1250,6 @@ inline Node NodeManager::mkNode(TNode opNode) {
   return nb.constructNode();
 }
 
-inline Node* NodeManager::mkNodePtr(TNode opNode) {
-  NodeBuilder nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  return nb.constructNodePtr();
-}
-
 inline Node NodeManager::mkNode(TNode opNode, TNode child1) {
   NodeBuilder nb(this, operatorToKind(opNode));
   if(opNode.getKind() != kind::BUILTIN) {
@@ -1332,15 +1259,6 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1) {
   return nb.constructNode();
 }
 
-inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) {
-  NodeBuilder nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb << child1;
-  return nb.constructNodePtr();
-}
-
 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) {
   NodeBuilder nb(this, operatorToKind(opNode));
   if(opNode.getKind() != kind::BUILTIN) {
@@ -1350,15 +1268,6 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) {
   return nb.constructNode();
 }
 
-inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) {
-  NodeBuilder nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb << child1 << child2;
-  return nb.constructNodePtr();
-}
-
 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
                                 TNode child3) {
   NodeBuilder nb(this, operatorToKind(opNode));
@@ -1369,16 +1278,6 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
   return nb.constructNode();
 }
 
-inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
-                                TNode child3) {
-  NodeBuilder nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb << child1 << child2 << child3;
-  return nb.constructNodePtr();
-}
-
 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
                                 TNode child3, TNode child4) {
   NodeBuilder nb(this, operatorToKind(opNode));
@@ -1389,16 +1288,6 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
   return nb.constructNode();
 }
 
-inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
-                                TNode child3, TNode child4) {
-  NodeBuilder nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb << child1 << child2 << child3 << child4;
-  return nb.constructNodePtr();
-}
-
 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
                                 TNode child3, TNode child4, TNode child5) {
   NodeBuilder nb(this, operatorToKind(opNode));
@@ -1409,16 +1298,6 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
   return nb.constructNode();
 }
 
-inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
-                                    TNode child3, TNode child4, TNode child5) {
-  NodeBuilder nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb << child1 << child2 << child3 << child4 << child5;
-  return nb.constructNodePtr();
-}
-
 // N-ary version for operators
 template <bool ref_count>
 inline Node NodeManager::mkNode(TNode opNode,
@@ -1432,19 +1311,6 @@ inline Node NodeManager::mkNode(TNode opNode,
   return nb.constructNode();
 }
 
-template <bool ref_count>
-inline Node* NodeManager::mkNodePtr(TNode opNode,
-                                    const std::vector<NodeTemplate<ref_count> >&
-                                    children) {
-  NodeBuilder nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb.append(children);
-  return nb.constructNodePtr();
-}
-
-
 inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1) {
   return (NodeBuilder(this, kind) << child1).constructTypeNode();
 }