diff options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/abstraction.cpp | 12 | ||||
-rw-r--r-- | src/theory/bv/bitblast/bitblaster.h | 2 | ||||
-rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_solver.h | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_solver_bitblast.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_solver_lazy.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_solver_lazy.h | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.cpp | 8 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_core.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 12 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 14 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.cpp | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 4 |
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; } |