diff options
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 62 |
1 files changed, 31 insertions, 31 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 857bcc25f..a72eada23 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -88,7 +88,6 @@ class NodeManager friend class expr::NodeValue; friend class expr::TypeChecker; - template <unsigned nchild_thresh> friend class NodeBuilder; friend class NodeManagerScope; @@ -1239,67 +1238,67 @@ inline Kind NodeManager::operatorToKind(TNode n) { } inline Node NodeManager::mkNode(Kind kind, TNode child1) { - NodeBuilder<1> nb(this, kind); + NodeBuilder nb(this, kind); nb << child1; return nb.constructNode(); } inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1) { - NodeBuilder<1> nb(this, kind); + NodeBuilder nb(this, kind); nb << child1; return nb.constructNodePtr(); } inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) { - NodeBuilder<2> nb(this, kind); + NodeBuilder nb(this, kind); nb << child1 << child2; return nb.constructNode(); } inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2) { - NodeBuilder<2> nb(this, kind); + NodeBuilder nb(this, kind); nb << child1 << child2; return nb.constructNodePtr(); } inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3) { - NodeBuilder<3> nb(this, kind); + NodeBuilder nb(this, kind); nb << child1 << child2 << child3; return nb.constructNode(); } inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3) { - NodeBuilder<3> nb(this, kind); + 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<4> nb(this, kind); + NodeBuilder nb(this, kind); nb << child1 << child2 << child3 << child4; return nb.constructNode(); } inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4) { - NodeBuilder<4> nb(this, kind); + 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<5> nb(this, kind); + NodeBuilder nb(this, kind); nb << child1 << child2 << child3 << child4 << child5; return nb.constructNode(); } inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5) { - NodeBuilder<5> nb(this, kind); + NodeBuilder nb(this, kind); nb << child1 << child2 << child3 << child4 << child5; return nb.constructNodePtr(); } @@ -1309,7 +1308,7 @@ template <bool ref_count> inline Node NodeManager::mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& children) { - NodeBuilder<> nb(this, kind); + NodeBuilder nb(this, kind); nb.append(children); return nb.constructNode(); } @@ -1346,14 +1345,14 @@ template <bool ref_count> inline Node* NodeManager::mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children) { - NodeBuilder<> nb(this, kind); + NodeBuilder nb(this, kind); nb.append(children); return nb.constructNodePtr(); } // for operators inline Node NodeManager::mkNode(TNode opNode) { - NodeBuilder<1> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1361,7 +1360,7 @@ inline Node NodeManager::mkNode(TNode opNode) { } inline Node* NodeManager::mkNodePtr(TNode opNode) { - NodeBuilder<1> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1369,7 +1368,7 @@ inline Node* NodeManager::mkNodePtr(TNode opNode) { } inline Node NodeManager::mkNode(TNode opNode, TNode child1) { - NodeBuilder<2> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1378,7 +1377,7 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1) { } inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) { - NodeBuilder<2> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1387,7 +1386,7 @@ inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) { } inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) { - NodeBuilder<3> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1396,7 +1395,7 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) { } inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) { - NodeBuilder<3> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1406,7 +1405,7 @@ inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) { inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, TNode child3) { - NodeBuilder<4> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1416,7 +1415,7 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3) { - NodeBuilder<4> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1426,7 +1425,7 @@ inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2, inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, TNode child3, TNode child4) { - NodeBuilder<5> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1436,7 +1435,7 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3, TNode child4) { - NodeBuilder<5> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1446,7 +1445,7 @@ inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2, inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5) { - NodeBuilder<6> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1456,7 +1455,7 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5) { - NodeBuilder<6> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1469,7 +1468,7 @@ template <bool ref_count> inline Node NodeManager::mkNode(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children) { - NodeBuilder<> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1481,7 +1480,7 @@ template <bool ref_count> inline Node* NodeManager::mkNodePtr(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children) { - NodeBuilder<> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1491,23 +1490,24 @@ inline Node* NodeManager::mkNodePtr(TNode opNode, inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1) { - return (NodeBuilder<1>(this, kind) << child1).constructTypeNode(); + return (NodeBuilder(this, kind) << child1).constructTypeNode(); } inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1, TypeNode child2) { - return (NodeBuilder<2>(this, kind) << child1 << child2).constructTypeNode(); + return (NodeBuilder(this, kind) << child1 << child2).constructTypeNode(); } inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1, TypeNode child2, TypeNode child3) { - return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode(); + return (NodeBuilder(this, kind) << child1 << child2 << child3) + .constructTypeNode(); } // N-ary version for types inline TypeNode NodeManager::mkTypeNode(Kind kind, const std::vector<TypeNode>& children) { - return NodeBuilder<>(this, kind).append(children).constructTypeNode(); + return NodeBuilder(this, kind).append(children).constructTypeNode(); } template <class T> |