From: Andres Noetzli Date: Wed, 19 May 2021 23:40:59 +0000 (-0700) Subject: Remove unused methods from `NodeManager` (#6578) X-Git-Tag: cvc5-1.0.0~1729 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=12770db5ef8a0a86dd264311955e105a78ae0b29;p=cvc5.git Remove unused methods from `NodeManager` (#6578) --- diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 780fda9ab..5d37a6db4 100644 --- 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::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::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 9952baf89..64db01300 100644 --- 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 Node mkNode(Kind kind, const std::vector >& children); - template - Node* mkNodePtr(Kind kind, const std::vector >& 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 Node mkNode(TNode opNode, const std::vector >& children); - template - Node* mkNodePtr(TNode opNode, const std::vector >& 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 inline Node NodeManager::mkNode(Kind kind, @@ -1297,15 +1241,6 @@ Node NodeManager::mkOr(const std::vector >& children) return mkNode(kind::OR, children); } -template -inline Node* NodeManager::mkNodePtr(Kind kind, - const std::vector >& - 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 inline Node NodeManager::mkNode(TNode opNode, @@ -1432,19 +1311,6 @@ inline Node NodeManager::mkNode(TNode opNode, return nb.constructNode(); } -template -inline Node* NodeManager::mkNodePtr(TNode opNode, - const std::vector >& - 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(); }