summaryrefslogtreecommitdiff
path: root/src/preprocessing
diff options
context:
space:
mode:
Diffstat (limited to 'src/preprocessing')
-rw-r--r--src/preprocessing/passes/bool_to_bv.cpp2
-rw-r--r--src/preprocessing/passes/bv_gauss.cpp4
-rw-r--r--src/preprocessing/passes/bv_to_bool.cpp4
-rw-r--r--src/preprocessing/passes/bv_to_int.cpp6
-rw-r--r--src/preprocessing/passes/foreign_theory_rewrite.cpp2
-rw-r--r--src/preprocessing/passes/int_to_bv.cpp4
-rw-r--r--src/preprocessing/passes/miplib_trick.cpp4
-rw-r--r--src/preprocessing/passes/static_learning.cpp2
-rw-r--r--src/preprocessing/util/ite_utilities.cpp18
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();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback