diff options
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/bool_to_bv.cpp | 2 | ||||
-rw-r--r-- | src/preprocessing/passes/bv_gauss.cpp | 4 | ||||
-rw-r--r-- | src/preprocessing/passes/bv_to_bool.cpp | 4 | ||||
-rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 6 | ||||
-rw-r--r-- | src/preprocessing/passes/foreign_theory_rewrite.cpp | 2 | ||||
-rw-r--r-- | src/preprocessing/passes/int_to_bv.cpp | 4 | ||||
-rw-r--r-- | src/preprocessing/passes/miplib_trick.cpp | 4 | ||||
-rw-r--r-- | src/preprocessing/passes/static_learning.cpp | 2 | ||||
-rw-r--r-- | src/preprocessing/util/ite_utilities.cpp | 18 |
9 files changed, 23 insertions, 23 deletions
diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp index df8e93bc7..ac7707d16 100644 --- a/src/preprocessing/passes/bool_to_bv.cpp +++ b/src/preprocessing/passes/bool_to_bv.cpp @@ -356,7 +356,7 @@ void BoolToBV::rebuildNode(const TNode& n, Kind new_kind) { Kind k = n.getKind(); NodeManager* nm = NodeManager::currentNM(); - NodeBuilder<> builder(new_kind); + NodeBuilder builder(new_kind); Debug("bool-to-bv") << "BoolToBV::rebuildNode with " << n << " and new_kind = " << kindToString(new_kind) diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp index 7bd0e7715..6b8b7af2f 100644 --- a/src/preprocessing/passes/bv_gauss.cpp +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -500,8 +500,8 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem( /* Flatten mult expression. */ n = RewriteRule<FlattenAssocCommut>::run<true>(n); /* Split operands into consts and non-consts */ - NodeBuilder<> nb_consts(NodeManager::currentNM(), k); - NodeBuilder<> nb_nonconsts(NodeManager::currentNM(), k); + NodeBuilder nb_consts(NodeManager::currentNM(), k); + NodeBuilder nb_nonconsts(NodeManager::currentNM(), k); for (const Node& nn : n) { Node nnrw = Rewriter::rewrite(nn); diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp index 9f219e7a4..a8382974c 100644 --- a/src/preprocessing/passes/bv_to_bool.cpp +++ b/src/preprocessing/passes/bv_to_bool.cpp @@ -220,7 +220,7 @@ Node BVToBool::convertBvTerm(TNode node) default: Unhandled(); } - NodeBuilder<> builder(new_kind); + NodeBuilder builder(new_kind); for (unsigned i = 0; i < node.getNumChildren(); ++i) { builder << convertBvTerm(node[i]); @@ -254,7 +254,7 @@ Node BVToBool::liftNode(TNode current) } else { - NodeBuilder<> builder(current.getKind()); + NodeBuilder builder(current.getKind()); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << current.getOperator(); diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 510d35419..c5f24c15c 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -116,7 +116,7 @@ Node BVToInt::makeBinary(Node n) else if (numChildren > 0) { // current has children, but we do not binarize it - NodeBuilder<> builder(k); + NodeBuilder builder(k); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << current.getOperator(); @@ -220,7 +220,7 @@ Node BVToInt::eliminationPass(Node n) { // The main operator is replaced, and the children // are replaced with their eliminated counterparts. - NodeBuilder<> builder(current.getKind()); + NodeBuilder builder(current.getKind()); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << current.getOperator(); @@ -886,7 +886,7 @@ Node BVToInt::reconstructNode(Node originalNode, // first, we adjust the children of the node as needed. // re-construct the term with the adjusted children. kind::Kind_t oldKind = originalNode.getKind(); - NodeBuilder<> builder(oldKind); + NodeBuilder builder(oldKind); if (originalNode.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << originalNode.getOperator(); diff --git a/src/preprocessing/passes/foreign_theory_rewrite.cpp b/src/preprocessing/passes/foreign_theory_rewrite.cpp index 307be46bf..60345992f 100644 --- a/src/preprocessing/passes/foreign_theory_rewrite.cpp +++ b/src/preprocessing/passes/foreign_theory_rewrite.cpp @@ -121,7 +121,7 @@ Node ForeignTheoryRewrite::reconstructNode(Node originalNode, } // re-build the node with the same kind and new children kind::Kind_t k = originalNode.getKind(); - NodeBuilder<> builder(k); + NodeBuilder builder(k); // special case for parameterized nodes if (originalNode.getMetaKind() == kind::metakind::PARAMETERIZED) { diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index b1f8ad771..ef9b261b0 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -79,7 +79,7 @@ Node intToBVMakeBinary(TNode n, NodeMap& cache) } else { - NodeBuilder<> builder(current.getKind()); + NodeBuilder builder(current.getKind()); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << current.getOperator(); } @@ -186,7 +186,7 @@ Node intToBV(TNode n, NodeMap& cache) } } } - NodeBuilder<> builder(newKind); + NodeBuilder builder(newKind); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << current.getOperator(); } diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 7c246c3e1..f3c4d2e12 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -57,7 +57,7 @@ size_t removeFromConjunction(Node& n, || (sub.getKind() == kind::AND && (subremovals = removeFromConjunction(sub, toRemove)) > 0)) { - NodeBuilder<> b(kind::AND); + NodeBuilder b(kind::AND); b.append(n.begin(), j); if (subremovals > 0) { @@ -559,7 +559,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( Node sum; if (pos.getKind() == kind::AND) { - NodeBuilder<> sumb(kind::PLUS); + NodeBuilder sumb(kind::PLUS); for (size_t jj = 0; jj < pos.getNumChildren(); ++jj) { sumb << nm->mkNode( diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp index 028322c1e..5e572d1d8 100644 --- a/src/preprocessing/passes/static_learning.cpp +++ b/src/preprocessing/passes/static_learning.cpp @@ -37,7 +37,7 @@ PreprocessingPassResult StaticLearning::applyInternal( for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { - NodeBuilder<> learned(kind::AND); + NodeBuilder learned(kind::AND); learned << (*assertionsToPreprocess)[i]; d_preprocContext->getTheoryEngine()->ppStaticLearn( (*assertionsToPreprocess)[i], learned); diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp index a3ad701a8..7826c207b 100644 --- a/src/preprocessing/util/ite_utilities.cpp +++ b/src/preprocessing/util/ite_utilities.cpp @@ -401,7 +401,7 @@ Node ITECompressor::compressBooleanITEs(Node toCompress) } } - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); Node curr = toCompress; while (curr.getKind() == kind::ITE && (curr[1] == d_false || curr[2] == d_false) @@ -465,7 +465,7 @@ Node ITECompressor::compressTerm(Node toCompress) } } - NodeBuilder<> nb(toCompress.getKind()); + NodeBuilder nb(toCompress.getKind()); if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) { @@ -504,7 +504,7 @@ Node ITECompressor::compressBoolean(Node toCompress) else { bool ta = ite::isTheoryAtom(toCompress); - NodeBuilder<> nb(toCompress.getKind()); + NodeBuilder nb(toCompress.getKind()); if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) { nb << (toCompress.getOperator()); @@ -906,7 +906,7 @@ Node ITESimplifier::replaceOver(Node n, Node replaceWith, Node simpVar) return d_replaceOverCache[p]; } - NodeBuilder<> builder(n.getKind()); + NodeBuilder builder(n.getKind()); if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << n.getOperator(); @@ -1207,7 +1207,7 @@ Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite) } else { - NodeBuilder<> nb(kind::OR); + NodeBuilder nb(kind::OR); NodeVec::const_iterator it = intersection.begin(), end = intersection.end(); for (; it != end; ++it) { @@ -1332,7 +1332,7 @@ Node ITESimplifier::simpConstants(TNode simpContext, if (iteNode.getKind() == kind::ITE) { - NodeBuilder<> builder(kind::ITE); + NodeBuilder builder(kind::ITE); builder << iteNode[0]; unsigned i = 1; for (; i < iteNode.getNumChildren(); ++i) @@ -1428,7 +1428,7 @@ Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar) return simpVar; } - NodeBuilder<> builder(c.getKind()); + NodeBuilder builder(c.getKind()); if (c.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << c.getOperator(); @@ -1584,7 +1584,7 @@ Node ITESimplifier::simpITE(TNode assertion) if (stackHead.d_children_added) { // Children have been processed, so substitute - NodeBuilder<> builder(current.getKind()); + NodeBuilder builder(current.getKind()); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << current.getOperator(); @@ -1731,7 +1731,7 @@ Node ITECareSimplifier::substitute(TNode e, return e; } - NodeBuilder<> builder(e.getKind()); + NodeBuilder builder(e.getKind()); if (e.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << e.getOperator(); |