diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-05-20 17:41:50 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-21 00:41:50 +0000 |
| commit | 9670dd43576cd21de82e22e76c57e783aa143d21 (patch) | |
| tree | 7a5157afa203bbe0a8755bdb0e178fb993d7e262 | |
| parent | 9e5f2385b73d55f675fa3996a2dd6df0e8d7652b (diff) | |
BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)
50 files changed, 380 insertions, 371 deletions
diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp index d59733d76..8768bd996 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/bitvectors.cpp @@ -96,7 +96,7 @@ int main() // Encoding code (2) // new_x_ = a + b - x - Term a_plus_b = slv.mkTerm(BITVECTOR_PLUS, a, b); + Term a_plus_b = slv.mkTerm(BITVECTOR_ADD, a, b); Term a_plus_b_minus_x = slv.mkTerm(BITVECTOR_SUB, a_plus_b, x); Term assignment2 = slv.mkTerm(EQUAL, new_x_, a_plus_b_minus_x); diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java index 1ef0ea23f..6d97b93fa 100644 --- a/examples/api/java/BitVectors.java +++ b/examples/api/java/BitVectors.java @@ -94,7 +94,7 @@ public class BitVectors { // Encoding code (2) // new_x_ = a + b - x - Expr a_plus_b = em.mkExpr(Kind.BITVECTOR_PLUS, a, b); + Expr a_plus_b = em.mkExpr(Kind.BITVECTOR_ADD, a, b); Expr a_plus_b_minus_x = em.mkExpr(Kind.BITVECTOR_SUB, a_plus_b, x); Expr assignment2 = em.mkExpr(Kind.EQUAL, new_x_, a_plus_b_minus_x); diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py index 1ddb02d8e..ff99bd785 100644 --- a/examples/api/python/bitvectors.py +++ b/examples/api/python/bitvectors.py @@ -92,7 +92,7 @@ if __name__ == "__main__": # Encoding code (2) # new_x_ = a + b - x - a_plus_b = slv.mkTerm(kinds.BVPlus, a, b) + a_plus_b = slv.mkTerm(kinds.BVAdd, a, b) a_plus_b_minus_x = slv.mkTerm(kinds.BVSub, a_plus_b, x) assignment2 = slv.mkTerm(kinds.Equal, new_x_, a_plus_b_minus_x) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index ed35659f0..b7923321c 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -163,7 +163,7 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{ {BITVECTOR_XNOR, cvc5::Kind::BITVECTOR_XNOR}, {BITVECTOR_COMP, cvc5::Kind::BITVECTOR_COMP}, {BITVECTOR_MULT, cvc5::Kind::BITVECTOR_MULT}, - {BITVECTOR_PLUS, cvc5::Kind::BITVECTOR_PLUS}, + {BITVECTOR_ADD, cvc5::Kind::BITVECTOR_ADD}, {BITVECTOR_SUB, cvc5::Kind::BITVECTOR_SUB}, {BITVECTOR_NEG, cvc5::Kind::BITVECTOR_NEG}, {BITVECTOR_UDIV, cvc5::Kind::BITVECTOR_UDIV}, @@ -442,7 +442,7 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction> {cvc5::Kind::BITVECTOR_XNOR, BITVECTOR_XNOR}, {cvc5::Kind::BITVECTOR_COMP, BITVECTOR_COMP}, {cvc5::Kind::BITVECTOR_MULT, BITVECTOR_MULT}, - {cvc5::Kind::BITVECTOR_PLUS, BITVECTOR_PLUS}, + {cvc5::Kind::BITVECTOR_ADD, BITVECTOR_ADD}, {cvc5::Kind::BITVECTOR_SUB, BITVECTOR_SUB}, {cvc5::Kind::BITVECTOR_NEG, BITVECTOR_NEG}, {cvc5::Kind::BITVECTOR_UDIV, BITVECTOR_UDIV}, diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index cad029b72..2805f6203 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -27,7 +27,9 @@ namespace api { /* Kind */ /* -------------------------------------------------------------------------- */ -// TODO(Gereon): Fix links that involve std::vector. See https://github.com/doxygen/doxygen/issues/8503 +// TODO(Gereon): Fix links that involve std::vector. See +// https://github.com/doxygen/doxygen/issues/8503 +// clang-format off /** * The kind of a cvc5 term. * @@ -888,7 +890,7 @@ enum CVC5_EXPORT Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ - BITVECTOR_PLUS, + BITVECTOR_ADD, /** * Subtraction of two bit-vectors. * @@ -3389,6 +3391,7 @@ enum CVC5_EXPORT Kind : int32_t /** Marks the upper-bound of this enumeration. */ LAST_KIND }; +// clang-format on /** * Get the string representation of a given kind. diff --git a/src/api/parsekinds.py b/src/api/parsekinds.py index f0ac415e1..0c39bca6f 100644 --- a/src/api/parsekinds.py +++ b/src/api/parsekinds.py @@ -102,7 +102,7 @@ class KindsParser: so that the word after "Is" is capitalized Examples: - BITVECTOR_PLUS --> BVPlus + BITVECTOR_ADD --> BVAdd APPLY_SELECTOR --> ApplySelector FLOATINGPOINT_ISNAN --> FPIsNan SETMINUS --> Setminus diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 02323b606..c2a6a30f6 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -140,7 +140,7 @@ const char* toString(PfRule id) case PfRule::BV_BITBLAST_NOR: return "BV_BITBLAST_NOR"; case PfRule::BV_BITBLAST_COMP: return "BV_BITBLAST_COMP"; case PfRule::BV_BITBLAST_MULT: return "BV_BITBLAST_MULT"; - case PfRule::BV_BITBLAST_PLUS: return "BV_BITBLAST_PLUS"; + case PfRule::BV_BITBLAST_ADD: return "BV_BITBLAST_ADD"; case PfRule::BV_BITBLAST_SUB: return "BV_BITBLAST_SUB"; case PfRule::BV_BITBLAST_NEG: return "BV_BITBLAST_NEG"; case PfRule::BV_BITBLAST_UDIV: return "BV_BITBLAST_UDIV"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index cfab15614..e4c33a840 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -757,7 +757,7 @@ enum class PfRule : uint32_t BV_BITBLAST_NOR, BV_BITBLAST_COMP, BV_BITBLAST_MULT, - BV_BITBLAST_PLUS, + BV_BITBLAST_ADD, BV_BITBLAST_SUB, BV_BITBLAST_NEG, BV_BITBLAST_UDIV, diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 6e3332651..c0a42ac26 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1904,7 +1904,7 @@ bvTerm[cvc5::api::Term& f] for (unsigned i = 0; i < args.size(); ++ i) { ENSURE_BV_SIZE(k, args[i]); } - f = MK_TERM(cvc5::api::BITVECTOR_PLUS, args); + f = MK_TERM(cvc5::api::BITVECTOR_ADD, args); } /* BV subtraction */ | BVSUB_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index c22b95af2..f3fd5697d 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -87,7 +87,7 @@ void Smt2::addBitvectorOperators() { addOperator(api::BITVECTOR_AND, "bvand"); addOperator(api::BITVECTOR_OR, "bvor"); addOperator(api::BITVECTOR_NEG, "bvneg"); - addOperator(api::BITVECTOR_PLUS, "bvadd"); + addOperator(api::BITVECTOR_ADD, "bvadd"); addOperator(api::BITVECTOR_MULT, "bvmul"); addOperator(api::BITVECTOR_UDIV, "bvudiv"); addOperator(api::BITVECTOR_UREM, "bvurem"); diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp index f34ebd02e..b3c34087d 100644 --- a/src/preprocessing/passes/bv_gauss.cpp +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -192,7 +192,7 @@ unsigned BVGauss::getMinBwExpr(Node expr) break; } - case kind::BITVECTOR_PLUS: + case kind::BITVECTOR_ADD: { Integer maxval = Integer(0); for (const Node& nn : n) @@ -490,7 +490,7 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem( /* Split into matrix columns */ Kind k = n.getKind(); - if (k == kind::BITVECTOR_PLUS) + if (k == kind::BITVECTOR_ADD) { for (const Node& nn : n) { stack.push_back(nn); } } @@ -668,16 +668,15 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem( } else { - Node tmp = stack.size() == 1 - ? stack[0] - : nm->mkNode(kind::BITVECTOR_PLUS, stack); + Node tmp = stack.size() == 1 ? stack[0] + : nm->mkNode(kind::BITVECTOR_ADD, stack); if (rhs[prow] != 0) { - tmp = nm->mkNode(kind::BITVECTOR_PLUS, - bv::utils::mkConst( - bv::utils::getSize(vvars[pcol]), rhs[prow]), - tmp); + tmp = nm->mkNode( + kind::BITVECTOR_ADD, + bv::utils::mkConst(bv::utils::getSize(vvars[pcol]), rhs[prow]), + tmp); } Assert(!is_bv_const(tmp)); res[vvars[pcol]] = nm->mkNode(kind::BITVECTOR_UREM, tmp, prime); @@ -730,7 +729,7 @@ PreprocessingPassResult BVGauss::applyInternal( continue; } - if (urem[0].getKind() == kind::BITVECTOR_PLUS && is_bv_const(urem[1])) + if (urem[0].getKind() == kind::BITVECTOR_ADD && is_bv_const(urem[1])) { equations[urem[1]].push_back(a); } diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index c725081c2..8b5d2417b 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -100,7 +100,7 @@ Node BVToInt::makeBinary(Node n) */ kind::Kind_t k = current.getKind(); if ((numChildren > 2) - && (k == kind::BITVECTOR_PLUS || k == kind::BITVECTOR_MULT + && (k == kind::BITVECTOR_ADD || k == kind::BITVECTOR_MULT || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_CONCAT)) { @@ -159,7 +159,7 @@ Node BVToInt::eliminationPass(Node n) CVC5_UNUSED kind::Kind_t k = current.getKind(); uint64_t numChildren = current.getNumChildren(); Assert((numChildren == 2) - || !(k == kind::BITVECTOR_PLUS || k == kind::BITVECTOR_MULT + || !(k == kind::BITVECTOR_ADD || k == kind::BITVECTOR_MULT || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_CONCAT)); toVisit.pop_back(); @@ -347,7 +347,7 @@ Node BVToInt::translateWithChildren(Node original, Node returnNode; switch (oldKind) { - case kind::BITVECTOR_PLUS: + case kind::BITVECTOR_ADD: { Assert(originalNumChildren == 2); uint64_t bvsize = original[0].getType().getBitVectorSize(); diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index 2f9fd28e6..779e0a931 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -140,7 +140,7 @@ Node intToBV(TNode n, NodeMap& cache) { case kind::PLUS: Assert(children.size() == 2); - newKind = kind::BITVECTOR_PLUS; + newKind = kind::BITVECTOR_ADD; max = max + 1; break; case kind::MULT: diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 0d4804310..54115bb54 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -454,7 +454,7 @@ void UnconstrainedSimplifier::processUnconstrained() case kind::XOR: case kind::BITVECTOR_XOR: case kind::BITVECTOR_XNOR: - case kind::BITVECTOR_PLUS: + case kind::BITVECTOR_ADD: case kind::BITVECTOR_SUB: checkParent = true; break; // Multiplication/division: must be non-integer and other operand must diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 8f433256d..42dfea308 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -702,8 +702,9 @@ void CvcPrinter::toStreamNode(std::ostream& out, op << "@"; opType = INFIX; break; - case kind::BITVECTOR_PLUS: { - // This interprets a BITVECTOR_PLUS as a bvadd in SMT-LIB + case kind::BITVECTOR_ADD: + { + // This interprets a BITVECTOR_ADD as a bvadd in SMT-LIB Assert(n.getType().isBitVector()); unsigned numc = n.getNumChildren()-2; unsigned child = 0; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 72d7fca89..2b1f16931 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -753,7 +753,10 @@ void Smt2Printer::toStream(std::ostream& out, case kind::BITVECTOR_XNOR: out << "bvxnor "; break; case kind::BITVECTOR_COMP: out << "bvcomp "; break; case kind::BITVECTOR_MULT: out << "bvmul "; forceBinary = true; break; - case kind::BITVECTOR_PLUS: out << "bvadd "; forceBinary = true; break; + case kind::BITVECTOR_ADD: + out << "bvadd "; + forceBinary = true; + break; case kind::BITVECTOR_SUB: out << "bvsub "; break; case kind::BITVECTOR_NEG: out << "bvneg "; break; case kind::BITVECTOR_UDIV: out << "bvudiv "; break; @@ -1157,7 +1160,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::BITVECTOR_XNOR: return "bvxnor"; case kind::BITVECTOR_COMP: return "bvcomp"; case kind::BITVECTOR_MULT: return "bvmul"; - case kind::BITVECTOR_PLUS: return "bvadd"; + case kind::BITVECTOR_ADD: return "bvadd"; case kind::BITVECTOR_SUB: return "bvsub"; case kind::BITVECTOR_NEG: return "bvneg"; case kind::BITVECTOR_UDIV: return "bvudiv"; diff --git a/src/smt_util/nary_builder.cpp b/src/smt_util/nary_builder.cpp index a5ab4a074..4fe1180be 100644 --- a/src/smt_util/nary_builder.cpp +++ b/src/smt_util/nary_builder.cpp @@ -129,7 +129,7 @@ bool RePairAssocCommutativeOperators::isAssociateCommutative(Kind k){ case BITVECTOR_OR: case BITVECTOR_XOR: case BITVECTOR_MULT: - case BITVECTOR_PLUS: + case BITVECTOR_ADD: case DISTINCT: case PLUS: case MULT: diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h index bb895fff2..f5259dc93 100644 --- a/src/theory/bv/bitblast/bitblast_strategies_template.h +++ b/src/theory/bv/bitblast/bitblast_strategies_template.h @@ -394,9 +394,11 @@ void DefaultMultBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { } template <class T> -void DefaultPlusBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_PLUS && res.size() == 0); +void DefaultAddBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb) +{ + Debug("bitvector-bb") << "theory::bv::DefaultAddBB bitblasting " << node + << "\n"; + Assert(node.getKind() == kind::BITVECTOR_ADD && res.size() == 0); bb->bbTerm(node[0], res); @@ -413,7 +415,6 @@ void DefaultPlusBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) { Assert(res.size() == utils::getSize(node)); } - template <class T> void DefaultSubBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) { Debug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n"; diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index a669e4a86..6e9444ba6 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -156,7 +156,7 @@ void TBitblaster<T>::initTermBBStrategies() d_termBBStrategies[kind::BITVECTOR_NOR] = DefaultNorBB<T>; d_termBBStrategies[kind::BITVECTOR_COMP] = DefaultCompBB<T>; d_termBBStrategies[kind::BITVECTOR_MULT] = DefaultMultBB<T>; - d_termBBStrategies[kind::BITVECTOR_PLUS] = DefaultPlusBB<T>; + d_termBBStrategies[kind::BITVECTOR_ADD] = DefaultAddBB<T>; d_termBBStrategies[kind::BITVECTOR_SUB] = DefaultSubBB<T>; d_termBBStrategies[kind::BITVECTOR_NEG] = DefaultNegBB<T>; d_termBBStrategies[kind::BITVECTOR_UDIV] = DefaultUdivBB<T>; diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp index 4d6501673..6082a7128 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.cpp +++ b/src/theory/bv/bitblast/proof_bitblaster.cpp @@ -46,7 +46,7 @@ std::unordered_map<Kind, PfRule, kind::KindHashFunction> {kind::BITVECTOR_NOR, PfRule::BV_BITBLAST_NOR}, {kind::BITVECTOR_COMP, PfRule::BV_BITBLAST_COMP}, {kind::BITVECTOR_MULT, PfRule::BV_BITBLAST_MULT}, - {kind::BITVECTOR_PLUS, PfRule::BV_BITBLAST_PLUS}, + {kind::BITVECTOR_ADD, PfRule::BV_BITBLAST_ADD}, {kind::BITVECTOR_SUB, PfRule::BV_BITBLAST_SUB}, {kind::BITVECTOR_NEG, PfRule::BV_BITBLAST_NEG}, {kind::BITVECTOR_UDIV, PfRule::BV_BITBLAST_UDIV}, diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp index 06ecea701..fbd910bee 100644 --- a/src/theory/bv/bv_solver_lazy.cpp +++ b/src/theory/bv/bv_solver_lazy.cpp @@ -434,15 +434,15 @@ TrustNode BVSolverLazy::ppRewrite(TNode t) Node result = RewriteRule<BitwiseEq>::run<false>(t); res = Rewriter::rewrite(result); } - else if (RewriteRule<UltPlusOne>::applies(t)) + else if (RewriteRule<UltAddOne>::applies(t)) { - Node result = RewriteRule<UltPlusOne>::run<false>(t); + Node result = RewriteRule<UltAddOne>::run<false>(t); res = Rewriter::rewrite(result); } else if (res.getKind() == kind::EQUAL - && ((res[0].getKind() == kind::BITVECTOR_PLUS + && ((res[0].getKind() == kind::BITVECTOR_ADD && RewriteRule<ConcatToMult>::applies(res[1])) - || (res[1].getKind() == kind::BITVECTOR_PLUS + || (res[1].getKind() == kind::BITVECTOR_ADD && RewriteRule<ConcatToMult>::applies(res[0])))) { Node mult = RewriteRule<ConcatToMult>::applies(res[0]) @@ -469,20 +469,20 @@ TrustNode BVSolverLazy::ppRewrite(TNode t) { res = RewriteRule<ZeroExtendEqConst>::run<false>(t); } - else if (RewriteRule<NormalizeEqPlusNeg>::applies(t)) + else if (RewriteRule<NormalizeEqAddNeg>::applies(t)) { - res = RewriteRule<NormalizeEqPlusNeg>::run<false>(t); + res = RewriteRule<NormalizeEqAddNeg>::run<false>(t); } // if(t.getKind() == kind::EQUAL && // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == - // kind::BITVECTOR_PLUS) || + // kind::BITVECTOR_ADD) || // (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() == - // kind::BITVECTOR_PLUS))) { + // kind::BITVECTOR_ADD))) { // // if we have an equality between a multiplication and addition // // try to express multiplication in terms of addition // Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1]; - // Node add = t[0].getKind() == kind::BITVECTOR_PLUS? t[0] : t[1]; + // Node add = t[0].getKind() == kind::BITVECTOR_ADD? t[0] : t[1]; // if (RewriteRule<MultSlice>::applies(mult)) { // Node new_mult = RewriteRule<MultSlice>::run<false>(mult); // Node new_eq = @@ -653,13 +653,13 @@ void BVSolverLazy::ppStaticLearn(TNode in, NodeBuilder& learned) if (in.getKind() == kind::EQUAL) { - if ((in[0].getKind() == kind::BITVECTOR_PLUS + if ((in[0].getKind() == kind::BITVECTOR_ADD && in[1].getKind() == kind::BITVECTOR_SHL) - || (in[1].getKind() == kind::BITVECTOR_PLUS + || (in[1].getKind() == kind::BITVECTOR_ADD && in[0].getKind() == kind::BITVECTOR_SHL)) { - TNode p = in[0].getKind() == kind::BITVECTOR_PLUS ? in[0] : in[1]; - TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0]; + TNode p = in[0].getKind() == kind::BITVECTOR_ADD ? in[0] : in[1]; + TNode s = in[0].getKind() == kind::BITVECTOR_ADD ? in[1] : in[0]; if (p.getNumChildren() == 2 && p[0].getKind() == kind::BITVECTOR_SHL && p[1].getKind() == kind::BITVECTOR_SHL) diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 7f3099f8c..7c97d1bbc 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -136,7 +136,7 @@ void CoreSolver::finishInit() // d_equalityEngine->addFunctionKind(kind::BITVECTOR_XNOR); // d_equalityEngine->addFunctionKind(kind::BITVECTOR_COMP); d_equalityEngine->addFunctionKind(kind::BITVECTOR_MULT, true); - d_equalityEngine->addFunctionKind(kind::BITVECTOR_PLUS, true); + d_equalityEngine->addFunctionKind(kind::BITVECTOR_ADD, true); d_equalityEngine->addFunctionKind(kind::BITVECTOR_EXTRACT, true); // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SUB); // d_equalityEngine->addFunctionKind(kind::BITVECTOR_NEG); diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 10b9a346e..aa93008c2 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -237,7 +237,7 @@ bool InequalitySolver::addInequality(TNode a, TNode b, bool strict, TNode fact) Node one = utils::mkConst(utils::getSize(a), 1); Node a_plus_one = Rewriter::rewrite( - NodeManager::currentNM()->mkNode(kind::BITVECTOR_PLUS, a, one)); + NodeManager::currentNM()->mkNode(kind::BITVECTOR_ADD, a, one)); if (d_ineqTerms.find(a_plus_one) != d_ineqTerms.end()) { ok = d_inequalityGraph.addInequality(a_plus_one, b, false, fact); diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index c9999d39b..6af586735 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -57,7 +57,7 @@ operator BITVECTOR_XNOR 2 "bitwise xnor of two bit-vectors" ## arithmetic kinds operator BITVECTOR_MULT 2: "multiplication of two or more bit-vectors" operator BITVECTOR_NEG 1 "unary negation of a bit-vector" -operator BITVECTOR_PLUS 2: "addition of two or more bit-vectors" +operator BITVECTOR_ADD 2: "addition of two or more bit-vectors" operator BITVECTOR_SUB 2 "subtraction of two bit-vectors" operator BITVECTOR_UDIV 2 "unsigned division of two bit-vectors, truncating towards 0 (defined to be the all-ones bit pattern, if divisor is 0)" operator BITVECTOR_UREM 2 "unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend, if divisor is 0)" @@ -179,7 +179,7 @@ typerule BITVECTOR_XOR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule ## arithmetic kinds typerule BITVECTOR_MULT ::cvc5::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_NEG ::cvc5::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_PLUS ::cvc5::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_ADD ::cvc5::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_SUB ::cvc5::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_UDIV ::cvc5::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_UREM ::cvc5::theory::bv::BitVectorFixedWidthTypeRule diff --git a/src/theory/bv/proof_checker.cpp b/src/theory/bv/proof_checker.cpp index b8ede6386..93ba9e67f 100644 --- a/src/theory/bv/proof_checker.cpp +++ b/src/theory/bv/proof_checker.cpp @@ -43,7 +43,7 @@ void BVProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::BV_BITBLAST_NOR, this); pc->registerChecker(PfRule::BV_BITBLAST_COMP, this); pc->registerChecker(PfRule::BV_BITBLAST_MULT, this); - pc->registerChecker(PfRule::BV_BITBLAST_PLUS, this); + pc->registerChecker(PfRule::BV_BITBLAST_ADD, this); pc->registerChecker(PfRule::BV_BITBLAST_SUB, this); pc->registerChecker(PfRule::BV_BITBLAST_NEG, this); pc->registerChecker(PfRule::BV_BITBLAST_UDIV, this); @@ -89,7 +89,7 @@ Node BVProofRuleChecker::checkInternal(PfRule id, || id == PfRule::BV_BITBLAST_OR || id == PfRule::BV_BITBLAST_XOR || id == PfRule::BV_BITBLAST_XNOR || id == PfRule::BV_BITBLAST_NAND || id == PfRule::BV_BITBLAST_NOR || id == PfRule::BV_BITBLAST_COMP - || id == PfRule::BV_BITBLAST_MULT || id == PfRule::BV_BITBLAST_PLUS + || id == PfRule::BV_BITBLAST_MULT || id == PfRule::BV_BITBLAST_ADD || id == PfRule::BV_BITBLAST_SUB || id == PfRule::BV_BITBLAST_NEG || id == PfRule::BV_BITBLAST_UDIV || id == PfRule::BV_BITBLAST_UREM || id == PfRule::BV_BITBLAST_SDIV || id == PfRule::BV_BITBLAST_SREM diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 296fca2c0..c5ab08f0c 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -112,7 +112,7 @@ void TheoryBV::finishInit() // ee->addFunctionKind(kind::BITVECTOR_XNOR); // ee->addFunctionKind(kind::BITVECTOR_COMP); ee->addFunctionKind(kind::BITVECTOR_MULT, true); - ee->addFunctionKind(kind::BITVECTOR_PLUS, true); + ee->addFunctionKind(kind::BITVECTOR_ADD, true); ee->addFunctionKind(kind::BITVECTOR_EXTRACT, true); // ee->addFunctionKind(kind::BITVECTOR_SUB); // ee->addFunctionKind(kind::BITVECTOR_NEG); diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 7fe9559f9..040d2c53f 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -89,7 +89,7 @@ enum RewriteRuleId EvalXor, EvalNot, EvalMult, - EvalPlus, + EvalAdd, EvalUdiv, EvalUrem, EvalShl, @@ -181,14 +181,14 @@ enum RewriteRuleId DoubleNeg, NegMult, NegSub, - NegPlus, + NegAdd, NotConcat, NotAnd, // not sure why this would help (not done) NotOr, // not sure why this would help (not done) NotXor, // not sure why this would help (not done) FlattenAssocCommut, FlattenAssocCommutNoDuplicates, - PlusCombineLikeTerms, + AddCombineLikeTerms, MultSimplify, MultDistribConst, MultDistrib, @@ -198,10 +198,10 @@ enum RewriteRuleId OrSimplify, XorSimplify, BitwiseSlicing, - NormalizeEqPlusNeg, + NormalizeEqAddNeg, // rules to simplify bitblasting - BBPlusNeg, - UltPlusOne, + BBAddNeg, + UltAddOne, ConcatToMult, IsPowerOfTwo, MultSltMult, @@ -258,7 +258,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case EvalXor : out << "EvalXor"; return out; case EvalNot : out << "EvalNot"; return out; case EvalMult : out << "EvalMult"; return out; - case EvalPlus : out << "EvalPlus"; return out; + case EvalAdd: out << "EvalAdd"; return out; case EvalUdiv : out << "EvalUdiv"; return out; case EvalUrem : out << "EvalUrem"; return out; case EvalShl : out << "EvalShl"; return out; @@ -340,8 +340,10 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case NotIdemp : out << "NotIdemp"; return out; case UleSelf: out << "UleSelf"; return out; case FlattenAssocCommut: out << "FlattenAssocCommut"; return out; - case FlattenAssocCommutNoDuplicates: out << "FlattenAssocCommutNoDuplicates"; return out; - case PlusCombineLikeTerms: out << "PlusCombineLikeTerms"; return out; + case FlattenAssocCommutNoDuplicates: + out << "FlattenAssocCommutNoDuplicates"; + return out; + case AddCombineLikeTerms: out << "AddCombineLikeTerms"; return out; case MultSimplify: out << "MultSimplify"; return out; case MultDistribConst: out << "MultDistribConst"; return out; case SolveEq : out << "SolveEq"; return out; @@ -351,8 +353,8 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case AndSimplify : out << "AndSimplify"; return out; case OrSimplify : out << "OrSimplify"; return out; case XorSimplify : out << "XorSimplify"; return out; - case NegPlus : out << "NegPlus"; return out; - case BBPlusNeg : out << "BBPlusNeg"; return out; + case NegAdd: out << "NegAdd"; return out; + case BBAddNeg: out << "BBAddNeg"; return out; case UltOne : out << "UltOne"; return out; case SltZero : out << "SltZero"; return out; case ZeroUlt : out << "ZeroUlt"; return out; @@ -366,11 +368,11 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case BitwiseSlicing : out << "BitwiseSlicing"; return out; case ExtractSignExtend : out << "ExtractSignExtend"; return out; case MultDistrib: out << "MultDistrib"; return out; - case UltPlusOne: out << "UltPlusOne"; return out; + case UltAddOne: out << "UltAddOne"; return out; case ConcatToMult: out << "ConcatToMult"; return out; case IsPowerOfTwo: out << "IsPowerOfTwo"; return out; case MultSltMult: out << "MultSltMult"; return out; - case NormalizeEqPlusNeg: out << "NormalizeEqPlusNeg"; return out; + case NormalizeEqAddNeg: out << "NormalizeEqAddNeg"; return out; case BitOfConst: out << "BitOfConst"; return out; default: Unreachable(); @@ -513,7 +515,7 @@ struct AllRewriteRules { RewriteRule<EvalNot> rule29; RewriteRule<EvalSlt> rule30; RewriteRule<EvalMult> rule31; - RewriteRule<EvalPlus> rule32; + RewriteRule<EvalAdd> rule32; RewriteRule<XorSimplify> rule33; RewriteRule<EvalUdiv> rule34; RewriteRule<EvalUrem> rule35; @@ -582,13 +584,13 @@ struct AllRewriteRules { RewriteRule<NotIdemp> rule102; RewriteRule<UleSelf> rule103; RewriteRule<FlattenAssocCommut> rule104; - RewriteRule<PlusCombineLikeTerms> rule105; + RewriteRule<AddCombineLikeTerms> rule105; RewriteRule<MultSimplify> rule106; RewriteRule<MultDistribConst> rule107; RewriteRule<AndSimplify> rule108; RewriteRule<OrSimplify> rule109; - RewriteRule<NegPlus> rule110; - RewriteRule<BBPlusNeg> rule111; + RewriteRule<NegAdd> rule110; + RewriteRule<BBAddNeg> rule111; RewriteRule<SolveEq> rule112; RewriteRule<BitwiseEq> rule113; RewriteRule<UltOne> rule114; @@ -596,7 +598,7 @@ struct AllRewriteRules { RewriteRule<BVToNatEliminate> rule116; RewriteRule<IntToBVEliminate> rule117; RewriteRule<MultDistrib> rule118; - RewriteRule<UltPlusOne> rule119; + RewriteRule<UltAddOne> rule119; RewriteRule<ConcatToMult> rule120; RewriteRule<IsPowerOfTwo> rule121; RewriteRule<RedorEliminate> rule122; @@ -606,7 +608,7 @@ struct AllRewriteRules { RewriteRule<SignExtendUltConst> rule126; RewriteRule<ZeroExtendUltConst> rule127; RewriteRule<MultSltMult> rule128; - RewriteRule<NormalizeEqPlusNeg> rule129; + RewriteRule<NormalizeEqAddNeg> rule129; RewriteRule<BvComp> rule130; RewriteRule<BvIteConstCond> rule131; RewriteRule<BvIteEqualChildren> rule132; diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h index 1c229ed72..af80ad00b 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -151,15 +151,16 @@ Node RewriteRule<EvalMult>::apply(TNode node) { return utils::mkConst(res); } -template<> inline -bool RewriteRule<EvalPlus>::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_PLUS && - utils::isBvConstTerm(node)); +template <> +inline bool RewriteRule<EvalAdd>::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_ADD && utils::isBvConstTerm(node)); } -template<> inline -Node RewriteRule<EvalPlus>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<EvalPlus>(" << node << ")" << std::endl; +template <> +inline Node RewriteRule<EvalAdd>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<EvalAdd>(" << node << ")" << std::endl; TNode::iterator child_it = node.begin(); BitVector res = (*child_it).getConst<BitVector>(); for(++child_it; child_it != node.end(); ++child_it) { diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 4a2d2943d..45e313e48 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -146,10 +146,10 @@ inline Node RewriteRule<ExtractSignExtend>::apply(TNode node) template<> inline bool RewriteRule<ExtractArith>::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_EXTRACT && - utils::getExtractLow(node) == 0 && - (node[0].getKind() == kind::BITVECTOR_PLUS || - node[0].getKind() == kind::BITVECTOR_MULT)); + return (node.getKind() == kind::BITVECTOR_EXTRACT + && utils::getExtractLow(node) == 0 + && (node[0].getKind() == kind::BITVECTOR_ADD + || node[0].getKind() == kind::BITVECTOR_MULT)); } template <> @@ -178,9 +178,9 @@ inline Node RewriteRule<ExtractArith>::apply(TNode node) // careful not to apply in a loop template<> inline bool RewriteRule<ExtractArith2>::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_EXTRACT && - (node[0].getKind() == kind::BITVECTOR_PLUS || - node[0].getKind() == kind::BITVECTOR_MULT)); + return (node.getKind() == kind::BITVECTOR_EXTRACT + && (node[0].getKind() == kind::BITVECTOR_ADD + || node[0].getKind() == kind::BITVECTOR_MULT)); } template <> @@ -204,11 +204,9 @@ inline Node RewriteRule<ExtractArith2>::apply(TNode node) template<> inline bool RewriteRule<FlattenAssocCommut>::applies(TNode node) { Kind kind = node.getKind(); - if (kind != kind::BITVECTOR_PLUS && - kind != kind::BITVECTOR_MULT && - kind != kind::BITVECTOR_OR && - kind != kind::BITVECTOR_XOR && - kind != kind::BITVECTOR_AND) + if (kind != kind::BITVECTOR_ADD && kind != kind::BITVECTOR_MULT + && kind != kind::BITVECTOR_OR && kind != kind::BITVECTOR_XOR + && kind != kind::BITVECTOR_AND) return false; TNode::iterator child_it = node.begin(); for(; child_it != node.end(); ++child_it) { @@ -247,7 +245,7 @@ inline Node RewriteRule<FlattenAssocCommut>::apply(TNode node) children.push_back(current); } } - if (node.getKind() == kind::BITVECTOR_PLUS + if (node.getKind() == kind::BITVECTOR_ADD || node.getKind() == kind::BITVECTOR_MULT) { return utils::mkNaryNode(kind, children); @@ -371,15 +369,16 @@ static inline void addToChildren(TNode term, } } -template<> inline -bool RewriteRule<PlusCombineLikeTerms>::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_PLUS); +template <> +inline bool RewriteRule<AddCombineLikeTerms>::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_ADD); } template <> -inline Node RewriteRule<PlusCombineLikeTerms>::apply(TNode node) +inline Node RewriteRule<AddCombineLikeTerms>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<PlusCombineLikeTerms>(" << node << ")" + Debug("bv-rewrite") << "RewriteRule<AddCombineLikeTerms>(" << node << ")" << std::endl; unsigned size = utils::getSize(node); BitVector constSum(size, (unsigned)0); @@ -419,9 +418,8 @@ inline Node RewriteRule<PlusCombineLikeTerms>::apply(TNode node) return node; } - return csize == 0 - ? utils::mkZero(size) - : utils::mkNaryNode(kind::BITVECTOR_PLUS, children); + return csize == 0 ? utils::mkZero(size) + : utils::mkNaryNode(kind::BITVECTOR_ADD, children); } template<> inline @@ -508,9 +506,9 @@ bool RewriteRule<MultDistribConst>::applies(TNode node) { return false; } TNode factor = node[0]; - return (factor.getKind() == kind::BITVECTOR_PLUS || - factor.getKind() == kind::BITVECTOR_SUB || - factor.getKind() == kind::BITVECTOR_NEG); + return (factor.getKind() == kind::BITVECTOR_ADD + || factor.getKind() == kind::BITVECTOR_SUB + || factor.getKind() == kind::BITVECTOR_NEG); } template <> @@ -547,13 +545,14 @@ bool RewriteRule<MultDistrib>::applies(TNode node) { node.getNumChildren() != 2) { return false; } - if (node[0].getKind() == kind::BITVECTOR_PLUS || - node[0].getKind() == kind::BITVECTOR_SUB) { - return node[1].getKind() != kind::BITVECTOR_PLUS && - node[1].getKind() != kind::BITVECTOR_SUB; + if (node[0].getKind() == kind::BITVECTOR_ADD + || node[0].getKind() == kind::BITVECTOR_SUB) + { + return node[1].getKind() != kind::BITVECTOR_ADD + && node[1].getKind() != kind::BITVECTOR_SUB; } - return node[1].getKind() == kind::BITVECTOR_PLUS || - node[1].getKind() == kind::BITVECTOR_SUB; + return node[1].getKind() == kind::BITVECTOR_ADD + || node[1].getKind() == kind::BITVECTOR_SUB; } template <> @@ -563,13 +562,13 @@ inline Node RewriteRule<MultDistrib>::apply(TNode node) << std::endl; NodeManager *nm = NodeManager::currentNM(); - bool is_rhs_factor = node[0].getKind() == kind::BITVECTOR_PLUS + bool is_rhs_factor = node[0].getKind() == kind::BITVECTOR_ADD || node[0].getKind() == kind::BITVECTOR_SUB; TNode factor = !is_rhs_factor ? node[0] : node[1]; TNode sum = is_rhs_factor ? node[0] : node[1]; - Assert(factor.getKind() != kind::BITVECTOR_PLUS + Assert(factor.getKind() != kind::BITVECTOR_ADD && factor.getKind() != kind::BITVECTOR_SUB - && (sum.getKind() == kind::BITVECTOR_PLUS + && (sum.getKind() == kind::BITVECTOR_ADD || sum.getKind() == kind::BITVECTOR_SUB)); std::vector<Node> children; @@ -643,7 +642,7 @@ inline Node RewriteRule<SolveEq>::apply(TNode node) std::map<Node, BitVector> leftMap, rightMap; // Collect terms and coefficients plus constant for left - if (left.getKind() == kind::BITVECTOR_PLUS) + if (left.getKind() == kind::BITVECTOR_ADD) { for (unsigned i = 0; i < left.getNumChildren(); ++i) { @@ -660,7 +659,7 @@ inline Node RewriteRule<SolveEq>::apply(TNode node) } // Collect terms and coefficients plus constant for right - if (right.getKind() == kind::BITVECTOR_PLUS) + if (right.getKind() == kind::BITVECTOR_ADD) { for (unsigned i = 0; i < right.getNumChildren(); ++i) { @@ -819,7 +818,7 @@ inline Node RewriteRule<SolveEq>::apply(TNode node) } else { - newLeft = utils::mkNaryNode(kind::BITVECTOR_PLUS, childrenLeft); + newLeft = utils::mkNaryNode(kind::BITVECTOR_ADD, childrenLeft); } if (childrenRight.size() == 0) @@ -828,7 +827,7 @@ inline Node RewriteRule<SolveEq>::apply(TNode node) } else { - newRight = utils::mkNaryNode(kind::BITVECTOR_PLUS, childrenRight); + newRight = utils::mkNaryNode(kind::BITVECTOR_ADD, childrenRight); } if (!changed) @@ -1018,23 +1017,24 @@ inline Node RewriteRule<NegSub>::apply(TNode node) kind::BITVECTOR_SUB, node[0][1], node[0][0]); } -template<> inline -bool RewriteRule<NegPlus>::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_NEG && - node[0].getKind() == kind::BITVECTOR_PLUS); +template <> +inline bool RewriteRule<NegAdd>::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_NEG + && node[0].getKind() == kind::BITVECTOR_ADD); } template <> -inline Node RewriteRule<NegPlus>::apply(TNode node) +inline Node RewriteRule<NegAdd>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<NegPlus>(" << node << ")" << std::endl; + Debug("bv-rewrite") << "RewriteRule<NegAdd>(" << node << ")" << std::endl; NodeManager *nm = NodeManager::currentNM(); std::vector<Node> children; for (unsigned i = 0; i < node[0].getNumChildren(); ++i) { children.push_back(nm->mkNode(kind::BITVECTOR_NEG, node[0][i])); } - return utils::mkNaryNode(kind::BITVECTOR_PLUS, children); + return utils::mkNaryNode(kind::BITVECTOR_ADD, children); } struct Count { @@ -1480,24 +1480,24 @@ inline Node RewriteRule<BitwiseSlicing>::apply(TNode node) } template <> -inline bool RewriteRule<NormalizeEqPlusNeg>::applies(TNode node) +inline bool RewriteRule<NormalizeEqAddNeg>::applies(TNode node) { return node.getKind() == kind::EQUAL - && (node[0].getKind() == kind::BITVECTOR_PLUS - || node[1].getKind() == kind::BITVECTOR_PLUS); + && (node[0].getKind() == kind::BITVECTOR_ADD + || node[1].getKind() == kind::BITVECTOR_ADD); } template <> -inline Node RewriteRule<NormalizeEqPlusNeg>::apply(TNode node) +inline Node RewriteRule<NormalizeEqAddNeg>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<NormalizeEqPlusNeg>(" << node << ")" + Debug("bv-rewrite") << "RewriteRule<NormalizeEqAddNeg>(" << node << ")" << std::endl; - NodeBuilder nb_lhs(kind::BITVECTOR_PLUS); - NodeBuilder nb_rhs(kind::BITVECTOR_PLUS); + NodeBuilder nb_lhs(kind::BITVECTOR_ADD); + NodeBuilder nb_rhs(kind::BITVECTOR_ADD); NodeManager *nm = NodeManager::currentNM(); - if (node[0].getKind() == kind::BITVECTOR_PLUS) + if (node[0].getKind() == kind::BITVECTOR_ADD) { for (const TNode &n : node[0]) { @@ -1512,7 +1512,7 @@ inline Node RewriteRule<NormalizeEqPlusNeg>::apply(TNode node) nb_lhs << node[0]; } - if (node[1].getKind() == kind::BITVECTOR_PLUS) + if (node[1].getKind() == kind::BITVECTOR_ADD) { for (const TNode &n : node[1]) { 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 023bbf55c..e44d1c9b7 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -50,8 +50,7 @@ inline Node RewriteRule<NegEliminate>::apply(TNode node) unsigned size = utils::getSize(a); Node one = utils::mkOne(size); Node nota = nm->mkNode(kind::BITVECTOR_NOT, a); - Node bvadd = - nm->mkNode(kind::BITVECTOR_PLUS, nota, one); + Node bvadd = nm->mkNode(kind::BITVECTOR_ADD, nota, one); return bvadd; } @@ -75,7 +74,7 @@ inline Node RewriteRule<OrEliminate>::apply(TNode node) NodeManager* nm = NodeManager::currentNM(); TNode a = node[0]; TNode b = node[1]; - Node bvadd = nm->mkNode(kind::BITVECTOR_PLUS, a, b); + Node bvadd = nm->mkNode(kind::BITVECTOR_ADD, a, b); Node bvand = nm->mkNode(kind::BITVECTOR_AND, a, b); Node result = nm->mkNode(kind::BITVECTOR_SUB, bvadd, bvand); @@ -191,8 +190,8 @@ inline Node RewriteRule<SltEliminate>::apply(TNode node) unsigned size = utils::getSize(node[0]); Integer val = Integer(1).multiplyByPow2(size - 1); Node pow_two = utils::mkConst(size, val); - Node a = nm->mkNode(kind::BITVECTOR_PLUS, node[0], pow_two); - Node b = nm->mkNode(kind::BITVECTOR_PLUS, node[1], pow_two); + Node a = nm->mkNode(kind::BITVECTOR_ADD, node[0], pow_two); + Node b = nm->mkNode(kind::BITVECTOR_ADD, node[1], pow_two); return nm->mkNode(kind::BITVECTOR_ULT, a, b); } @@ -267,7 +266,7 @@ inline Node RewriteRule<SubEliminate>::apply(TNode node) Node negb = nm->mkNode(kind::BITVECTOR_NEG, node[1]); Node a = node[0]; - return nm->mkNode(kind::BITVECTOR_PLUS, a, negb); + return nm->mkNode(kind::BITVECTOR_ADD, a, negb); } template <> @@ -636,8 +635,8 @@ inline Node RewriteRule<SmodEliminate>::apply(TNode node) cond1.iteNode( u, cond2.iteNode( - nm->mkNode(kind::BITVECTOR_PLUS, neg_u, t), - cond3.iteNode(nm->mkNode(kind::BITVECTOR_PLUS, u, t), neg_u)))); + nm->mkNode(kind::BITVECTOR_ADD, neg_u, t), + cond3.iteNode(nm->mkNode(kind::BITVECTOR_ADD, u, t), neg_u)))); return result; } @@ -703,8 +702,8 @@ inline Node RewriteRule<SmodEliminateFewerBitwiseOps>::apply(TNode node) cond1.iteNode( u, cond2.iteNode( - nm->mkNode(kind::BITVECTOR_PLUS, neg_u, t), - cond3.iteNode(nm->mkNode(kind::BITVECTOR_PLUS, u, t), neg_u)))); + nm->mkNode(kind::BITVECTOR_ADD, neg_u, t), + cond3.iteNode(nm->mkNode(kind::BITVECTOR_ADD, u, t), neg_u)))); return result; } diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 949dbce1a..1e38aba0f 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -1610,16 +1610,18 @@ inline Node RewriteRule<UgtUrem>::apply(TNode node) /* -------------------------------------------------------------------------- */ /** - * BBPlusNeg - * + * BBAddNeg + * * -a1 - a2 - ... - an + ak + .. ==> - (a1 + a2 + ... + an) + ak * */ -template<> inline -bool RewriteRule<BBPlusNeg>::applies(TNode node) { - if (node.getKind() != kind::BITVECTOR_PLUS) { - return false; +template <> +inline bool RewriteRule<BBAddNeg>::applies(TNode node) +{ + if (node.getKind() != kind::BITVECTOR_ADD) + { + return false; } unsigned neg_count = 0; @@ -1632,9 +1634,9 @@ bool RewriteRule<BBPlusNeg>::applies(TNode node) { } template <> -inline Node RewriteRule<BBPlusNeg>::apply(TNode node) +inline Node RewriteRule<BBAddNeg>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<BBPlusNeg>(" << node << ")" << std::endl; + Debug("bv-rewrite") << "RewriteRule<BBAddNeg>(" << node << ")" << std::endl; NodeManager *nm = NodeManager::currentNM(); std::vector<Node> children; unsigned neg_count = 0; @@ -1653,7 +1655,7 @@ inline Node RewriteRule<BBPlusNeg>::apply(TNode node) Assert(neg_count != 0); children.push_back(utils::mkConst(utils::getSize(node), neg_count)); - return utils::mkNaryNode(kind::BITVECTOR_PLUS, children); + return utils::mkNaryNode(kind::BITVECTOR_ADD, children); } /* -------------------------------------------------------------------------- */ @@ -2003,7 +2005,7 @@ inline Node RewriteRule<MultSlice>::apply(TNode node) Node term3 = nm->mkNode(kind::BITVECTOR_CONCAT, nm->mkNode(kind::BITVECTOR_MULT, top_a, bottom_b), zeros); - return nm->mkNode(kind::BITVECTOR_PLUS, term1, term2, term3); + return nm->mkNode(kind::BITVECTOR_ADD, term1, term2, term3); } /* -------------------------------------------------------------------------- */ @@ -2015,12 +2017,13 @@ inline Node RewriteRule<MultSlice>::apply(TNode node) * * @return */ -template<> inline -bool RewriteRule<UltPlusOne>::applies(TNode node) { +template <> +inline bool RewriteRule<UltAddOne>::applies(TNode node) +{ if (node.getKind() != kind::BITVECTOR_ULT) return false; TNode x = node[0]; TNode y1 = node[1]; - if (y1.getKind() != kind::BITVECTOR_PLUS) return false; + if (y1.getKind() != kind::BITVECTOR_ADD) return false; if (y1[0].getKind() != kind::CONST_BITVECTOR && y1[1].getKind() != kind::CONST_BITVECTOR) return false; @@ -2034,13 +2037,13 @@ bool RewriteRule<UltPlusOne>::applies(TNode node) { TNode one = y1[0].getKind() == kind::CONST_BITVECTOR ? y1[0] : y1[1]; if (one != utils::mkConst(utils::getSize(one), 1)) return false; - return true; + return true; } template <> -inline Node RewriteRule<UltPlusOne>::apply(TNode node) +inline Node RewriteRule<UltAddOne>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<UltPlusOne>(" << node << ")" << std::endl; + Debug("bv-rewrite") << "RewriteRule<UltAddOne>(" << node << ")" << std::endl; NodeManager *nm = NodeManager::currentNM(); TNode x = node[0]; TNode y1 = node[1]; @@ -2188,12 +2191,12 @@ bool RewriteRule<MultSltMult>::applies(TNode node) return false; TNode addxt, x, a; - if (ml[0].getKind() == kind::BITVECTOR_PLUS) + if (ml[0].getKind() == kind::BITVECTOR_ADD) { addxt = ml[0]; a = ml[1]; } - else if (ml[1].getKind() == kind::BITVECTOR_PLUS) + else if (ml[1].getKind() == kind::BITVECTOR_ADD) { addxt = ml[1]; a = ml[0]; @@ -2228,14 +2231,14 @@ Node RewriteRule<MultSltMult>::apply(TNode node) std::tie(mr[0], mr[1], std::ignore) = extract_ext_tuple(node[1]); TNode addxt, x, t, a; - if (ml[0].getKind() == kind::BITVECTOR_PLUS) + if (ml[0].getKind() == kind::BITVECTOR_ADD) { addxt = ml[0]; a = ml[1]; } else { - Assert(ml[1].getKind() == kind::BITVECTOR_PLUS); + Assert(ml[1].getKind() == kind::BITVECTOR_ADD); addxt = ml[1]; a = ml[0]; } diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index bda212351..d0579703d 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -412,7 +412,8 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool prerewrite) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool prerewrite) { +RewriteResponse TheoryBVRewriter::RewriteAdd(TNode node, bool prerewrite) +{ Node resultNode = node; if (prerewrite) { resultNode = LinearRewriteStrategy @@ -420,17 +421,16 @@ RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool prerewrite) { >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); } - - resultNode = LinearRewriteStrategy - < RewriteRule<FlattenAssocCommut>, - RewriteRule<PlusCombineLikeTerms> - >::apply(node); + + resultNode = + LinearRewriteStrategy<RewriteRule<FlattenAssocCommut>, + RewriteRule<AddCombineLikeTerms>>::apply(node); if (node != resultNode) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } - - return RewriteResponse(REWRITE_DONE, resultNode); + + return RewriteResponse(REWRITE_DONE, resultNode); } RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool prerewrite){ @@ -450,12 +450,13 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool prerewrite) { RewriteRule<NegIdemp>, RewriteRule<NegSub> >::apply(node); - - if (RewriteRule<NegPlus>::applies(node)) { - resultNode = RewriteRule<NegPlus>::run<false>(node); - return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + + if (RewriteRule<NegAdd>::applies(node)) + { + resultNode = RewriteRule<NegAdd>::run<false>(node); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } - + if(!prerewrite) { if (RewriteRule<NegMult>::applies(node)) { resultNode = RewriteRule<NegMult>::run<false>(node); @@ -718,7 +719,7 @@ void TheoryBVRewriter::initializeRewrites() { d_rewriteTable [ kind::BITVECTOR_NOR ] = RewriteNor; d_rewriteTable [ kind::BITVECTOR_COMP ] = RewriteComp; d_rewriteTable [ kind::BITVECTOR_MULT ] = RewriteMult; - d_rewriteTable [ kind::BITVECTOR_PLUS ] = RewritePlus; + d_rewriteTable[kind::BITVECTOR_ADD] = RewriteAdd; d_rewriteTable [ kind::BITVECTOR_SUB ] = RewriteSub; d_rewriteTable [ kind::BITVECTOR_NEG ] = RewriteNeg; d_rewriteTable [ kind::BITVECTOR_UDIV ] = RewriteUdiv; diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 56eb718df..9dc1ab351 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -76,7 +76,7 @@ class TheoryBVRewriter : public TheoryRewriter static RewriteResponse RewriteNor(TNode node, bool prerewrite = false); static RewriteResponse RewriteComp(TNode node, bool prerewrite = false); static RewriteResponse RewriteMult(TNode node, bool prerewrite = false); - static RewriteResponse RewritePlus(TNode node, bool prerewrite = false); + static RewriteResponse RewriteAdd(TNode node, bool prerewrite = false); static RewriteResponse RewriteSub(TNode node, bool prerewrite = false); static RewriteResponse RewriteNeg(TNode node, bool prerewrite = false); static RewriteResponse RewriteUdiv(TNode node, bool prerewrite = false); diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index 1549df639..927a40b82 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -398,7 +398,7 @@ Node mkConcat(TNode node, unsigned repeat) Node mkInc(TNode t) { return NodeManager::currentNM()->mkNode( - kind::BITVECTOR_PLUS, t, mkOne(getSize(t))); + kind::BITVECTOR_ADD, t, mkOne(getSize(t))); } Node mkDec(TNode t) diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 8e916e975..fca449917 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -118,7 +118,7 @@ Node mkNaryNode(Kind k, const std::vector<NodeTemplate<ref_count>>& nodes) { Assert(k == kind::AND || k == kind::OR || k == kind::XOR || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR - || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_PLUS + || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_ADD || k == kind::BITVECTOR_SUB || k == kind::BITVECTOR_MULT); if (nodes.size() == 1) { return nodes[0]; } diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp index da6ff9803..36dfc710b 100644 --- a/src/theory/datatypes/sygus_simple_sym.cpp +++ b/src/theory/datatypes/sygus_simple_sym.cpp @@ -336,11 +336,11 @@ bool SygusSimpleSymBreak::considerArgKind( // (~ (- y z) x) ----> (~ y (+ x z)) rt.d_req_kind = pk; rt.d_children[arg].d_req_type = dt[c].getArgType(0); - rt.d_children[oarg].d_req_kind = k == MINUS ? PLUS : BITVECTOR_PLUS; + rt.d_children[oarg].d_req_kind = k == MINUS ? PLUS : BITVECTOR_ADD; rt.d_children[oarg].d_children[0].d_req_type = pdt[pc].getArgType(oarg); rt.d_children[oarg].d_children[1].d_req_type = dt[c].getArgType(1); } - else if (pk == PLUS || pk == BITVECTOR_PLUS) + else if (pk == PLUS || pk == BITVECTOR_ADD) { // (+ x (- y z)) -----> (- (+ x y) z) // (+ (- y z) x) -----> (- (+ x y) z) diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index c0a3a2a2f..07a4e4b85 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -734,7 +734,7 @@ EvalResult Evaluator::evalInternal( break; } - case kind::BITVECTOR_PLUS: + case kind::BITVECTOR_ADD: { BitVector res = results[currNode[0]].d_bv; for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index a2306cc6a..3a058772c 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -477,7 +477,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator+( const symbolicBitVector<isSigned> &op) const { return symbolicBitVector<isSigned>( - NodeManager::currentNM()->mkNode(kind::BITVECTOR_PLUS, *this, op)); + NodeManager::currentNM()->mkNode(kind::BITVECTOR_ADD, *this, op)); } template <bool isSigned> @@ -530,7 +530,7 @@ template <bool isSigned> symbolicBitVector<isSigned> symbolicBitVector<isSigned>::increment() const { return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode( - kind::BITVECTOR_PLUS, *this, one(this->getWidth()))); + kind::BITVECTOR_ADD, *this, one(this->getWidth()))); } template <bool isSigned> diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 86444b8cf..fd204fffd 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -108,7 +108,7 @@ static bool isInvertible(Kind k, unsigned index) return k == NOT || k == EQUAL || k == BITVECTOR_ULT || k == BITVECTOR_SLT || k == BITVECTOR_COMP || k == BITVECTOR_NOT || k == BITVECTOR_NEG || k == BITVECTOR_CONCAT || k == BITVECTOR_SIGN_EXTEND - || k == BITVECTOR_PLUS || k == BITVECTOR_MULT || k == BITVECTOR_UREM + || k == BITVECTOR_ADD || k == BITVECTOR_MULT || k == BITVECTOR_UREM || k == BITVECTOR_UDIV || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR || k == BITVECTOR_LSHR || k == BITVECTOR_ASHR || k == BITVECTOR_SHL; @@ -284,7 +284,7 @@ Node BvInverter::solveBvLit(Node sv, { t = nm->mkNode(k, t); } - else if (litk == EQUAL && k == BITVECTOR_PLUS) + else if (litk == EQUAL && k == BITVECTOR_ADD) { t = nm->mkNode(BITVECTOR_SUB, t, s); } diff --git a/src/theory/quantifiers/bv_inverter_utils.cpp b/src/theory/quantifiers/bv_inverter_utils.cpp index ff932cf15..e7427178a 100644 --- a/src/theory/quantifiers/bv_inverter_utils.cpp +++ b/src/theory/quantifiers/bv_inverter_utils.cpp @@ -327,7 +327,7 @@ Node getICBvUrem( * (or (= t z) (distinct (bvsub s (_ bv1 w)) t)))) * where * z = 0 with getSize(z) = w */ - Node add = nm->mkNode(BITVECTOR_PLUS, t, t); + Node add = nm->mkNode(BITVECTOR_ADD, t, t); Node sub = nm->mkNode(BITVECTOR_SUB, add, s); Node a = nm->mkNode(BITVECTOR_AND, sub, s); scl = nm->mkNode(BITVECTOR_UGE, a, t); @@ -386,7 +386,7 @@ Node getICBvUrem( * (or * (bvuge (bvand (bvsub (bvadd t t) s) s) t) ; eq, synthesized * (bvult t s)) ; ugt, synthesized */ - Node add = nm->mkNode(BITVECTOR_PLUS, t, t); + Node add = nm->mkNode(BITVECTOR_ADD, t, t); Node sub = nm->mkNode(BITVECTOR_SUB, add, s); Node a = nm->mkNode(BITVECTOR_AND, sub, s); Node sceq = nm->mkNode(BITVECTOR_UGE, a, t); @@ -1920,7 +1920,7 @@ Node getICBvShl( * min is the signed minimum value with getSize(min) = w */ Node min = bv::utils::mkMinSigned(w); Node shl = nm->mkNode(BITVECTOR_SHL, min, s); - Node add = nm->mkNode(BITVECTOR_PLUS, t, min); + Node add = nm->mkNode(BITVECTOR_ADD, t, min); scl = nm->mkNode(BITVECTOR_ULT, shl, add); } else diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index ec15b926f..9ffb31df3 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -184,7 +184,7 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, Assert(slack.isConst()); // remember the slack value for the asserted literal d_alit_to_model_slack[lit] = slack; - ret = nm->mkNode(EQUAL, s, nm->mkNode(BITVECTOR_PLUS, t, slack)); + ret = nm->mkNode(EQUAL, s, nm->mkNode(BITVECTOR_ADD, t, slack)); Trace("cegqi-bv") << "Slack is " << slack << std::endl; } else @@ -218,7 +218,7 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, else { Node bv_one = bv::utils::mkOne(bv::utils::getSize(s)); - ret = nm->mkNode(BITVECTOR_PLUS, s, bv_one).eqNode(t); + ret = nm->mkNode(BITVECTOR_ADD, s, bv_one).eqNode(t); } } Trace("cegqi-bv") << "Process " << lit << " as " << ret << std::endl; @@ -573,7 +573,7 @@ Node BvInstantiator::rewriteTermForSolvePv( return result; } } - else if (n.getKind() == BITVECTOR_MULT || n.getKind() == BITVECTOR_PLUS) + else if (n.getKind() == BITVECTOR_MULT || n.getKind() == BITVECTOR_ADD) { if (options::cegqiBvLinearize() && contains_pv[n]) { diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp index 5040125ba..9825130e5 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp @@ -166,8 +166,8 @@ Node normalizePvPlus(Node pv, std::unordered_map<Node, bool>& contains_pv) { NodeManager* nm; - NodeBuilder nb_c(BITVECTOR_PLUS); - NodeBuilder nb_l(BITVECTOR_PLUS); + NodeBuilder nb_c(BITVECTOR_ADD); + NodeBuilder nb_l(BITVECTOR_ADD); BvLinearAttribute is_linear; bool neg; @@ -199,7 +199,7 @@ Node normalizePvPlus(Node pv, nb_c << coeff; continue; } - else if (nc.getKind() == BITVECTOR_PLUS && nc.getAttribute(is_linear)) + else if (nc.getKind() == BITVECTOR_ADD && nc.getAttribute(is_linear)) { Assert(isLinearPlus(nc, pv, contains_pv)); Node coeff = utils::getPvCoeff(pv, nc[0]); @@ -240,7 +240,7 @@ Node normalizePvPlus(Node pv, } else { - result = nm->mkNode(BITVECTOR_PLUS, pv_mult_coeffs, leafs); + result = nm->mkNode(BITVECTOR_ADD, pv_mult_coeffs, leafs); contains_pv[result] = true; result.setAttribute(is_linear, true); } @@ -272,7 +272,7 @@ Node normalizePvEqual(Node pv, } if (child.getAttribute(is_linear) || child == pv) { - if (child.getKind() == BITVECTOR_PLUS) + if (child.getKind() == BITVECTOR_ADD) { Assert(isLinearPlus(child, pv, contains_pv)); coeffs[i] = utils::getPvCoeff(pv, child[0]); diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h index 6be22805d..4c7c096b4 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h @@ -66,7 +66,7 @@ Node normalizePvMult(TNode pv, std::unordered_map<Node, bool>& contains_pv); /** - * Normalizes the children of a BITVECTOR_PLUS w.r.t. pv. contains_pv marks + * Normalizes the children of a BITVECTOR_ADD w.r.t. pv. contains_pv marks * terms in which pv occurs. * For example, * diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index 29194ff36..047318e86 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -131,9 +131,9 @@ class ExtendedRewriter * be treated as immutable. This is for instance to prevent propagation * beneath illegal terms. As an example: * (bvand A (bvor A B)) is equivalent to (bvand A (bvor 1...1 B)), but - * (bvand A (bvplus A B)) is not equivalent to (bvand A (bvplus 1..1 B)), + * (bvand A (bvadd A B)) is not equivalent to (bvand A (bvadd 1..1 B)), * hence, when using this function to do BCP for bit-vectors, we have that - * BITVECTOR_AND is a bcp_kind, but BITVECTOR_PLUS is not. + * BITVECTOR_AND is a bcp_kind, but BITVECTOR_ADD is not. * * If this function returns a non-null node ret, then n ---> ret. */ diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 263b36abf..7ee22dc5b 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -811,7 +811,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::vector<Kind> bin_kinds = {BITVECTOR_AND, BITVECTOR_OR, BITVECTOR_XOR, - BITVECTOR_PLUS, + BITVECTOR_ADD, BITVECTOR_SUB, BITVECTOR_MULT, BITVECTOR_UDIV, diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index b771db986..0c9cb91d7 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -287,7 +287,7 @@ bool TermUtil::isAssoc(Kind k, bool reqNAry) } } return k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR - || k == XOR || k == BITVECTOR_PLUS || k == BITVECTOR_MULT + || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR || k == BITVECTOR_XNOR || k == BITVECTOR_CONCAT || k == STRING_CONCAT || k == UNION || k == INTERSECTION || k == JOIN || k == PRODUCT @@ -304,7 +304,7 @@ bool TermUtil::isComm(Kind k, bool reqNAry) } } return k == EQUAL || k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND - || k == OR || k == XOR || k == BITVECTOR_PLUS || k == BITVECTOR_MULT + || k == OR || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR || k == BITVECTOR_XNOR || k == UNION || k == INTERSECTION || k == SEP_STAR; @@ -389,7 +389,7 @@ Node TermUtil::mkTypeValueOffset(TypeNode tn, else if (tn.isBitVector()) { val_o = Rewriter::rewrite( - NodeManager::currentNM()->mkNode(BITVECTOR_PLUS, val, offset_val)); + NodeManager::currentNM()->mkNode(BITVECTOR_ADD, val, offset_val)); } } return val_o; @@ -443,10 +443,8 @@ bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg) TypeNode tn = n.getType(); if (n == mkTypeValue(tn, 0)) { - if (ik == PLUS || ik == OR || ik == XOR || ik == BITVECTOR_PLUS - || ik == BITVECTOR_OR - || ik == BITVECTOR_XOR - || ik == STRING_CONCAT) + if (ik == PLUS || ik == OR || ik == XOR || ik == BITVECTOR_ADD + || ik == BITVECTOR_OR || ik == BITVECTOR_XOR || ik == STRING_CONCAT) { return true; } diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp index 839b516e4..a8c1fae25 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.cpp +++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp @@ -895,9 +895,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique1) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_one), + kind::BITVECTOR_ADD, d_x_mul_one, d_y_mul_one), d_z_mul_one), d_p), d_five); @@ -907,9 +907,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique1) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three), + kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_three), d_z_mul_five), d_p), d_eight); @@ -919,7 +919,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique1) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_four, d_z_mul_five), + kind::BITVECTOR_ADD, d_x_mul_four, d_z_mul_five), d_p), d_two); @@ -949,7 +949,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2) Node p = d_nodeManager->mkNode( zextop6, bv::utils::mkConcat(bv::utils::mkZero(6), - d_nodeManager->mkNode(kind::BITVECTOR_PLUS, + d_nodeManager->mkNode(kind::BITVECTOR_ADD, bv::utils::mkConst(20, 7), bv::utils::mkConst(20, 4)))); @@ -980,7 +980,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2) bv::utils::mkExtract( d_nodeManager->mkNode( zextop6, - d_nodeManager->mkNode(kind::BITVECTOR_PLUS, d_three, d_two)), + d_nodeManager->mkNode(kind::BITVECTOR_ADD, d_three, d_two)), 31, 0), d_z); @@ -990,7 +990,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2) d_nodeManager->mkNode( kind::BITVECTOR_UDIV, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nodeManager->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(32, 4), bv::utils::mkConst(32, 5)), @@ -1003,8 +1003,8 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, - d_nodeManager->mkNode(kind::BITVECTOR_PLUS, x_mul_one, y_mul_one), + kind::BITVECTOR_ADD, + d_nodeManager->mkNode(kind::BITVECTOR_ADD, x_mul_one, y_mul_one), z_mul_one), p), d_five); @@ -1014,9 +1014,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, x_mul_two, y_mul_three), + kind::BITVECTOR_ADD, x_mul_two, y_mul_three), z_mul_five), p), d_eight); @@ -1025,7 +1025,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2) kind::EQUAL, d_nodeManager->mkNode( kind::BITVECTOR_UREM, - d_nodeManager->mkNode(kind::BITVECTOR_PLUS, x_mul_four, z_mul_five), + d_nodeManager->mkNode(kind::BITVECTOR_ADD, x_mul_four, z_mul_five), d_p), d_two); @@ -1055,8 +1055,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1a) kind::EQUAL, d_nodeManager->mkNode( kind::BITVECTOR_UREM, - d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_one, d_z_mul_nine), + d_nodeManager->mkNode(kind::BITVECTOR_ADD, d_x_mul_one, d_z_mul_nine), d_p), d_seven); @@ -1065,7 +1064,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1a) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_y_mul_one, d_z_mul_three), + kind::BITVECTOR_ADD, d_y_mul_one, d_z_mul_three), d_p), d_nine); @@ -1077,14 +1076,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1a) Node x1 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_seven32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)), d_p); Node y1 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nine32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)), d_p); @@ -1092,14 +1091,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1a) Node x2 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_two32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)), d_p); Node z2 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_three32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)), d_p); @@ -1107,14 +1106,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1a) Node y3 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_three32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)), d_p); Node z3 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_two32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)), d_p); @@ -1181,7 +1180,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1b) kind::EQUAL, d_nodeManager->mkNode( kind::BITVECTOR_UREM, - d_nodeManager->mkNode(kind::BITVECTOR_PLUS, d_x, d_z_mul_nine), + d_nodeManager->mkNode(kind::BITVECTOR_ADD, d_x, d_z_mul_nine), d_p), d_seven); @@ -1189,7 +1188,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1b) kind::EQUAL, d_nodeManager->mkNode( kind::BITVECTOR_UREM, - d_nodeManager->mkNode(kind::BITVECTOR_PLUS, d_y, d_z_mul_three), + d_nodeManager->mkNode(kind::BITVECTOR_ADD, d_y, d_z_mul_three), d_p), d_nine); @@ -1201,14 +1200,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1b) Node x1 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_seven32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)), d_p); Node y1 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nine32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)), d_p); @@ -1216,14 +1215,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1b) Node x2 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_two32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)), d_p); Node z2 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_three32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)), d_p); @@ -1231,14 +1230,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1b) Node y3 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_three32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)), d_p); Node z3 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_two32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)), d_p); @@ -1306,7 +1305,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial2) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_three), + kind::BITVECTOR_ADD, d_x_mul_one, d_y_mul_three), d_p), d_seven); @@ -1323,14 +1322,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial2) Node x1 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_seven32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_eight32)), d_p); Node y2 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_six32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_seven32)), d_p); @@ -1395,8 +1394,8 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial3) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, - d_nodeManager->mkNode(kind::BITVECTOR_PLUS, d_x_mul_one, d_y), + kind::BITVECTOR_ADD, + d_nodeManager->mkNode(kind::BITVECTOR_ADD, d_x_mul_one, d_y), d_z_mul_one), d_p), d_five); @@ -1406,9 +1405,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial3) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three), + kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_three), d_z_mul_five), d_p), d_eight); @@ -1421,42 +1420,42 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial3) Node x1 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_seven32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)), d_p); Node y1 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nine32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)), d_p); Node x2 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_two32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)), d_p); Node z2 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_three32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)), d_p); Node y3 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_three32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)), d_p); Node z3 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_two32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)), d_p); @@ -1525,9 +1524,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial4) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_four), + kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_four), d_z_mul_six), d_p), d_eighteen); @@ -1537,9 +1536,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial4) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_four, d_y_mul_five), + kind::BITVECTOR_ADD, d_x_mul_four, d_y_mul_five), d_z_mul_six), d_p), d_twentyfour); @@ -1549,9 +1548,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial4) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_seven), + kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_seven), d_z_mul_twelve), d_p), d_thirty); @@ -1564,42 +1563,42 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial4) Node x1 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_one32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_one32)), d_p); Node y1 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_four32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_nine32)), d_p); Node x2 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_three32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_five32)), d_p); Node z2 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_two32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_five32)), d_p); Node y3 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_six32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_nine32)), d_p); Node z3 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_ten32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_one32)), d_p); @@ -1676,9 +1675,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial5) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_four), + kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_four), d_z_mul_six), d_three), d_eighteen); @@ -1688,9 +1687,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial5) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_four, d_y_mul_five), + kind::BITVECTOR_ADD, d_x_mul_four, d_y_mul_five), d_z_mul_six), d_three), d_twentyfour); @@ -1700,9 +1699,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial5) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_seven), + kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_seven), d_z_mul_twelve), d_three), d_thirty); @@ -1796,9 +1795,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial6) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_one, y_mul_two), + kind::BITVECTOR_ADD, d_x_mul_one, y_mul_two), w_mul_six), d_p), d_two); @@ -1807,7 +1806,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial6) kind::EQUAL, d_nodeManager->mkNode( kind::BITVECTOR_UREM, - d_nodeManager->mkNode(kind::BITVECTOR_PLUS, z_mul_two, w_mul_two), + d_nodeManager->mkNode(kind::BITVECTOR_ADD, z_mul_two, w_mul_two), d_p), d_two); @@ -1822,7 +1821,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial6) Node x1 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_one32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_nine32)), d_p); @@ -1832,7 +1831,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial6) Node y2 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_six32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_five32)), d_p); @@ -1897,7 +1896,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial) kind::EQUAL, d_nodeManager->mkNode( kind::BITVECTOR_UREM, - d_nodeManager->mkNode(kind::BITVECTOR_PLUS, x_mul_one, nine_mul_z), + d_nodeManager->mkNode(kind::BITVECTOR_ADD, x_mul_one, nine_mul_z), d_p), d_seven); @@ -1905,7 +1904,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial) kind::EQUAL, d_nodeManager->mkNode( kind::BITVECTOR_UREM, - d_nodeManager->mkNode(kind::BITVECTOR_PLUS, one_mul_y, z_mul_three), + d_nodeManager->mkNode(kind::BITVECTOR_ADD, one_mul_y, z_mul_three), d_p), d_nine); @@ -1921,14 +1920,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial) Node x1 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_seven32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, z, d_two32)), d_p); Node y1 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nine32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, z, d_eight32)), d_p); @@ -1936,14 +1935,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial) Node x2 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_two32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, y, d_three32)), d_p); Node z2 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_three32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, y, d_seven32)), d_p); @@ -1951,14 +1950,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial) Node y3 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_three32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, x, d_four32)), d_p); Node z3 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_two32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, x, d_six32)), d_p); @@ -2067,7 +2066,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, x_mul_one_mul_xx, z_mul_nine_mul_zz), + kind::BITVECTOR_ADD, x_mul_one_mul_xx, z_mul_nine_mul_zz), d_p), d_seven); @@ -2076,7 +2075,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, y_mul_yy_mul_one, three_mul_z_mul_zz), + kind::BITVECTOR_ADD, y_mul_yy_mul_one, three_mul_z_mul_zz), d_p), d_nine); @@ -2092,14 +2091,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial) Node x1 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_seven32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, z_mul_zz, d_two32)), d_p); Node y1 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nine32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, z_mul_zz, d_eight32)), d_p); @@ -2107,14 +2106,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial) Node x2 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_two32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, y_mul_yy, d_three32)), d_p); Node z2 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_three32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, y_mul_yy, d_seven32)), d_p); @@ -2122,14 +2121,14 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial) Node y3 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_three32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, x_mul_xx, d_four32)), d_p); Node z3 = d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_two32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, x_mul_xx, d_six32)), d_p); @@ -2254,7 +2253,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid2) d_nodeManager->mkNode(kind::BITVECTOR_MULT, x, y), z); Node n3 = d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_nodeManager->mkNode(kind::BITVECTOR_MULT, x, y), bv::utils::mkConcat(d_zero, d_two)), @@ -2367,9 +2366,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique1) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_one), + kind::BITVECTOR_ADD, d_x_mul_one, d_y_mul_one), d_z_mul_one), d_p), d_five); @@ -2379,9 +2378,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique1) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three), + kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_three), d_z_mul_five), d_p), d_eight); @@ -2391,7 +2390,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique1) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_four, d_z_mul_five), + kind::BITVECTOR_ADD, d_x_mul_four, d_z_mul_five), d_p), d_two); @@ -2436,9 +2435,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique2) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_one), + kind::BITVECTOR_ADD, d_x_mul_one, d_y_mul_one), d_z_mul_one), d_p), d_five); @@ -2448,9 +2447,9 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique2) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three), + kind::BITVECTOR_ADD, d_x_mul_two, d_y_mul_three), d_z_mul_five), d_p), d_eight); @@ -2460,7 +2459,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique2) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_four, d_z_mul_five), + kind::BITVECTOR_ADD, d_x_mul_four, d_z_mul_five), d_p), d_two); @@ -2470,7 +2469,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique2) kind::EQUAL, d_nodeManager->mkNode( kind::BITVECTOR_UREM, - d_nodeManager->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, y_mul_six), + d_nodeManager->mkNode(kind::BITVECTOR_ADD, d_x_mul_two, y_mul_six), d_seven), d_four); @@ -2478,7 +2477,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique2) kind::EQUAL, d_nodeManager->mkNode( kind::BITVECTOR_UREM, - d_nodeManager->mkNode(kind::BITVECTOR_PLUS, d_x_mul_four, y_mul_six), + d_nodeManager->mkNode(kind::BITVECTOR_ADD, d_x_mul_four, y_mul_six), d_seven), d_three); @@ -2524,8 +2523,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial) kind::EQUAL, d_nodeManager->mkNode( kind::BITVECTOR_UREM, - d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_x_mul_one, d_z_mul_nine), + d_nodeManager->mkNode(kind::BITVECTOR_ADD, d_x_mul_one, d_z_mul_nine), d_p), d_seven); @@ -2534,7 +2532,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, d_y_mul_one, d_z_mul_three), + kind::BITVECTOR_ADD, d_y_mul_one, d_z_mul_three), d_p), d_nine); @@ -2553,7 +2551,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_seven32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)), d_p)); @@ -2563,7 +2561,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nine32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)), d_p)); @@ -2574,7 +2572,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_two32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)), d_p)); @@ -2584,7 +2582,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_three32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)), d_p)); @@ -2595,7 +2593,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_three32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)), d_p)); @@ -2605,7 +2603,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial) d_nodeManager->mkNode( kind::BITVECTOR_UREM, d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_two32, d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)), d_p)); @@ -2723,44 +2721,44 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw1) Node urem3x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x8, zext48x); ASSERT_EQ(BVGauss::getMinBwExpr(urem3x), 8); - Node add1p = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, extp, extp); + Node add1p = d_nodeManager->mkNode(kind::BITVECTOR_ADD, extp, extp); ASSERT_EQ(BVGauss::getMinBwExpr(add1p), 5); - Node add1x = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, extx, extx); + Node add1x = d_nodeManager->mkNode(kind::BITVECTOR_ADD, extx, extx); ASSERT_EQ(BVGauss::getMinBwExpr(add1x), 0); - Node add2p = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext40p, zext40p); + Node add2p = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext40p, zext40p); ASSERT_EQ(BVGauss::getMinBwExpr(add2p), 5); - Node add2x = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext40x, zext40x); + Node add2x = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext40x, zext40x); ASSERT_EQ(BVGauss::getMinBwExpr(add2x), 17); - Node add3p = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext48p8, zext48p); + Node add3p = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext48p8, zext48p); ASSERT_EQ(BVGauss::getMinBwExpr(add3p), 5); - Node add3x = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext48x8, zext48x); + Node add3x = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext48x8, zext48x); ASSERT_EQ(BVGauss::getMinBwExpr(add3x), 17); - NodeBuilder nbadd4p(kind::BITVECTOR_PLUS); + NodeBuilder nbadd4p(kind::BITVECTOR_ADD); nbadd4p << zext48p << zext48p << zext48p; Node add4p = nbadd4p; ASSERT_EQ(BVGauss::getMinBwExpr(add4p), 6); - NodeBuilder nbadd4x(kind::BITVECTOR_PLUS); + NodeBuilder nbadd4x(kind::BITVECTOR_ADD); nbadd4x << zext48x << zext48x << zext48x; Node add4x = nbadd4x; ASSERT_EQ(BVGauss::getMinBwExpr(add4x), 18); - NodeBuilder nbadd5p(kind::BITVECTOR_PLUS); + NodeBuilder nbadd5p(kind::BITVECTOR_ADD); nbadd5p << zext48p << zext48p8 << zext48p; Node add5p = nbadd5p; ASSERT_EQ(BVGauss::getMinBwExpr(add5p), 6); - NodeBuilder nbadd5x(kind::BITVECTOR_PLUS); + NodeBuilder nbadd5x(kind::BITVECTOR_ADD); nbadd5x << zext48x << zext48x8 << zext48x; Node add5x = nbadd5x; ASSERT_EQ(BVGauss::getMinBwExpr(add5x), 18); - NodeBuilder nbadd6p(kind::BITVECTOR_PLUS); + NodeBuilder nbadd6p(kind::BITVECTOR_ADD); nbadd6p << zext48p << zext48p << zext48p << zext48p; Node add6p = nbadd6p; ASSERT_EQ(BVGauss::getMinBwExpr(add6p), 6); - NodeBuilder nbadd6x(kind::BITVECTOR_PLUS); + NodeBuilder nbadd6x(kind::BITVECTOR_ADD); nbadd6x << zext48x << zext48x << zext48x << zext48x; Node add6x = nbadd6x; ASSERT_EQ(BVGauss::getMinBwExpr(add6x), 18); @@ -2850,7 +2848,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw4a) Node udiv2_2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1_2, ext2_2); Node zext2_2 = d_nodeManager->mkNode(zextop7, udiv2_2); - Node plus = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext2_1, zext2_2); + Node plus = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext2_1, zext2_2); ASSERT_EQ(BVGauss::getMinBwExpr(plus), 6); } @@ -2882,7 +2880,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw4b) Node udiv2_2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1_2, ext2_2); Node zext2_2 = d_nodeManager->mkNode(zextop7, udiv2_2); - Node plus = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext2_1, zext2_2); + Node plus = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext2_1, zext2_2); ASSERT_EQ(BVGauss::getMinBwExpr(plus), 6); } @@ -2954,38 +2952,38 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw5a) Node s15 = bv::utils::mkConcat(bv::utils::mkZero(5), ext15s); Node plus1 = d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nodeManager->mkNode( kind::BITVECTOR_MULT, bv::utils::mkConst(13, 86), xx), d_nodeManager->mkNode( kind::BITVECTOR_MULT, bv::utils::mkConst(13, 41), yy)); Node plus2 = d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, plus1, d_nodeManager->mkNode( kind::BITVECTOR_MULT, bv::utils::mkConst(13, 37), zz)); Node plus3 = d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, plus2, d_nodeManager->mkNode( kind::BITVECTOR_MULT, bv::utils::mkConst(13, 170), uu)); Node plus4 = d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, plus3, d_nodeManager->mkNode( kind::BITVECTOR_MULT, bv::utils::mkConst(13, 112), uu)); Node plus5 = d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, plus4, d_nodeManager->mkNode( kind::BITVECTOR_MULT, bv::utils::mkConst(13, 195), s15)); Node plus6 = d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, plus5, d_nodeManager->mkNode( kind::BITVECTOR_MULT, bv::utils::mkConst(13, 124), s7)); Node plus7 = d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, plus6, d_nodeManager->mkNode( kind::BITVECTOR_MULT, bv::utils::mkConst(13, 83), ww)); @@ -3058,38 +3056,38 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw5b) Node s15 = bv::utils::mkConcat(bv::utils::mkZero(12), ext15s); Node plus1 = d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, d_nodeManager->mkNode( kind::BITVECTOR_MULT, bv::utils::mkConst(20, 86), xx), d_nodeManager->mkNode( kind::BITVECTOR_MULT, bv::utils::mkConst(20, 41), yy)); Node plus2 = d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, plus1, d_nodeManager->mkNode( kind::BITVECTOR_MULT, bv::utils::mkConst(20, 37), zz)); Node plus3 = d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, plus2, d_nodeManager->mkNode( kind::BITVECTOR_MULT, bv::utils::mkConst(20, 170), uu)); Node plus4 = d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, plus3, d_nodeManager->mkNode( kind::BITVECTOR_MULT, bv::utils::mkConst(20, 112), uu)); Node plus5 = d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, plus4, d_nodeManager->mkNode( kind::BITVECTOR_MULT, bv::utils::mkConst(20, 195), s15)); Node plus6 = d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, plus5, d_nodeManager->mkNode( kind::BITVECTOR_MULT, bv::utils::mkConst(20, 124), s7)); Node plus7 = d_nodeManager->mkNode( - kind::BITVECTOR_PLUS, + kind::BITVECTOR_ADD, plus6, d_nodeManager->mkNode( kind::BITVECTOR_MULT, bv::utils::mkConst(20, 83), ww)); diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp index bfdcfb604..094a32772 100644 --- a/test/unit/theory/theory_bv_white.cpp +++ b/test/unit/theory/theory_bv_white.cpp @@ -58,7 +58,7 @@ TEST_F(TestTheoryWhiteBv, bitblaster_core) Node x = d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(16)); Node y = d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(16)); - Node x_plus_y = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, x, y); + Node x_plus_y = d_nodeManager->mkNode(kind::BITVECTOR_ADD, x, y); Node one = d_nodeManager->mkConst<BitVector>(BitVector(16, 1u)); Node x_shl_one = d_nodeManager->mkNode(kind::BITVECTOR_SHL, x, one); Node eq = d_nodeManager->mkNode(kind::EQUAL, x_plus_y, x_shl_one); diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp index 85f14b245..6c336afd4 100644 --- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp @@ -50,12 +50,12 @@ class TestTheoryWhiteyQuantifiersBvInstantiator : public TestSmt Node mkPlus(TNode a, TNode b) { - return d_nodeManager->mkNode(kind::BITVECTOR_PLUS, a, b); + return d_nodeManager->mkNode(kind::BITVECTOR_ADD, a, b); } Node mkPlus(const std::vector<Node>& children) { - return d_nodeManager->mkNode(kind::BITVECTOR_PLUS, children); + return d_nodeManager->mkNode(kind::BITVECTOR_ADD, children); } }; @@ -230,7 +230,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus) Node norm_xa = normalizePvPlus(x, {x, a}, contains_x); ASSERT_TRUE(contains_x[norm_xa]); ASSERT_TRUE(norm_xa.getAttribute(is_linear)); - ASSERT_EQ(norm_xa.getKind(), kind::BITVECTOR_PLUS); + ASSERT_EQ(norm_xa.getKind(), kind::BITVECTOR_ADD); ASSERT_EQ(norm_xa.getNumChildren(), 2); ASSERT_EQ(norm_xa[0], x); ASSERT_EQ(norm_xa[1], a); @@ -239,7 +239,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus) Node norm_ax = normalizePvPlus(x, {a, x}, contains_x); ASSERT_TRUE(contains_x[norm_ax]); ASSERT_TRUE(norm_ax.getAttribute(is_linear)); - ASSERT_EQ(norm_ax.getKind(), kind::BITVECTOR_PLUS); + ASSERT_EQ(norm_ax.getKind(), kind::BITVECTOR_ADD); ASSERT_EQ(norm_ax.getNumChildren(), 2); ASSERT_EQ(norm_ax[0], x); ASSERT_EQ(norm_ax[1], a); @@ -248,7 +248,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus) Node norm_neg_ax = normalizePvPlus(x, {a, neg_x}, contains_x); ASSERT_TRUE(contains_x[norm_neg_ax]); ASSERT_TRUE(norm_neg_ax.getAttribute(is_linear)); - ASSERT_EQ(norm_neg_ax.getKind(), kind::BITVECTOR_PLUS); + ASSERT_EQ(norm_neg_ax.getKind(), kind::BITVECTOR_ADD); ASSERT_EQ(norm_neg_ax.getNumChildren(), 2); ASSERT_EQ(norm_neg_ax[0].getKind(), kind::BITVECTOR_MULT); ASSERT_EQ(norm_neg_ax[0].getNumChildren(), 2); @@ -272,7 +272,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus) Node norm_abcxd = normalizePvPlus(x, {a, b, c, x, d}, contains_x); ASSERT_TRUE(contains_x[norm_abcxd]); ASSERT_TRUE(norm_abcxd.getAttribute(is_linear)); - ASSERT_EQ(norm_abcxd.getKind(), kind::BITVECTOR_PLUS); + ASSERT_EQ(norm_abcxd.getKind(), kind::BITVECTOR_ADD); ASSERT_EQ(norm_abcxd.getNumChildren(), 2); ASSERT_EQ(norm_abcxd[0], x); ASSERT_EQ(norm_abcxd[1], Rewriter::rewrite(mkPlus({a, b, c, d}))); @@ -281,7 +281,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus) Node norm_neg_abcxd = normalizePvPlus(x, {a, b, c, neg_x, d}, contains_x); ASSERT_TRUE(contains_x[norm_neg_abcxd]); ASSERT_TRUE(norm_neg_abcxd.getAttribute(is_linear)); - ASSERT_EQ(norm_neg_abcxd.getKind(), kind::BITVECTOR_PLUS); + ASSERT_EQ(norm_neg_abcxd.getKind(), kind::BITVECTOR_ADD); ASSERT_EQ(norm_neg_abcxd.getNumChildren(), 2); ASSERT_EQ(norm_neg_abcxd[0].getKind(), kind::BITVECTOR_MULT); ASSERT_EQ(norm_neg_abcxd[0].getNumChildren(), 2); @@ -295,7 +295,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus) Node norm_bxa = normalizePvPlus(x, {b, norm_ax}, contains_x); ASSERT_TRUE(contains_x[norm_bxa]); ASSERT_TRUE(norm_bxa.getAttribute(is_linear)); - ASSERT_EQ(norm_bxa.getKind(), kind::BITVECTOR_PLUS); + ASSERT_EQ(norm_bxa.getKind(), kind::BITVECTOR_ADD); ASSERT_EQ(norm_bxa.getNumChildren(), 2); ASSERT_EQ(norm_bxa[0], x); ASSERT_EQ(norm_bxa[1], Rewriter::rewrite(mkPlus(b, a))); @@ -306,7 +306,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus) Node norm_neg_bxa = normalizePvPlus(x, {b, neg_norm_ax}, contains_x); ASSERT_TRUE(contains_x[norm_neg_bxa]); ASSERT_TRUE(norm_neg_bxa.getAttribute(is_linear)); - ASSERT_EQ(norm_neg_bxa.getKind(), kind::BITVECTOR_PLUS); + ASSERT_EQ(norm_neg_bxa.getKind(), kind::BITVECTOR_ADD); ASSERT_EQ(norm_neg_bxa.getNumChildren(), 2); ASSERT_EQ(norm_neg_abcxd[0].getKind(), kind::BITVECTOR_MULT); ASSERT_EQ(norm_neg_abcxd[0].getNumChildren(), 2); diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp index 83d982d8e..e5ba92995 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp @@ -696,97 +696,97 @@ TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_neg_sgt_false1) TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ult_true0) { - Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s); + Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_x, d_s); runTestPred(true, BITVECTOR_ULT, x, getICBvUltUgt); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ult_true1) { - Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x); + Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_s, d_x); runTestPred(true, BITVECTOR_ULT, x, getICBvUltUgt); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ult_false0) { - Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s); + Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_x, d_s); runTestPred(false, BITVECTOR_ULT, x, getICBvUltUgt); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ult_false1) { - Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x); + Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_s, d_x); runTestPred(false, BITVECTOR_ULT, x, getICBvUltUgt); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ugt_true0) { - Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s); + Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_x, d_s); runTestPred(true, BITVECTOR_UGT, x, getICBvUltUgt); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ugt_true1) { - Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x); + Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_s, d_x); runTestPred(true, BITVECTOR_UGT, x, getICBvUltUgt); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ugt_false0) { - Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s); + Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_x, d_s); runTestPred(false, BITVECTOR_UGT, x, getICBvUltUgt); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_ugt_false1) { - Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x); + Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_s, d_x); runTestPred(false, BITVECTOR_UGT, x, getICBvUltUgt); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_slt_true0) { - Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s); + Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_x, d_s); runTestPred(true, BITVECTOR_SLT, x, getICBvSltSgt); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_slt_true1) { - Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x); + Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_s, d_x); runTestPred(true, BITVECTOR_SLT, x, getICBvSltSgt); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_slt_false0) { - Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s); + Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_x, d_s); runTestPred(false, BITVECTOR_SLT, x, getICBvSltSgt); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_slt_false1) { - Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x); + Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_s, d_x); runTestPred(false, BITVECTOR_SLT, x, getICBvSltSgt); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_sgt_true0) { - Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s); + Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_x, d_s); runTestPred(true, BITVECTOR_SGT, x, getICBvSltSgt); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_sgt_true1) { - Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x); + Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_s, d_x); runTestPred(true, BITVECTOR_SGT, x, getICBvSltSgt); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_sgt_false0) { - Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_x, d_s); + Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_x, d_s); runTestPred(false, BITVECTOR_SGT, x, getICBvSltSgt); } TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_plus_sgt_false1) { - Node x = d_nodeManager->mkNode(BITVECTOR_PLUS, d_s, d_x); + Node x = d_nodeManager->mkNode(BITVECTOR_ADD, d_s, d_x); runTestPred(false, BITVECTOR_SGT, x, getICBvSltSgt); } |