summaryrefslogtreecommitdiff
path: root/src/theory/bv
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv')
-rw-r--r--src/theory/bv/abstraction.cpp12
-rw-r--r--src/theory/bv/bitblast/bitblaster.h2
-rw-r--r--src/theory/bv/bitblast/lazy_bitblaster.cpp2
-rw-r--r--src/theory/bv/bv_solver.h2
-rw-r--r--src/theory/bv/bv_solver_bitblast.cpp2
-rw-r--r--src/theory/bv/bv_solver_lazy.cpp2
-rw-r--r--src/theory/bv/bv_solver_lazy.h2
-rw-r--r--src/theory/bv/bv_subtheory_algebraic.cpp8
-rw-r--r--src/theory/bv/theory_bv.cpp2
-rw-r--r--src/theory/bv/theory_bv.h2
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules.h2
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_core.h2
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_normalization.h12
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h2
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_simplification.h14
-rw-r--r--src/theory/bv/theory_bv_utils.cpp4
-rw-r--r--src/theory/bv/theory_bv_utils.h4
17 files changed, 38 insertions, 38 deletions
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index 62c458723..acb67a373 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -151,7 +151,7 @@ Node AbstractionModule::reverseAbstraction(Node assertion, NodeNodeMap& seen) {
return assertion;
}
- NodeBuilder<> result(assertion.getKind());
+ NodeBuilder result(assertion.getKind());
if (assertion.getMetaKind() == kind::metakind::PARAMETERIZED) {
result << assertion.getOperator();
}
@@ -204,7 +204,7 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions)
assertion_table.addEntry(func.getOperator(), args);
}
- NodeBuilder<> assertion_builder(kind::OR);
+ NodeBuilder assertion_builder(kind::OR);
// construct skolemized assertion
for (ArgsTable::iterator it = assertion_table.begin();
it != assertion_table.end();
@@ -214,7 +214,7 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions)
++(d_statistics.d_numArgsSkolemized);
TNode func = it->first;
ArgsTableEntry& args = it->second;
- NodeBuilder<> skolem_func(kind::APPLY_UF);
+ NodeBuilder skolem_func(kind::APPLY_UF);
skolem_func << func;
std::vector<Node> skolem_args;
@@ -241,7 +241,7 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions)
// for (ArgsTableEntry::iterator it = args.begin(); it != args.end();
// ++it)
{
- NodeBuilder<> arg_assignment(kind::AND);
+ NodeBuilder arg_assignment(kind::AND);
// ArgsVec& args = *it;
for (unsigned k = 0; k < av.size(); ++k)
{
@@ -342,7 +342,7 @@ Node AbstractionModule::computeSignatureRec(TNode node, NodeNodeMap& cache) {
return sig;
}
- NodeBuilder<> builder(node.getKind());
+ NodeBuilder builder(node.getKind());
if (node.getMetaKind() == kind::metakind::PARAMETERIZED) {
builder << node.getOperator();
}
@@ -676,7 +676,7 @@ Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsign
return signature;
}
- NodeBuilder<> builder(signature.getKind());
+ NodeBuilder builder(signature.getKind());
if (signature.getMetaKind() == kind::metakind::PARAMETERIZED) {
builder << signature.getOperator();
}
diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index 311d44c94..dd0be5cc0 100644
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -247,7 +247,7 @@ Node TBitblaster<T>::getTermModel(TNode node, bool fullModel)
}
Assert(node.getType().isBitVector());
- NodeBuilder<> nb(node.getKind());
+ NodeBuilder nb(node.getKind());
if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
{
nb << node.getOperator();
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index a5d3e9bb6..568ef2ebf 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -411,7 +411,7 @@ bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) {
void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
if (clause.size() > 1) {
- NodeBuilder<> lemmab(kind::OR);
+ NodeBuilder lemmab(kind::OR);
for (unsigned i = 0; i < clause.size(); ++ i) {
lemmab << d_cnf->getNode(clause[i]);
}
diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h
index faa285b97..8fa8fd850 100644
--- a/src/theory/bv/bv_solver.h
+++ b/src/theory/bv/bv_solver.h
@@ -90,7 +90,7 @@ class BVSolver
virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); };
- virtual void ppStaticLearn(TNode in, NodeBuilder<>& learned){};
+ virtual void ppStaticLearn(TNode in, NodeBuilder& learned){};
virtual void presolve(){};
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index 125cb243f..0aa99a889 100644
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -256,7 +256,7 @@ Node BVSolverBitblast::getValue(TNode node)
}
else if (it->second.isNull())
{
- NodeBuilder<> nb(cur.getKind());
+ NodeBuilder nb(cur.getKind());
if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
{
nb << cur.getOperator();
diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index 00190233c..c12121bf8 100644
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -741,7 +741,7 @@ EqualityStatus BVSolverLazy::getEqualityStatus(TNode a, TNode b)
;
}
-void BVSolverLazy::ppStaticLearn(TNode in, NodeBuilder<>& learned)
+void BVSolverLazy::ppStaticLearn(TNode in, NodeBuilder& learned)
{
if (d_staticLearnCache.find(in) != d_staticLearnCache.end())
{
diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h
index ea647346e..35b9964e0 100644
--- a/src/theory/bv/bv_solver_lazy.h
+++ b/src/theory/bv/bv_solver_lazy.h
@@ -97,7 +97,7 @@ class BVSolverLazy : public BVSolver
TrustNode ppRewrite(TNode t) override;
- void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
+ void ppStaticLearn(TNode in, NodeBuilder& learned) override;
void presolve() override;
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index c025dab5d..221ad3cbd 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -160,7 +160,7 @@ Node SubstitutionEx::internalApply(TNode node) {
// children already processed
if (head.childrenAdded) {
- NodeBuilder<> nb(current.getKind());
+ NodeBuilder nb(current.getKind());
std::vector<Node> reasons;
if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
@@ -512,7 +512,7 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) {
return changed;
}
- NodeBuilder<> nb(kind::BITVECTOR_XOR);
+ NodeBuilder nb(kind::BITVECTOR_XOR);
for (unsigned i = 1; i < left.getNumChildren(); ++i) {
nb << left[i];
}
@@ -848,7 +848,7 @@ void ExtractSkolemizer::skolemize(std::vector<WorklistElement>& facts) {
Node sk = utils::mkVar(size);
skolems.push_back(sk);
}
- NodeBuilder<> skolem_nb(kind::BITVECTOR_CONCAT);
+ NodeBuilder skolem_nb(kind::BITVECTOR_CONCAT);
for (int i = skolems.size() - 1; i >= 0; --i) {
skolem_nb << skolems[i];
@@ -975,7 +975,7 @@ Node mergeExplanations(const std::vector<Node>& expls) {
return *literals.begin();
}
- NodeBuilder<> nb(kind::AND);
+ NodeBuilder nb(kind::AND);
for (TNodeSet::const_iterator it = literals.begin(); it!= literals.end(); ++it) {
nb << *it;
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 8f9f88ea2..2c6d52b15 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -223,7 +223,7 @@ void TheoryBV::notifySharedTerm(TNode t)
d_internal->notifySharedTerm(t);
}
-void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned)
+void TheoryBV::ppStaticLearn(TNode in, NodeBuilder& learned)
{
d_internal->ppStaticLearn(in, learned);
}
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index c9ddaad11..c22f5c95a 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -92,7 +92,7 @@ class TheoryBV : public Theory
TrustNode ppRewrite(TNode t, std::vector<SkolemLemma>& lems) override;
- void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
+ void ppStaticLearn(TNode in, NodeBuilder& learned) override;
void presolve() override;
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index e92ed5543..6435e0e3c 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -642,7 +642,7 @@ struct ApplyRuleToChildren {
if (node.getKind() != kind) {
return RewriteRule<rule>::template run<true>(node);
}
- NodeBuilder<> result(kind);
+ NodeBuilder result(kind);
for (unsigned i = 0, end = node.getNumChildren(); i < end; ++ i) {
result << RewriteRule<rule>::template run<true>(node[i]);
}
diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index 7060b68a9..c463f0faf 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -36,7 +36,7 @@ bool RewriteRule<ConcatFlatten>::applies(TNode node) {
template<> inline
Node RewriteRule<ConcatFlatten>::apply(TNode node) {
Debug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << node << ")" << std::endl;
- NodeBuilder<> result(kind::BITVECTOR_CONCAT);
+ NodeBuilder result(kind::BITVECTOR_CONCAT);
std::vector<Node> processing_stack;
processing_stack.push_back(node);
while (!processing_stack.empty()) {
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 4872f8070..39425b41e 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -284,7 +284,7 @@ static inline void updateCoefMap(TNode current, unsigned size,
}
}
else if (current[current.getNumChildren()-1].isConst()) {
- NodeBuilder<> nb(kind::BITVECTOR_MULT);
+ NodeBuilder nb(kind::BITVECTOR_MULT);
TNode::iterator child_it = current.begin();
for(; (child_it+1) != current.end(); ++child_it) {
Assert(!(*child_it).isConst());
@@ -353,7 +353,7 @@ static inline void addToChildren(TNode term,
}
else if (term.getKind() == kind::BITVECTOR_MULT)
{
- NodeBuilder<> nb(kind::BITVECTOR_MULT);
+ NodeBuilder nb(kind::BITVECTOR_MULT);
TNode::iterator child_it = term.begin();
for (; child_it != term.end(); ++child_it)
{
@@ -896,7 +896,7 @@ bool RewriteRule<BitwiseEq>::applies(TNode node) {
static inline Node mkNodeKind(Kind k, TNode node, TNode c) {
unsigned i = 0;
unsigned nc = node.getNumChildren();
- NodeBuilder<> nb(k);
+ NodeBuilder nb(k);
for(; i < nc; ++i) {
nb << node[i].eqNode(c);
}
@@ -991,7 +991,7 @@ template<> inline
Node RewriteRule<NegMult>::apply(TNode node) {
Debug("bv-rewrite") << "RewriteRule<NegMult>(" << node << ")" << std::endl;
TNode mult = node[0];
- NodeBuilder<> nb(kind::BITVECTOR_MULT);
+ NodeBuilder nb(kind::BITVECTOR_MULT);
BitVector bv(utils::getSize(node), (unsigned)1);
TNode::iterator child_it = mult.begin();
for(; (child_it+1) != mult.end(); ++child_it) {
@@ -1492,8 +1492,8 @@ inline Node RewriteRule<NormalizeEqPlusNeg>::apply(TNode node)
Debug("bv-rewrite") << "RewriteRule<NormalizeEqPlusNeg>(" << node << ")"
<< std::endl;
- NodeBuilder<> nb_lhs(kind::BITVECTOR_PLUS);
- NodeBuilder<> nb_rhs(kind::BITVECTOR_PLUS);
+ NodeBuilder nb_lhs(kind::BITVECTOR_PLUS);
+ NodeBuilder nb_rhs(kind::BITVECTOR_PLUS);
NodeManager *nm = NodeManager::currentNM();
if (node[0].getKind() == kind::BITVECTOR_PLUS)
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 3244ebb6e..3dd0da3bd 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -286,7 +286,7 @@ inline Node RewriteRule<RepeatEliminate>::apply(TNode node)
if(amount == 1) {
return a;
}
- NodeBuilder<> result(kind::BITVECTOR_CONCAT);
+ NodeBuilder result(kind::BITVECTOR_CONCAT);
for(unsigned i = 0; i < amount; ++i) {
result << node[0];
}
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 2e99cc467..c0bce9097 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -558,10 +558,10 @@ inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node)
Kind kind = node.getKind();
TNode concat;
Node x, y, z, c;
- NodeBuilder<> xb(kind);
- NodeBuilder<> yb(kind::BITVECTOR_CONCAT);
- NodeBuilder<> zb(kind::BITVECTOR_CONCAT);
- NodeBuilder<> res(kind::BITVECTOR_CONCAT);
+ NodeBuilder xb(kind);
+ NodeBuilder yb(kind::BITVECTOR_CONCAT);
+ NodeBuilder zb(kind::BITVECTOR_CONCAT);
+ NodeBuilder res(kind::BITVECTOR_CONCAT);
NodeManager* nm = NodeManager::currentNM();
for (const TNode& child : node)
@@ -1680,13 +1680,13 @@ Node RewriteRule<MergeSignExtend>::apply(TNode node) {
.d_zeroExtendAmount;
if (amount2 == 0)
{
- NodeBuilder<> nb(kind::BITVECTOR_SIGN_EXTEND);
+ NodeBuilder nb(kind::BITVECTOR_SIGN_EXTEND);
Node op = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(amount1));
nb << op << node[0][0];
Node res = nb;
return res;
}
- NodeBuilder<> nb(kind::BITVECTOR_ZERO_EXTEND);
+ NodeBuilder nb(kind::BITVECTOR_ZERO_EXTEND);
Node op = nm->mkConst<BitVectorZeroExtend>(
BitVectorZeroExtend(amount1 + amount2));
nb << op << node[0][0];
@@ -2246,7 +2246,7 @@ Node RewriteRule<MultSltMult>::apply(TNode node)
Node zero_t = utils::mkZero(utils::getSize(t));
Node zero_a = utils::mkZero(utils::getSize(a));
- NodeBuilder<> nb(kind::AND);
+ NodeBuilder nb(kind::AND);
Kind k = is_sext ? kind::BITVECTOR_SLT : kind::BITVECTOR_ULT;
nb << t.eqNode(zero_t).notNode();
nb << a.eqNode(zero_a).notNode();
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index c2a7f05b6..96f91ea9f 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -384,7 +384,7 @@ Node mkConcat(TNode node, unsigned repeat)
{
return node;
}
- NodeBuilder<> result(kind::BITVECTOR_CONCAT);
+ NodeBuilder result(kind::BITVECTOR_CONCAT);
for (unsigned i = 0; i < repeat; ++i)
{
result << node;
@@ -503,7 +503,7 @@ Node eliminateInt2Bv(TNode node)
{
return v[0];
}
- NodeBuilder<> result(kind::BITVECTOR_CONCAT);
+ NodeBuilder result(kind::BITVECTOR_CONCAT);
result.append(v.rbegin(), v.rend());
return Node(result);
}
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 04258d441..38b6caf94 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -140,7 +140,7 @@ Node mkAnd(const std::vector<NodeTemplate<ref_count>>& conjunctions)
/* All the same, or just one */
if (all.size() == 1) { return conjunctions[0]; }
- NodeBuilder<> conjunction(kind::AND);
+ NodeBuilder conjunction(kind::AND);
for (TNode n : all) { conjunction << n; }
return conjunction;
}
@@ -159,7 +159,7 @@ Node mkOr(const std::vector<NodeTemplate<ref_count>>& nodes)
/* All the same, or just one */
if (all.size() == 1) { return nodes[0]; }
- NodeBuilder<> disjunction(kind::OR);
+ NodeBuilder disjunction(kind::OR);
for (TNode n : all) { disjunction << n; }
return disjunction;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback