From eab7bf6702c174c2c58373035cf9b8a099a209ae Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 2 Feb 2022 14:27:14 -0800 Subject: [PATCH] Rename kinds MINUS -> SUB and UMINUS -> NEG. (#8035) This renames the internal arithmetic kinds MINUS and UMINUS for consistency with our naming scheme for other operators (e.g., BITVECTOR_SUB, FLOATINGPOINT_SUB). --- src/api/cpp/cvc5.cpp | 8 +-- src/preprocessing/passes/int_to_bv.cpp | 6 +- src/preprocessing/passes/nl_ext_purify.cpp | 3 +- .../passes/unconstrained_simplifier.cpp | 4 +- src/printer/smt2/smt2_printer.cpp | 4 +- src/proof/alethe/alethe_post_processor.cpp | 4 +- src/proof/lfsc/lfsc_node_converter.cpp | 15 ++-- src/theory/arith/arith_poly_norm.cpp | 8 +-- src/theory/arith/arith_poly_norm.h | 2 +- src/theory/arith/arith_rewriter.cpp | 31 ++++---- src/theory/arith/arith_rewriter.h | 4 +- src/theory/arith/kinds | 8 +-- src/theory/arith/nl/ext/monomial_check.cpp | 6 +- src/theory/arith/nl/ext/proof_checker.cpp | 2 +- .../arith/nl/ext/tangent_plane_check.cpp | 2 +- src/theory/arith/nl/iand_solver.cpp | 2 +- src/theory/arith/nl/iand_utils.cpp | 2 +- src/theory/arith/nl/nl_model.cpp | 2 +- .../nl/transcendental/exponential_solver.cpp | 2 +- .../arith/nl/transcendental/proof_checker.cpp | 10 +-- .../arith/nl/transcendental/sine_solver.cpp | 7 +- .../nl/transcendental/taylor_generator.cpp | 2 +- .../transcendental/transcendental_state.cpp | 8 +-- src/theory/arith/operator_elim.cpp | 6 +- src/theory/arith/theory_arith.cpp | 2 +- src/theory/arith/theory_arith_private.cpp | 9 +-- src/theory/bags/bag_reduction.cpp | 4 +- src/theory/bags/inference_generator.cpp | 4 +- src/theory/bv/int_blaster.cpp | 10 +-- src/theory/datatypes/sygus_extension.cpp | 4 +- src/theory/datatypes/sygus_simple_sym.cpp | 16 ++--- src/theory/evaluator.cpp | 4 +- .../cegqi/ceg_arith_instantiator.cpp | 18 ++--- .../quantifiers/cegqi/ceg_instantiator.cpp | 2 +- .../ematching/inst_match_generator.cpp | 4 +- .../ematching/pattern_term_selector.cpp | 4 +- .../quantifiers/fmf/bounded_integers.cpp | 4 +- .../quantifiers/quant_conflict_find.cpp | 2 +- .../quantifiers/quantifiers_rewriter.cpp | 2 +- src/theory/quantifiers/skolemize.cpp | 2 +- .../quantifiers/sygus/sygus_grammar_cons.cpp | 4 +- src/theory/quantifiers/sygus_sampler.cpp | 2 +- src/theory/quantifiers/term_util.cpp | 4 +- src/theory/sets/theory_sets_rewriter.cpp | 4 +- src/theory/strings/arith_entail.cpp | 24 +++---- src/theory/strings/array_core_solver.cpp | 2 +- src/theory/strings/array_solver.cpp | 2 +- src/theory/strings/core_solver.cpp | 2 +- src/theory/strings/regexp_elim.cpp | 14 ++-- src/theory/strings/regexp_operation.cpp | 8 +-- src/theory/strings/sequences_rewriter.cpp | 18 +++-- src/theory/strings/skolem_cache.cpp | 8 +-- src/theory/strings/strings_entail.cpp | 8 +-- .../strings/theory_strings_preprocess.cpp | 71 +++++++++---------- src/theory/strings/theory_strings_utils.cpp | 2 +- test/unit/node/node_black.cpp | 6 +- test/unit/node/node_builder_black.cpp | 2 +- test/unit/theory/arith_poly_white.cpp | 10 +-- test/unit/theory/sequences_rewriter_white.cpp | 2 +- .../theory/theory_arith_rewriter_black.cpp | 6 +- 60 files changed, 213 insertions(+), 225 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 2105ecca0..4371bac8d 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -134,8 +134,8 @@ const static std::unordered_map s_kinds{ {MULT, cvc5::Kind::MULT}, {IAND, cvc5::Kind::IAND}, {POW2, cvc5::Kind::POW2}, - {MINUS, cvc5::Kind::MINUS}, - {UMINUS, cvc5::Kind::UMINUS}, + {MINUS, cvc5::Kind::SUB}, + {UMINUS, cvc5::Kind::NEG}, {DIVISION, cvc5::Kind::DIVISION}, {INTS_DIVISION, cvc5::Kind::INTS_DIVISION}, {INTS_MODULUS, cvc5::Kind::INTS_MODULUS}, @@ -416,8 +416,8 @@ const static std::unordered_map {cvc5::Kind::MULT, MULT}, {cvc5::Kind::IAND, IAND}, {cvc5::Kind::POW2, POW2}, - {cvc5::Kind::MINUS, MINUS}, - {cvc5::Kind::UMINUS, UMINUS}, + {cvc5::Kind::SUB, MINUS}, + {cvc5::Kind::NEG, UMINUS}, {cvc5::Kind::DIVISION, DIVISION}, {cvc5::Kind::DIVISION_TOTAL, INTERNAL_KIND}, {cvc5::Kind::INTS_DIVISION, INTS_DIVISION}, diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index 3082377c7..4927247bb 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -160,12 +160,12 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache) newKind = kind::BITVECTOR_MULT; max = max * 2; break; - case kind::MINUS: + case kind::SUB: Assert(children.size() == 2); newKind = kind::BITVECTOR_SUB; max = max + 1; break; - case kind::UMINUS: + case kind::NEG: Assert(children.size() == 1); newKind = kind::BITVECTOR_NEG; max = max + 1; @@ -234,7 +234,7 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache) Node bv2int = nm->mkNode( kind::ITE, nm->mkNode(kind::BITVECTOR_SLT, result, nm->mkConst(bvzero)), - nm->mkNode(kind::UMINUS, negResult), + nm->mkNode(kind::NEG, negResult), nm->mkNode(kind::BITVECTOR_TO_NAT, result)); d_preprocContext->addSubstitution(current, bv2int); } diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp index 27f34f177..aa7805284 100644 --- a/src/preprocessing/passes/nl_ext_purify.cpp +++ b/src/preprocessing/passes/nl_ext_purify.cpp @@ -60,8 +60,7 @@ Node NlExtPurify::purifyNlTerms(TNode n, Node ret = n; if (n.getNumChildren() > 0) { - if (beneathMult - && (n.getKind() == kind::PLUS || n.getKind() == kind::MINUS)) + if (beneathMult && (n.getKind() == kind::PLUS || n.getKind() == kind::SUB)) { // don't do it if it rewrites to a constant Node nr = rewrite(n); diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 7a58fc231..31a888dd0 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -310,7 +310,7 @@ void UnconstrainedSimplifier::processUnconstrained() case kind::NOT: case kind::BITVECTOR_NOT: case kind::BITVECTOR_NEG: - case kind::UMINUS: + case kind::NEG: ++d_numUnconstrainedElim; Assert(parent[0] == current); if (currentSub.isNull()) @@ -448,7 +448,7 @@ void UnconstrainedSimplifier::processUnconstrained() // N-ary operators returning same type requiring at least one child to // be unconstrained case kind::PLUS: - case kind::MINUS: + case kind::SUB: if (current.getType().isInteger() && !parent.getType().isInteger()) { break; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index cf85e6b0e..173247b1c 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1009,8 +1009,8 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::ARCCOTANGENT: return "arccot"; case kind::PI: return "real.pi"; case kind::SQRT: return "sqrt"; - case kind::MINUS: return "-"; - case kind::UMINUS: return "-"; + case kind::SUB: return "-"; + case kind::NEG: return "-"; case kind::LT: return "<"; case kind::LEQ: return "<="; case kind::GT: return ">"; diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index af683ffc6..4d1a3b5a6 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -418,12 +418,12 @@ bool AletheProofPostprocessCallback::update(Node res, vrule = AletheRule::PROD_SIMPLIFY; break; } - case kind::MINUS: + case kind::SUB: { vrule = AletheRule::MINUS_SIMPLIFY; break; } - case kind::UMINUS: + case kind::NEG: { vrule = AletheRule::UNARY_MINUS_SIMPLIFY; break; diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index 56326a2fe..ffde0b274 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -292,14 +292,14 @@ Node LfscNodeConverter::postConvert(Node n) ArrayStoreAll storeAll = n.getConst(); return nm->mkNode(APPLY_UF, f, convert(storeAll.getValue())); } - else if (k == GEQ || k == GT || k == LEQ || k == LT || k == MINUS + else if (k == GEQ || k == GT || k == LEQ || k == LT || k == SUB || k == DIVISION || k == DIVISION_TOTAL || k == INTS_DIVISION || k == INTS_DIVISION_TOTAL || k == INTS_MODULUS - || k == INTS_MODULUS_TOTAL || k == UMINUS || k == POW + || k == INTS_MODULUS_TOTAL || k == NEG || k == POW || isIndexedOperatorKind(k)) { // must give special names to SMT-LIB operators with arithmetic subtyping - // note that MINUS is not n-ary + // note that SUB is not n-ary // get the macro-apply version of the operator Node opc = getOperatorOfTerm(n, true); std::vector children; @@ -983,15 +983,14 @@ Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply) } // all arithmetic kinds must explicitly deal with real vs int subtyping if (k == PLUS || k == MULT || k == NONLINEAR_MULT || k == GEQ || k == GT - || k == LEQ || k == LT || k == MINUS || k == DIVISION - || k == DIVISION_TOTAL || k == INTS_DIVISION || k == INTS_DIVISION_TOTAL - || k == INTS_MODULUS || k == INTS_MODULUS_TOTAL || k == UMINUS - || k == POW) + || k == LEQ || k == LT || k == SUB || k == DIVISION || k == DIVISION_TOTAL + || k == INTS_DIVISION || k == INTS_DIVISION_TOTAL || k == INTS_MODULUS + || k == INTS_MODULUS_TOTAL || k == NEG || k == POW) { // currently allow subtyping opName << "a."; } - if (k == UMINUS) + if (k == NEG) { opName << "u"; } diff --git a/src/theory/arith/arith_poly_norm.cpp b/src/theory/arith/arith_poly_norm.cpp index 151adc874..99a38dd58 100644 --- a/src/theory/arith/arith_poly_norm.cpp +++ b/src/theory/arith/arith_poly_norm.cpp @@ -201,7 +201,7 @@ PolyNorm PolyNorm::mkPolyNorm(TNode n) visited[cur].addMonomial(null, r); } } - else if (k == PLUS || k == MINUS || k == UMINUS || k == MULT + else if (k == PLUS || k == SUB || k == NEG || k == MULT || k == NONLINEAR_MULT) { visited[cur] = PolyNorm(); @@ -225,15 +225,15 @@ PolyNorm PolyNorm::mkPolyNorm(TNode n) switch (k) { case PLUS: - case MINUS: - case UMINUS: + case SUB: + case NEG: case MULT: case NONLINEAR_MULT: for (size_t i = 0, nchild = cur.getNumChildren(); i < nchild; i++) { it = visited.find(cur[i]); Assert(it != visited.end()); - if ((k == MINUS && i == 1) || k == UMINUS) + if ((k == SUB && i == 1) || k == NEG) { ret.subtract(it->second); } diff --git a/src/theory/arith/arith_poly_norm.h b/src/theory/arith/arith_poly_norm.h index fafa94ee3..c36da60be 100644 --- a/src/theory/arith/arith_poly_norm.h +++ b/src/theory/arith/arith_poly_norm.h @@ -58,7 +58,7 @@ class PolyNorm bool isEqual(const PolyNorm& p) const; /** * Make polynomial from real term n. This method normalizes applications - * of operators PLUS, MINUS, UMINUS, MULT, and NONLINEAR_MULT only. + * of operators PLUS, SUB, NEG, MULT, and NONLINEAR_MULT only. */ static PolyNorm mkPolyNorm(TNode n); /** Do a and b normalize to the same polynomial? */ diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index c57665948..49907450a 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -355,9 +355,9 @@ RewriteResponse ArithRewriter::rewriteVariable(TNode t){ return RewriteResponse(REWRITE_DONE, t); } -RewriteResponse ArithRewriter::rewriteMinus(TNode t) +RewriteResponse ArithRewriter::rewriteSub(TNode t) { - Assert(t.getKind() == kind::MINUS); + Assert(t.getKind() == kind::SUB); Assert(t.getNumChildren() == 2); auto* nm = NodeManager::currentNM(); @@ -372,8 +372,9 @@ RewriteResponse ArithRewriter::rewriteMinus(TNode t) nm->mkNode(Kind::PLUS, t[0], makeUnaryMinusNode(t[1]))); } -RewriteResponse ArithRewriter::rewriteUMinus(TNode t, bool pre){ - Assert(t.getKind() == kind::UMINUS); +RewriteResponse ArithRewriter::rewriteNeg(TNode t, bool pre) +{ + Assert(t.getKind() == kind::NEG); if (t[0].isConst()) { @@ -405,8 +406,8 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ }else{ switch(Kind k = t.getKind()){ case kind::REAL_ALGEBRAIC_NUMBER: return rewriteRAN(t); - case kind::MINUS: return rewriteMinus(t); - case kind::UMINUS: return rewriteUMinus(t, true); + case kind::SUB: return rewriteSub(t); + case kind::NEG: return rewriteNeg(t, true); case kind::DIVISION: case kind::DIVISION_TOTAL: return rewriteDiv(t, true); case kind::PLUS: return preRewritePlus(t); @@ -453,8 +454,8 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ Trace("arith-rewriter") << "postRewriteTerm: " << t << std::endl; switch(t.getKind()){ case kind::REAL_ALGEBRAIC_NUMBER: return rewriteRAN(t); - case kind::MINUS: return rewriteMinus(t); - case kind::UMINUS: return rewriteUMinus(t, false); + case kind::SUB: return rewriteSub(t); + case kind::NEG: return rewriteNeg(t, false); case kind::DIVISION: case kind::DIVISION_TOTAL: return rewriteDiv(t, false); case kind::PLUS: return postRewritePlus(t); @@ -801,7 +802,7 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { } else if (rat.sgn() == -1) { - Node ret = nm->mkNode(kind::UMINUS, + Node ret = nm->mkNode(kind::NEG, nm->mkNode(kind::SINE, nm->mkConstReal(-rat))); return RewriteResponse(REWRITE_AGAIN_FULL, ret); } @@ -851,10 +852,8 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { kind::INTS_DIVISION, mkRationalNode(r_abs + rone), ntwo); Node new_pi_factor; if( r.sgn()==1 ){ - new_pi_factor = - nm->mkNode(kind::MINUS, - pi_factor, - nm->mkNode(kind::MULT, ntwo, ra_div_two)); + new_pi_factor = nm->mkNode( + kind::SUB, pi_factor, nm->mkNode(kind::MULT, ntwo, ra_div_two)); }else{ Assert(r.sgn() == -1); new_pi_factor = @@ -882,7 +881,7 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { { return RewriteResponse( REWRITE_AGAIN_FULL, - nm->mkNode(kind::UMINUS, nm->mkNode(kind::SINE, rem))); + nm->mkNode(kind::NEG, nm->mkNode(kind::SINE, rem))); } } else if (rem.isNull()) @@ -917,7 +916,7 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { REWRITE_AGAIN_FULL, nm->mkNode( kind::SINE, - nm->mkNode(kind::MINUS, + nm->mkNode(kind::SUB, nm->mkNode(kind::MULT, nm->mkConstReal(Rational(1) / Rational(2)), mkPi()), @@ -1164,7 +1163,7 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre) // (mod x (- c)) ---> (mod x c) Node nn = nm->mkNode(k, t[0], nm->mkConstInt(-t[1].getConst())); Node ret = (k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL) - ? nm->mkNode(kind::UMINUS, nn) + ? nm->mkNode(kind::NEG, nn) : nn; return returnRewrite(t, ret, Rewrite::DIV_MOD_PULL_NEG_DEN); } diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 90140cc18..072894000 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -56,8 +56,8 @@ class ArithRewriter : public TheoryRewriter static RewriteResponse rewriteRAN(TNode t); static RewriteResponse rewriteVariable(TNode t); - static RewriteResponse rewriteMinus(TNode t); - static RewriteResponse rewriteUMinus(TNode t, bool pre); + static RewriteResponse rewriteSub(TNode t); + static RewriteResponse rewriteNeg(TNode t, bool pre); static RewriteResponse rewriteDiv(TNode t, bool pre); static RewriteResponse rewriteAbs(TNode t); static RewriteResponse rewriteIntsDivMod(TNode t, bool pre); diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index ba326ba56..5d96e019f 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -15,8 +15,8 @@ rewriter ::cvc5::theory::arith::ArithRewriter "theory/arith/arith_rewriter.h" operator PLUS 2: "arithmetic addition (N-ary)" operator MULT 2: "arithmetic multiplication (N-ary)" operator NONLINEAR_MULT 2: "synonym for MULT" -operator MINUS 2 "arithmetic binary subtraction operator" -operator UMINUS 1 "arithmetic unary negation" +operator SUB 2 "arithmetic binary subtraction operator" +operator NEG 1 "arithmetic unary negation" operator DIVISION 2 "real division, division by 0 undefined (user symbol)" operator DIVISION_TOTAL 2 "real division with interpreted division by 0 (internal symbol)" operator INTS_DIVISION 2 "integer division, division by 0 undefined (user symbol)" @@ -121,8 +121,8 @@ operator CAST_TO_REAL 1 "cast term to real same as TO_REAL, but it is used inter typerule PLUS ::cvc5::theory::arith::ArithOperatorTypeRule typerule MULT ::cvc5::theory::arith::ArithOperatorTypeRule typerule NONLINEAR_MULT ::cvc5::theory::arith::ArithOperatorTypeRule -typerule MINUS ::cvc5::theory::arith::ArithOperatorTypeRule -typerule UMINUS ::cvc5::theory::arith::ArithOperatorTypeRule +typerule SUB ::cvc5::theory::arith::ArithOperatorTypeRule +typerule NEG ::cvc5::theory::arith::ArithOperatorTypeRule typerule DIVISION ::cvc5::theory::arith::ArithOperatorTypeRule typerule POW ::cvc5::theory::arith::ArithOperatorTypeRule diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index a16ffdd02..887ef3f1b 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -717,7 +717,7 @@ Node MonomialCheck::mkLit(Node a, Node b, int status, bool isAbsolute) const { return a_eq_b; } - Node negate_b = NodeManager::currentNM()->mkNode(Kind::UMINUS, b); + Node negate_b = NodeManager::currentNM()->mkNode(Kind::NEG, b); return a_eq_b.orNode(a.eqNode(negate_b)); } else if (status < 0) @@ -734,8 +734,8 @@ Node MonomialCheck::mkLit(Node a, Node b, int status, bool isAbsolute) const // return nm->mkNode( greater_op, mkAbs( a ), mkAbs( b ) ); Node a_is_nonnegative = nm->mkNode(Kind::GEQ, a, d_data->d_zero); Node b_is_nonnegative = nm->mkNode(Kind::GEQ, b, d_data->d_zero); - Node negate_a = nm->mkNode(Kind::UMINUS, a); - Node negate_b = nm->mkNode(Kind::UMINUS, b); + Node negate_a = nm->mkNode(Kind::NEG, a); + Node negate_b = nm->mkNode(Kind::NEG, b); return a_is_nonnegative.iteNode( b_is_nonnegative.iteNode(nm->mkNode(greater_op, a, b), nm->mkNode(greater_op, a, negate_b)), diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp index ff6d6a5e8..fe134abb4 100644 --- a/src/theory/arith/nl/ext/proof_checker.cpp +++ b/src/theory/arith/nl/ext/proof_checker.cpp @@ -136,7 +136,7 @@ Node ExtProofRuleChecker::checkInternal(PfRule id, Node b = args[4]; int sgn = args[5].getConst().getNumerator().sgn(); Assert(sgn == -1 || sgn == 1); - Node tplane = nm->mkNode(Kind::MINUS, + Node tplane = nm->mkNode(Kind::SUB, nm->mkNode(Kind::PLUS, nm->mkNode(Kind::MULT, b, x), nm->mkNode(Kind::MULT, a, y)), diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp index fbf8caf6a..4ec1f2ca2 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.cpp +++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp @@ -119,7 +119,7 @@ void TangentPlaneCheck::check(bool asWaitingLemmas) Node b_v = pts[1][p]; // tangent plane - Node tplane = nm->mkNode(Kind::MINUS, + Node tplane = nm->mkNode(Kind::SUB, nm->mkNode(Kind::PLUS, nm->mkNode(Kind::MULT, b_v, a), nm->mkNode(Kind::MULT, a_v, b)), diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index c661dab4b..dc6b9c9d7 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -220,7 +220,7 @@ Node IAndSolver::mkIOr(unsigned k, Node x, Node y) const Node IAndSolver::mkINot(unsigned k, Node x) const { NodeManager* nm = NodeManager::currentNM(); - Node ret = nm->mkNode(MINUS, d_iandUtils.twoToKMinusOne(k), x); + Node ret = nm->mkNode(SUB, d_iandUtils.twoToKMinusOne(k), x); ret = rewrite(ret); return ret; } diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp index 700eb6de9..d64c19963 100644 --- a/src/theory/arith/nl/iand_utils.cpp +++ b/src/theory/arith/nl/iand_utils.cpp @@ -267,7 +267,7 @@ Node IAndUtils::twoToKMinusOne(unsigned k) const { // could be faster NodeManager* nm = NodeManager::currentNM(); - return nm->mkNode(kind::MINUS, twoToK(k), d_one); + return nm->mkNode(kind::SUB, twoToK(k), d_one); } } // namespace nl diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index 90138bf3e..1f50290c1 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -676,7 +676,7 @@ bool NlModel::simpleCheckModelLit(Node lit) Trace("nl-ext-cms-debug") << " b = " << b << std::endl; // find maximal/minimal value on the interval Node apex = nm->mkNode( - DIVISION, nm->mkNode(UMINUS, b), nm->mkNode(MULT, d_two, a)); + DIVISION, nm->mkNode(NEG, b), nm->mkNode(MULT, d_two, a)); apex = rewrite(apex); Assert(apex.isConst()); // for lower, upper, whether we are greater than the apex diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 77e5f9f3f..3992c31f6 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -264,7 +264,7 @@ std::pair ExponentialSolver::getSecantBounds(TNode e, { // pick c-1 bounds.first = rewrite( - NodeManager::currentNM()->mkNode(Kind::MINUS, center, d_data->d_one)); + NodeManager::currentNM()->mkNode(Kind::SUB, center, d_data->d_one)); } if (bounds.second.isNull()) { diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp index 3bf1ace98..cbf867ef4 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.cpp +++ b/src/theory/arith/nl/transcendental/proof_checker.cpp @@ -51,9 +51,9 @@ Node mkSecant(TNode t, TNode l, TNode u, TNode evall, TNode evalu) evall, nm->mkNode(Kind::MULT, nm->mkNode(Kind::DIVISION, - nm->mkNode(Kind::MINUS, evall, evalu), - nm->mkNode(Kind::MINUS, l, u)), - nm->mkNode(Kind::MINUS, t, l))); + nm->mkNode(Kind::SUB, evall, evalu), + nm->mkNode(Kind::SUB, l, u)), + nm->mkNode(Kind::SUB, t, l))); } } // namespace @@ -271,10 +271,10 @@ Node TranscendentalProofRuleChecker::checkInternal( AND, nm->mkNode(IMPLIES, nm->mkNode(GT, args[0], mpi), - nm->mkNode(GT, s, nm->mkNode(MINUS, mpi, args[0]))), + nm->mkNode(GT, s, nm->mkNode(SUB, mpi, args[0]))), nm->mkNode(IMPLIES, nm->mkNode(LT, args[0], pi), - nm->mkNode(LT, s, nm->mkNode(MINUS, pi, args[0])))); + nm->mkNode(LT, s, nm->mkNode(SUB, pi, args[0])))); } else if (id == PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG) { diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index d574a9572..3c5ae8006 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -189,13 +189,12 @@ void SineSolver::checkInitialRefine() nm->mkNode(Kind::GT, t[0], d_data->d_pi_neg), nm->mkNode(Kind::GT, t, - nm->mkNode(Kind::MINUS, d_data->d_pi_neg, t[0]))), + nm->mkNode(Kind::SUB, d_data->d_pi_neg, t[0]))), nm->mkNode( Kind::IMPLIES, nm->mkNode(Kind::LT, t[0], d_data->d_pi), - nm->mkNode(Kind::LT, - t, - nm->mkNode(Kind::MINUS, d_data->d_pi, t[0])))); + nm->mkNode( + Kind::LT, t, nm->mkNode(Kind::SUB, d_data->d_pi, t[0])))); CDProof* proof = nullptr; if (d_data->isProofEnabled()) { diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp index c9e0015e2..5afe3a705 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.cpp +++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp @@ -121,7 +121,7 @@ void TaylorGenerator::getPolynomialApproximationBounds( else { Assert(k == Kind::SINE); - Node l = nm->mkNode(Kind::MINUS, taylor_sum, ru); + Node l = nm->mkNode(Kind::SUB, taylor_sum, ru); Node u = nm->mkNode(Kind::PLUS, taylor_sum, ru); pbounds.d_lower = l; pbounds.d_upperNeg = u; diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index e32f336ac..fd5f7d07a 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -268,7 +268,7 @@ Node TranscendentalState::mkSecantPlane( { NodeManager* nm = NodeManager::currentNM(); // Figure 3: S_l( x ), S_u( x ) for s = 0,1 - Node rcoeff_n = rewrite(nm->mkNode(Kind::MINUS, lower, upper)); + Node rcoeff_n = rewrite(nm->mkNode(Kind::SUB, lower, upper)); Assert(rcoeff_n.isConst()); Rational rcoeff = rcoeff_n.getConst(); Assert(rcoeff.sgn() != 0); @@ -277,9 +277,9 @@ Node TranscendentalState::mkSecantPlane( lval, nm->mkNode(Kind::MULT, nm->mkNode(Kind::DIVISION, - nm->mkNode(Kind::MINUS, lval, uval), - nm->mkNode(Kind::MINUS, lower, upper)), - nm->mkNode(Kind::MINUS, arg, lower))); + nm->mkNode(Kind::SUB, lval, uval), + nm->mkNode(Kind::SUB, lower, upper)), + nm->mkNode(Kind::SUB, arg, lower))); Trace("nl-trans") << "Creating secant plane for transcendental function of " << arg << std::endl; Trace("nl-trans") << "\tfrom ( " << lower << " ; " << lval << " ) to ( " diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index f346d7596..ab98f67ac 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -124,7 +124,7 @@ Node OperatorElim::eliminateOperators(Node node, bvm->mkBoundVar(node[0], nm->integerType()); Node one = nm->mkConstReal(Rational(1)); Node zero = nm->mkConstReal(Rational(0)); - Node diff = nm->mkNode(MINUS, node[0], v); + Node diff = nm->mkNode(SUB, node[0], v); Node lem = mkInRange(diff, zero, one); Node toIntSkolem = mkWitnessTerm(v, @@ -227,7 +227,7 @@ Node OperatorElim::eliminateOperators(Node node, v, lem, "linearIntDiv", "the result of an intdiv-by-k term", lems); if (k == INTS_MODULUS_TOTAL) { - Node nn = nm->mkNode(MINUS, num, nm->mkNode(MULT, den, intVar)); + Node nn = nm->mkNode(SUB, num, nm->mkNode(MULT, den, intVar)); return nn; } else @@ -320,7 +320,7 @@ Node OperatorElim::eliminateOperators(Node node, nm->mkNode(LT, node[0], nm->mkConstRealOrInt(node[0].getType(), Rational(0))), - nm->mkNode(UMINUS, node[0]), + nm->mkNode(NEG, node[0]), node[0]); break; } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 61dbe4fce..60f925e75 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -342,7 +342,7 @@ EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) { { return d_internal->getEqualityStatus(a,b); } - Node diff = d_env.getNodeManager()->mkNode(Kind::MINUS, a, b); + Node diff = d_env.getNodeManager()->mkNode(Kind::SUB, a, b); std::optional isZero = isExpressionZero(d_env, diff, d_arithModelCache); if (isZero) { diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 4efdfc2bf..572af7fb3 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -3782,10 +3782,12 @@ DeltaRational TheoryArithPrivate::getDeltaValue(TNode term) const } return value; } - case kind::MINUS: { // 2 args + case kind::SUB: + { // 2 args return getDeltaValue(term[0]) - getDeltaValue(term[1]); } - case kind::UMINUS: { // 1 arg + case kind::NEG: + { // 1 arg return (-getDeltaValue(term[0])); } @@ -4878,8 +4880,7 @@ bool TheoryArithPrivate::decomposeLiteral(Node lit, Kind& k, int& dir, Rational& success = decomposeTerm(rewrite(right), rm, rp, rc); if(!success){ return false; } - Node diff = - rewrite(NodeManager::currentNM()->mkNode(kind::MINUS, left, right)); + Node diff = rewrite(NodeManager::currentNM()->mkNode(kind::SUB, left, right)); Rational dc; success = decomposeTerm(diff, dm, dp, dc); Assert(success); diff --git a/src/theory/bags/bag_reduction.cpp b/src/theory/bags/bag_reduction.cpp index a6895e4b1..4e4b75c09 100644 --- a/src/theory/bags/bag_reduction.cpp +++ b/src/theory/bags/bag_reduction.cpp @@ -87,7 +87,7 @@ Node BagReduction::reduceFoldOperator(Node node, std::vector& asserts) Node i = bvm->mkBoundVar(node, "i", nm->integerType()); Node iList = nm->mkNode(BOUND_VAR_LIST, i); - Node iMinusOne = nm->mkNode(MINUS, i, one); + Node iMinusOne = nm->mkNode(SUB, i, one); Node uf_i = nm->mkNode(APPLY_UF, uf, i); Node combine_0 = nm->mkNode(APPLY_UF, combine, zero); Node combine_iMinusOne = nm->mkNode(APPLY_UF, combine, iMinusOne); @@ -158,7 +158,7 @@ Node BagReduction::reduceCardOperator(Node node, std::vector& asserts) bvm->mkBoundVar(node, "j", nm->integerType()); Node iList = nm->mkNode(BOUND_VAR_LIST, i); Node jList = nm->mkNode(BOUND_VAR_LIST, j); - Node iMinusOne = nm->mkNode(MINUS, i, one); + Node iMinusOne = nm->mkNode(SUB, i, one); Node uf_i = nm->mkNode(APPLY_UF, uf, i); Node uf_j = nm->mkNode(APPLY_UF, uf, j); Node cardinality_0 = nm->mkNode(APPLY_UF, cardinality, zero); diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index 3247548c5..248f0337e 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -262,7 +262,7 @@ InferInfo InferenceGenerator::differenceSubtract(Node n, Node e) Node skolem = getSkolem(n, inferInfo); Node count = getMultiplicityTerm(e, skolem); - Node subtract = d_nm->mkNode(MINUS, countA, countB); + Node subtract = d_nm->mkNode(SUB, countA, countB); Node gte = d_nm->mkNode(GEQ, countA, countB); Node difference = d_nm->mkNode(ITE, gte, subtract, d_zero); Node equal = count.eqNode(difference); @@ -447,7 +447,7 @@ std::tuple InferenceGenerator::mapDownwards(Node n, Node iList = d_nm->mkNode(BOUND_VAR_LIST, i); Node jList = d_nm->mkNode(BOUND_VAR_LIST, j); Node iPlusOne = d_nm->mkNode(PLUS, i, d_one); - Node iMinusOne = d_nm->mkNode(MINUS, i, d_one); + Node iMinusOne = d_nm->mkNode(SUB, i, d_one); Node uf_i = d_nm->mkNode(APPLY_UF, uf, i); Node uf_j = d_nm->mkNode(APPLY_UF, uf, j); Node f_uf_i = d_nm->mkNode(APPLY_UF, f, uf_i); diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp index b761a5dcd..f69ca7854 100644 --- a/src/theory/bv/int_blaster.cpp +++ b/src/theory/bv/int_blaster.cpp @@ -303,7 +303,7 @@ Node IntBlaster::translateWithChildren( returnNode = d_nm->mkNode( kind::ITE, d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero), - d_nm->mkNode(kind::MINUS, pow2BvSize, d_one), + d_nm->mkNode(kind::SUB, pow2BvSize, d_one), divNode); break; } @@ -598,7 +598,7 @@ Node IntBlaster::uts(Node x, uint64_t bvsize) Node modNode = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, x, powNode); Node two = d_nm->mkConstInt(Rational(2)); Node twoTimesNode = d_nm->mkNode(kind::MULT, two, modNode); - return d_nm->mkNode(kind::MINUS, twoTimesNode, x); + return d_nm->mkNode(kind::SUB, twoTimesNode, x); } Node IntBlaster::createSignExtendNode(Node x, uint64_t bvsize, uint64_t amount) @@ -1064,7 +1064,7 @@ Node IntBlaster::createBVOrNode(Node x, Node IntBlaster::createBVSubNode(Node x, Node y, uint64_t bvsize) { - Node minus = d_nm->mkNode(kind::MINUS, x, y); + Node minus = d_nm->mkNode(kind::SUB, x, y); Node p2 = pow2(bvsize); return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, minus, p2); } @@ -1081,12 +1081,12 @@ Node IntBlaster::createBVNegNode(Node n, uint64_t bvsize) // Based on Hacker's Delight section 2-2 equation a: // -x = ~x+1 Node p2 = pow2(bvsize); - return d_nm->mkNode(kind::MINUS, p2, n); + return d_nm->mkNode(kind::SUB, p2, n); } Node IntBlaster::createBVNotNode(Node n, uint64_t bvsize) { - return d_nm->mkNode(kind::MINUS, maxInt(bvsize), n); + return d_nm->mkNode(kind::SUB, maxInt(bvsize), n); } } // namespace cvc5 diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 1134c0a5a..2ec6dfe1b 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -701,7 +701,7 @@ Node SygusExtension::getSimpleSymBreakPred(Node e, if (doSymBreak) { // direct solving for children - // for instance, we may want to insist that the LHS of MINUS is 0 + // for instance, we may want to insist that the LHS of SUB is 0 Trace("sygus-sb-simple-debug") << " Solve children..." << std::endl; std::map children_solved; for (unsigned j = 0; j < dt_index_nargs; j++) @@ -747,7 +747,7 @@ Node SygusExtension::getSimpleSymBreakPred(Node e, { // other cases of rewriting x k x -> x' Node req_const; - if (nk == GT || nk == LT || nk == XOR || nk == MINUS + if (nk == GT || nk == LT || nk == XOR || nk == SUB || nk == BITVECTOR_SUB || nk == BITVECTOR_XOR || nk == BITVECTOR_UREM) { diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp index 4826e87bc..c819218ce 100644 --- a/src/theory/datatypes/sygus_simple_sym.cpp +++ b/src/theory/datatypes/sygus_simple_sym.cpp @@ -200,7 +200,7 @@ bool SygusSimpleSymBreak::considerArgKind( Assert(rt.empty()); // construct rt by cases - if (pk == NOT || pk == BITVECTOR_NOT || pk == UMINUS || pk == BITVECTOR_NEG) + if (pk == NOT || pk == BITVECTOR_NOT || pk == NEG || pk == BITVECTOR_NEG) { // negation normal form if (pk == k) @@ -280,12 +280,12 @@ bool SygusSimpleSymBreak::considerArgKind( rt.d_req_kind = BITVECTOR_XNOR; } } - else if (pk == UMINUS) + else if (pk == NEG) { if (k == PLUS) { rt.d_req_kind = PLUS; - reqk = UMINUS; + reqk = NEG; } } else if (pk == BITVECTOR_NEG) @@ -327,17 +327,17 @@ bool SygusSimpleSymBreak::considerArgKind( } } } - else if (k == MINUS || k == BITVECTOR_SUB) + else if (k == SUB || k == BITVECTOR_SUB) { - if (pk == EQUAL || pk == MINUS || pk == BITVECTOR_SUB || pk == LEQ - || pk == LT || pk == GEQ || pk == GT) + if (pk == EQUAL || pk == SUB || pk == BITVECTOR_SUB || pk == LEQ || pk == LT + || pk == GEQ || pk == GT) { int oarg = arg == 0 ? 1 : 0; // (~ x (- y z)) ----> (~ (+ x z) y) // (~ (- 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_ADD; + rt.d_children[oarg].d_req_kind = k == SUB ? 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); } @@ -345,7 +345,7 @@ bool SygusSimpleSymBreak::considerArgKind( { // (+ x (- y z)) -----> (- (+ x y) z) // (+ (- y z) x) -----> (- (+ x y) z) - rt.d_req_kind = pk == PLUS ? MINUS : BITVECTOR_SUB; + rt.d_req_kind = pk == PLUS ? SUB : BITVECTOR_SUB; int oarg = arg == 0 ? 1 : 0; rt.d_children[0].d_req_kind = pk; rt.d_children[0].d_children[0].d_req_type = pdt[pc].getArgType(oarg); diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index 6b4176c13..1ab234ae9 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -427,7 +427,7 @@ EvalResult Evaluator::evalInternal( break; } - case kind::MINUS: + case kind::SUB: { const Rational& x = results[currNode[0]].d_rat; const Rational& y = results[currNode[1]].d_rat; @@ -435,7 +435,7 @@ EvalResult Evaluator::evalInternal( break; } - case kind::UMINUS: + case kind::NEG: { const Rational& x = results[currNode[0]].d_rat; results[currNode] = EvalResult(-x); diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index ecf2d9a48..6528959c3 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -291,8 +291,8 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, else { Node delta = d_vtc->getVtsDelta(); - uval = nm->mkNode( - uires == CEG_TT_UPPER_STRICT ? PLUS : MINUS, uval, delta); + uval = + nm->mkNode(uires == CEG_TT_UPPER_STRICT ? PLUS : SUB, uval, delta); uval = rewrite(uval); } } @@ -363,7 +363,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, // could get rho value for infinity here if (rr == 0) { - val = nm->mkNode(UMINUS, val); + val = nm->mkNode(NEG, val); val = rewrite(val); } TermProperties pv_prop_no_bound; @@ -623,7 +623,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, } else if (!vals[1].isNull()) { - val = nm->mkNode(MINUS, vals[1], d_one); + val = nm->mkNode(SUB, vals[1], d_one); val = rewrite(val); } } @@ -933,8 +933,8 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci, (msum[pv].isNull() || msum[pv].getConst().sgn() == 1) ? 1 : -1; val = rewrite( - nm->mkNode(ires_use == -1 ? PLUS : MINUS, - nm->mkNode(ires_use == -1 ? MINUS : PLUS, val, realPart), + nm->mkNode(ires_use == -1 ? PLUS : SUB, + nm->mkNode(ires_use == -1 ? SUB : PLUS, val, realPart), nm->mkNode(TO_INTEGER, realPart))); // could round up for upper bounds here Trace("cegqi-arith-debug") << "result : " << val << std::endl; @@ -1001,11 +1001,11 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci, Node rho; if (isLower) { - rho = nm->mkNode(MINUS, ceValue, mt); + rho = nm->mkNode(SUB, ceValue, mt); } else { - rho = nm->mkNode(MINUS, mt, ceValue); + rho = nm->mkNode(SUB, mt, ceValue); } rho = rewrite(rho); Trace("cegqi-arith-bound2") @@ -1015,7 +1015,7 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci, rho = nm->mkNode(INTS_MODULUS_TOTAL, rho, new_theta); rho = rewrite(rho); Trace("cegqi-arith-bound2") << rho << std::endl; - Kind rk = isLower ? PLUS : MINUS; + Kind rk = isLower ? PLUS : SUB; val = nm->mkNode(rk, val, rho); val = rewrite(val); Trace("cegqi-arith-bound2") << "(after rho) : " << val << std::endl; diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 45ac899e1..bd3f616d6 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -1272,7 +1272,7 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >& atom_lhs = atom[0]; atom_rhs = atom[1]; }else{ - atom_lhs = nm->mkNode(MINUS, atom[0], atom[1]); + atom_lhs = nm->mkNode(SUB, atom[0], atom[1]); atom_lhs = rewrite(atom_lhs); atom_rhs = nm->mkConstRealOrInt(atom_lhs.getType(), Rational(0)); } diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index ab4bbc91b..fe852a90c 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -364,8 +364,8 @@ int InstMatchGenerator::getMatch(Node f, Node t, InstMatch& m) { if (pat.getKind() == GT) { - t_match = nm->mkNode( - MINUS, t, nm->mkConstRealOrInt(t.getType(), Rational(1))); + t_match = + nm->mkNode(SUB, t, nm->mkConstRealOrInt(t.getType(), Rational(1))); }else{ t_match = t; } diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp index e4d7436c8..e792faa5f 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp +++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp @@ -671,7 +671,7 @@ Node PatternTermSelector::getInversion(Node n, Node x) { if (nk == PLUS) { - x = nm->mkNode(MINUS, x, nc); + x = nm->mkNode(SUB, x, nc); } else if (nk == MULT) { @@ -685,7 +685,7 @@ Node PatternTermSelector::getInversion(Node n, Node x) } if (nc.getConst().sgn() < 0) { - x = nm->mkNode(UMINUS, x); + x = nm->mkNode(NEG, x); } } else diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 5c0283863..54fa24c76 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -369,7 +369,7 @@ void BoundedIntegers::checkOwnership(Node f) != bound_int_range_term[b].end()); d_bounds[b][f][v] = bound_int_range_term[b][v]; } - Node r = nm->mkNode(MINUS, d_bounds[1][f][v], d_bounds[0][f][v]); + Node r = nm->mkNode(SUB, d_bounds[1][f][v], d_bounds[0][f][v]); d_range[f][v] = rewrite(r); Trace("bound-int") << "Variable " << v << " is bound because of int range literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl; } @@ -814,7 +814,7 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node }else{ NodeManager* nm = NodeManager::currentNM(); Trace("bound-int-rsi") << "Can limit bounds of " << v << " to " << l << "..." << u << std::endl; - Node range = rewrite(nm->mkNode(MINUS, u, l)); + Node range = rewrite(nm->mkNode(SUB, u, l)); // 9999 is an arbitrary range past which we do not do exhaustive // bounded instantation, based on the check below. Node ra = diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index e1bebee74..f87b1ab2c 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -836,7 +836,7 @@ bool QuantInfo::completeMatch(std::vector& assigned, bool doContinue) { Kind kn = k; if( d_vars[index].getKind()==PLUS ){ - kn = MINUS; + kn = SUB; } if( kn!=k ){ sum = NodeManager::currentNM()->mkNode( kn, v, lhs ); diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 67df20694..f1260eb69 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -932,7 +932,7 @@ Node QuantifiersRewriter::getVarElimEqString(Node lit, STRING_SUBSTR, slv, tpreL, - nm->mkNode(MINUS, slvL, nm->mkNode(PLUS, tpreL, tpostL))); + nm->mkNode(SUB, slvL, nm->mkNode(PLUS, tpreL, tpostL))); // forall x. r ++ x ++ t = s => P( x ) // is equivalent to // r ++ s' ++ t = s => P( s' ) where diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 6399340aa..fdd5fa0ac 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -288,7 +288,7 @@ Node Skolemize::mkSkolemizedBody(Node f, Node icond = nm->mkNode(GEQ, k, nm->mkConstInt(Rational(0))); Node iret = ret.substitute(ind_vars[0], - nm->mkNode(MINUS, k, nm->mkConstInt(Rational(1)))) + nm->mkNode(SUB, k, nm->mkConstInt(Rational(1)))) .negate(); n_str_ind = nm->mkNode(OR, icond.negate(), iret); n_str_ind = nm->mkNode(AND, icond, n_str_ind); diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 13f52a12f..dc7b3d5e9 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -773,8 +773,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( if (types[i].isRealOrInt()) { - // Add PLUS, MINUS - Kind kinds[2] = {PLUS, MINUS}; + // Add PLUS, SUB + Kind kinds[2] = {PLUS, SUB}; for (const Kind kind : kinds) { Trace("sygus-grammar-def") << "...add for " << kind << std::endl; diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index e1491936a..2d0561462 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -610,7 +610,7 @@ Node SygusSampler::getRandomValue(TypeNode tn) if (Random::getRandom().pickWithProb(0.5)) { // negative - ret = nm->mkNode(kind::UMINUS, ret); + ret = nm->mkNode(kind::NEG, ret); } ret = d_env.getRewriter()->rewrite(ret); Assert(ret.isConst()); diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 5bd22f986..23372b794 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -263,7 +263,7 @@ Node TermUtil::mkNegate(Kind notk, Node n) bool TermUtil::isNegate(Kind k) { - return k == NOT || k == BITVECTOR_NOT || k == BITVECTOR_NEG || k == UMINUS; + return k == NOT || k == BITVECTOR_NOT || k == BITVECTOR_NEG || k == NEG; } bool TermUtil::isAssoc(Kind k, bool reqNAry) @@ -437,7 +437,7 @@ bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg) { return true; } - else if (ik == MINUS || ik == BITVECTOR_SHL || ik == BITVECTOR_LSHR + else if (ik == SUB || ik == BITVECTOR_SHL || ik == BITVECTOR_LSHR || ik == BITVECTOR_ASHR || ik == BITVECTOR_SUB || ik == BITVECTOR_UREM) { diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index cb9b26731..9cf2a908d 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -282,7 +282,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { else if (node[0].getKind() == kind::SET_UNION) { Node ret = NodeManager::currentNM()->mkNode( - kind::MINUS, + kind::SUB, NodeManager::currentNM()->mkNode( kind::PLUS, NodeManager::currentNM()->mkNode(kind::SET_CARD, node[0][0]), @@ -296,7 +296,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { else if (node[0].getKind() == kind::SET_MINUS) { Node ret = NodeManager::currentNM()->mkNode( - kind::MINUS, + kind::SUB, NodeManager::currentNM()->mkNode(kind::SET_CARD, node[0][0]), NodeManager::currentNM()->mkNode( kind::SET_CARD, diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp index 0659a2ff9..46d89520b 100644 --- a/src/theory/strings/arith_entail.cpp +++ b/src/theory/strings/arith_entail.cpp @@ -54,7 +54,7 @@ bool ArithEntail::check(Node a, Node b, bool strict) { return !strict; } - Node diff = NodeManager::currentNM()->mkNode(kind::MINUS, a, b); + Node diff = NodeManager::currentNM()->mkNode(kind::SUB, a, b); return check(diff, strict); } @@ -76,10 +76,9 @@ bool ArithEntail::check(Node a, bool strict) return a.getConst().sgn() >= (strict ? 1 : 0); } - Node ar = - strict ? NodeManager::currentNM()->mkNode( - kind::MINUS, a, NodeManager::currentNM()->mkConstInt(Rational(1))) - : a; + Node ar = strict ? NodeManager::currentNM()->mkNode( + kind::SUB, a, NodeManager::currentNM()->mkConstInt(Rational(1))) + : a; ar = d_rr->rewrite(ar); if (ar.getAttribute(StrCheckEntailArithComputedAttr())) @@ -417,7 +416,7 @@ void ArithEntail::getArithApproximations(Node a, { // n <= len( x ) implies // len( x ) - n >= len( substr( x, n, m ) ) - approx.push_back(nm->mkNode(MINUS, lenx, a[0][1])); + approx.push_back(nm->mkNode(SUB, lenx, a[0][1])); } else { @@ -438,7 +437,7 @@ void ArithEntail::getArithApproximations(Node a, // len(x)-n <= len( substr( x, n, m ) ) if (check(a[0][1]) && check(npm, lenx)) { - approx.push_back(nm->mkNode(MINUS, lenx, a[0][1])); + approx.push_back(nm->mkNode(SUB, lenx, a[0][1])); } } } @@ -474,7 +473,7 @@ void ArithEntail::getArithApproximations(Node a, else { // len( x ) - len( y ) <= len( replace( x, y, z ) ) - approx.push_back(nm->mkNode(MINUS, lenx, leny)); + approx.push_back(nm->mkNode(SUB, lenx, leny)); } } } @@ -524,7 +523,7 @@ void ArithEntail::getArithApproximations(Node a, { // len( x ) >= len( y ) implies // len( x ) - len( y ) >= indexof( x, y, n ) - approx.push_back(nm->mkNode(MINUS, lenx, leny)); + approx.push_back(nm->mkNode(SUB, lenx, leny)); } else { @@ -577,7 +576,7 @@ bool ArithEntail::checkWithEqAssumption(Node assumption, Node a, bool strict) toVisit.pop_back(); if (curr.getKind() == kind::PLUS || curr.getKind() == kind::MULT - || curr.getKind() == kind::MINUS || curr.getKind() == kind::EQUAL) + || curr.getKind() == kind::SUB || curr.getKind() == kind::EQUAL) { for (const auto& currChild : curr) { @@ -660,8 +659,7 @@ bool ArithEntail::checkWithAssumption(Node assumption, // (not (>= s t)) --> (>= (t - 1) s) Assert(assumption.getKind() == kind::NOT && assumption[0].getKind() == kind::GEQ); - x = nm->mkNode( - kind::MINUS, assumption[0][1], nm->mkConstInt(Rational(1))); + x = nm->mkNode(kind::SUB, assumption[0][1], nm->mkConstInt(Rational(1))); y = assumption[0][0]; } @@ -671,7 +669,7 @@ bool ArithEntail::checkWithAssumption(Node assumption, nm->mkNode(kind::EQUAL, x, nm->mkNode(kind::PLUS, y, slen))); } - Node diff = nm->mkNode(kind::MINUS, a, b); + Node diff = nm->mkNode(kind::SUB, a, b); bool res = false; if (assumption.isConst()) { diff --git a/src/theory/strings/array_core_solver.cpp b/src/theory/strings/array_core_solver.cpp index c7e72c11f..58d1efaf7 100644 --- a/src/theory/strings/array_core_solver.cpp +++ b/src/theory/strings/array_core_solver.cpp @@ -237,7 +237,7 @@ void ArrayCoreSolver::check(const std::vector& nthTerms, Node i = n[1]; Node sLen = nm->mkNode(STRING_LENGTH, s); Node iRev = nm->mkNode( - MINUS, sLen, nm->mkNode(PLUS, i, nm->mkConstInt(Rational(1)))); + SUB, sLen, nm->mkNode(PLUS, i, nm->mkConstInt(Rational(1)))); std::vector nexp; nexp.push_back(nm->mkNode(LEQ, nm->mkConstInt(Rational(0)), i)); diff --git a/src/theory/strings/array_solver.cpp b/src/theory/strings/array_solver.cpp index 90725bd2a..d7663170a 100644 --- a/src/theory/strings/array_solver.cpp +++ b/src/theory/strings/array_solver.cpp @@ -267,7 +267,7 @@ void ArraySolver::checkTerm(Node t, bool checkInv) if (!lacc.empty()) { currSum = lacc.size() == 1 ? lacc[0] : nm->mkNode(PLUS, lacc); - currIndex = nm->mkNode(MINUS, currIndex, currSum); + currIndex = nm->mkNode(SUB, currIndex, currSum); } Node cc; if (k == STRING_UPDATE && checkInv) diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index ee54b0fce..f2fe97c7b 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -834,7 +834,7 @@ Node CoreSolver::getDecomposeConclusion(Node x, { Assert(l.getType().isInteger()); NodeManager* nm = NodeManager::currentNM(); - Node n = isRev ? nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, x), l) : l; + Node n = isRev ? nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, x), l) : l; Node sk1 = skc->mkSkolemCached(x, n, SkolemCache::SK_PREFIX, "dc_spt1"); newSkolems.push_back(sk1); Node sk2 = skc->mkSkolemCached(x, n, SkolemCache::SK_SUFFIX_REM, "dc_spt2"); diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index a638d6009..a94f09cb7 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -160,7 +160,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) Node ppSum = childLengthsPostPivot.size() == 1 ? childLengthsPostPivot[0] : nm->mkNode(PLUS, childLengthsPostPivot); - currEnd = nm->mkNode(MINUS, lenx, ppSum); + currEnd = nm->mkNode(SUB, lenx, ppSum); } else { @@ -312,7 +312,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) // ... ^ "B" = substr( x, len( x ) - 3, 1 ) ^ ... Node sc = sep_children.back(); Node lenSc = nm->mkNode(STRING_LENGTH, sc); - Node loc = nm->mkNode(MINUS, lenx, nm->mkNode(PLUS, lenSc, cEnd)); + Node loc = nm->mkNode(SUB, lenx, nm->mkNode(PLUS, lenSc, cEnd)); Node scc = sc.eqNode(nm->mkNode(STRING_SUBSTR, x, loc, lenSc)); // We also must ensure that we fit. This constraint is necessary in // addition to the constraint above. Take this example: @@ -415,7 +415,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) Assert(children[index + (r == 0 ? 1 : -1)].getKind() != STRING_TO_REGEXP); Node s = c[0]; Node lens = nm->mkNode(STRING_LENGTH, s); - Node sss = r == 0 ? zero : nm->mkNode(MINUS, lenx, lens); + Node sss = r == 0 ? zero : nm->mkNode(SUB, lenx, lens); Node ss = nm->mkNode(STRING_SUBSTR, x, sss, lens); sConstraints.push_back(ss.eqNode(s)); if (r == 0) @@ -428,7 +428,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) Node bound = nm->mkNode(GEQ, sss, sStartIndex); sConstraints.push_back(bound); } - sLength = nm->mkNode(MINUS, sLength, lens); + sLength = nm->mkNode(SUB, sLength, lens); } if (r == 1 && !sConstraints.empty()) { @@ -470,7 +470,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) } else if (i + 1 == nchildren) { - k = nm->mkNode(MINUS, lenx, lens); + k = nm->mkNode(SUB, lenx, lens); } else { @@ -481,7 +481,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) Node bound = nm->mkNode(AND, nm->mkNode(LEQ, zero, k), - nm->mkNode(LEQ, k, nm->mkNode(MINUS, lenx, lens))); + nm->mkNode(LEQ, k, nm->mkNode(SUB, lenx, lens))); echildren.push_back(bound); } Node substrEq = nm->mkNode(STRING_SUBSTR, x, k, lens).eqNode(s); @@ -503,7 +503,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) Node ks = nm->mkNode(PLUS, k, lens); Node substrSuffix = nm->mkNode( STRING_IN_REGEXP, - nm->mkNode(STRING_SUBSTR, x, ks, nm->mkNode(MINUS, lenx, ks)), + nm->mkNode(STRING_SUBSTR, x, ks, nm->mkNode(SUB, lenx, ks)), rps); echildren.push_back(substrSuffix); } diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index eb6d2d355..2b6c4a697 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -929,7 +929,7 @@ Node RegExpOpr::reduceRegExpNeg(Node mem) nm->mkNode(AND, nm->mkNode(GT, b1, zero), nm->mkNode(GEQ, lens, b1)); // internal Node s1 = nm->mkNode(STRING_SUBSTR, s, zero, b1); - Node s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(MINUS, lens, b1)); + Node s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(SUB, lens, b1)); Node s1r1 = nm->mkNode(STRING_IN_REGEXP, s1, r[0]).negate(); Node s2r2 = nm->mkNode(STRING_IN_REGEXP, s2, r).negate(); @@ -984,12 +984,12 @@ Node RegExpOpr::reduceRegExpNegConcatFixed(Node mem, Node reLen, size_t index) if (index == 0) { s1 = nm->mkNode(STRING_SUBSTR, s, zero, b1); - s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(MINUS, lens, b1)); + s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(SUB, lens, b1)); } else { - s1 = nm->mkNode(STRING_SUBSTR, s, nm->mkNode(MINUS, lens, b1), b1); - s2 = nm->mkNode(STRING_SUBSTR, s, zero, nm->mkNode(MINUS, lens, b1)); + s1 = nm->mkNode(STRING_SUBSTR, s, nm->mkNode(SUB, lens, b1), b1); + s2 = nm->mkNode(STRING_SUBSTR, s, zero, nm->mkNode(SUB, lens, b1)); } Node s1r1 = nm->mkNode(STRING_IN_REGEXP, s1, r[index]).negate(); std::vector nvec; diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index bbe25b7a3..3068c6815 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -1989,8 +1989,7 @@ Node SequencesRewriter::rewriteSubstr(Node node) else { // strip up to ( str.len(node[0]) - end_pt ) off the end of the string - curr = - d_arithEntail.rewrite(nm->mkNode(kind::MINUS, tot_len, end_pt)); + curr = d_arithEntail.rewrite(nm->mkNode(kind::SUB, tot_len, end_pt)); } } } @@ -2031,8 +2030,8 @@ Node SequencesRewriter::rewriteSubstr(Node node) // the length of a string from the inner substr subtracts the start point // of the outer substr - Node len_from_inner = d_arithEntail.rewrite( - nm->mkNode(kind::MINUS, node[0][2], start_outer)); + Node len_from_inner = + d_arithEntail.rewrite(nm->mkNode(kind::SUB, node[0][2], start_outer)); Node len_from_outer = node[2]; Node new_len; // take quantity that is for sure smaller than the other @@ -2136,7 +2135,7 @@ Node SequencesRewriter::rewriteUpdate(Node node) { // str.update(str.rev(s), n, t) ---> // str.rev(str.update(s, len(s) - (n + 1), t)) - Node idx = nm->mkNode(MINUS, + Node idx = nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, s), nm->mkNode(PLUS, i, nm->mkConstInt(Rational(1)))); Node ret = nm->mkNode(STRING_REV, nm->mkNode(STRING_UPDATE, s[0], idx, x)); @@ -2579,7 +2578,7 @@ Node SequencesRewriter::rewriteIndexof(Node node) Node len0 = nm->mkNode(STRING_LENGTH, node[0]); Node len1 = nm->mkNode(STRING_LENGTH, node[1]); - Node len0m2 = nm->mkNode(MINUS, len0, node[2]); + Node len0m2 = nm->mkNode(SUB, len0, node[2]); if (node[1].isConst()) { @@ -2669,7 +2668,7 @@ Node SequencesRewriter::rewriteIndexof(Node node) Node nn = utils::mkConcat(children0, stype); Node ret = nm->mkNode(PLUS, - nm->mkNode(MINUS, node[2], new_len), + nm->mkNode(SUB, node[2], new_len), nm->mkNode(STRING_INDEXOF, nn, node[1], new_len)); return returnRewrite(node, ret, Rewrite::IDOF_STRIP_SYM_LEN); } @@ -3035,8 +3034,7 @@ Node SequencesRewriter::rewriteReplace(Node node) kind::STRING_SUBSTR, lastChild1[0], lastChild1[1], - nm->mkNode( - kind::PLUS, len0, one, nm->mkNode(kind::UMINUS, partLen1)))); + nm->mkNode(kind::PLUS, len0, one, nm->mkNode(kind::NEG, partLen1)))); Node res = nm->mkNode(kind::STRING_REPLACE, node[0], utils::mkConcat(children1, stype), @@ -3551,7 +3549,7 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n) } else { - val = NodeManager::currentNM()->mkNode(kind::MINUS, lent, lens); + val = NodeManager::currentNM()->mkNode(kind::SUB, lent, lens); } // Check if we can turn the prefix/suffix into equalities by showing that the diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 03c9f9375..a92fd3424 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -211,7 +211,7 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) // SK_ID_*_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) (str.len y))) id = SK_PREFIX; b = nm->mkNode( - MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkNode(STRING_LENGTH, b)); + SUB, nm->mkNode(STRING_LENGTH, a), nm->mkNode(STRING_LENGTH, b)); } else if (id == SK_ID_VC_SPT) { @@ -224,7 +224,7 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) // SK_ID_VC_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) 1)) id = SK_PREFIX; b = nm->mkNode( - MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkConstInt(Rational(1))); + SUB, nm->mkNode(STRING_LENGTH, a), nm->mkConstInt(Rational(1))); } else if (id == SK_ID_DC_SPT) { @@ -264,9 +264,9 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) bool isRev = (id == SK_ID_V_UNIFIED_SPT_REV); Node la = nm->mkNode(STRING_LENGTH, a); Node lb = nm->mkNode(STRING_LENGTH, b); - Node ta = isRev ? utils::mkPrefix(a, nm->mkNode(MINUS, la, lb)) + Node ta = isRev ? utils::mkPrefix(a, nm->mkNode(SUB, la, lb)) : utils::mkSuffix(a, lb); - Node tb = isRev ? utils::mkPrefix(b, nm->mkNode(MINUS, lb, la)) + Node tb = isRev ? utils::mkPrefix(b, nm->mkNode(SUB, lb, la)) : utils::mkSuffix(b, la); id = SK_PURIFY; // SK_ID_V_UNIFIED_SPT(x,y) ---> diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp index 952a1a36b..7491f510f 100644 --- a/src/theory/strings/strings_entail.cpp +++ b/src/theory/strings/strings_entail.cpp @@ -146,13 +146,13 @@ bool StringsEntail::stripSymbolicLength(std::vector& n1, Node s = n1[sindex_use]; size_t slen = Word::getLength(s); Node ncl = nm->mkConstInt(cvc5::Rational(slen)); - Node next_s = nm->mkNode(MINUS, lowerBound, ncl); + Node next_s = nm->mkNode(SUB, lowerBound, ncl); next_s = d_rr->rewrite(next_s); Assert(next_s.isConst()); // we can remove the entire constant if (next_s.getConst().sgn() >= 0) { - curr = d_rr->rewrite(nm->mkNode(MINUS, curr, ncl)); + curr = d_rr->rewrite(nm->mkNode(SUB, curr, ncl)); success = true; sindex++; } @@ -162,7 +162,7 @@ bool StringsEntail::stripSymbolicLength(std::vector& n1, // lower bound minus the length of a concrete string is negative, // hence lowerBound cannot be larger than long max Assert(lbr < Rational(String::maxSize())); - curr = d_rr->rewrite(nm->mkNode(MINUS, curr, lowerBound)); + curr = d_rr->rewrite(nm->mkNode(SUB, curr, lowerBound)); uint32_t lbsize = lbr.getNumerator().toUnsignedInt(); Assert(lbsize < slen); if (dir == 1) @@ -190,7 +190,7 @@ bool StringsEntail::stripSymbolicLength(std::vector& n1, else { Node next_s = NodeManager::currentNM()->mkNode( - MINUS, + SUB, curr, NodeManager::currentNM()->mkNode(STRING_LENGTH, n1[sindex_use])); next_s = d_rr->rewrite(next_s); diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 4c2319b4e..2667c1989 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -85,7 +85,7 @@ Node StringsPreprocess::reduce(Node t, // len(s) - n -m Node b13 = nm->mkNode( OR, - nm->mkNode(EQUAL, lsk2, nm->mkNode(MINUS, lt0, nm->mkNode(PLUS, n, m))), + nm->mkNode(EQUAL, lsk2, nm->mkNode(SUB, lt0, nm->mkNode(PLUS, n, m))), nm->mkNode(EQUAL, lsk2, zero)); // Length of the result is at most m Node b14 = nm->mkNode(LEQ, nm->mkNode(STRING_LENGTH, skt), m); @@ -139,7 +139,7 @@ Node StringsPreprocess::reduce(Node t, } else { - rs = nm->mkNode(STRING_SUBSTR, r, zero, nm->mkNode(MINUS, lens, n)); + rs = nm->mkNode(STRING_SUBSTR, r, zero, nm->mkNode(SUB, lens, n)); } Node rslen = nm->mkNode(STRING_LENGTH, rs); Node nsuf = nm->mkNode(PLUS, n, rslen); @@ -187,10 +187,8 @@ Node StringsPreprocess::reduce(Node t, Node negone = nm->mkConstInt(Rational(-1)); // substr( x, n, len( x ) - n ) - Node st = nm->mkNode(STRING_SUBSTR, - x, - n, - nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, x), n)); + Node st = nm->mkNode( + STRING_SUBSTR, x, n, nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, x), n)); Node io2 = sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_PRE, "iopre"); Node io4 = @@ -216,17 +214,16 @@ Node StringsPreprocess::reduce(Node t, Node c31 = st.eqNode(nm->mkNode(STRING_CONCAT, io2, y, io4)); // ~contains( str.++( io2, substr( y, 0, len( y ) - 1) ), y ) Node c32 = - nm->mkNode( - STRING_CONTAINS, - nm->mkNode( - STRING_CONCAT, - io2, - nm->mkNode( - STRING_SUBSTR, - y, - zero, - nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, y), one))), - y) + nm->mkNode(STRING_CONTAINS, + nm->mkNode( + STRING_CONCAT, + io2, + nm->mkNode( + STRING_SUBSTR, + y, + zero, + nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, y), one))), + y) .negate(); // skk = n + len( io2 ) Node c33 = skk.eqNode(nm->mkNode(PLUS, n, nm->mkNode(STRING_LENGTH, io2))); @@ -281,7 +278,7 @@ Node StringsPreprocess::reduce(Node t, nm->mkNode(GEQ, i, n), nm->mkNode(LT, i, nm->mkNode(ITE, retNegOne, sLen, skk)), nm->mkNode(GT, l, zero), - nm->mkNode(LEQ, l, nm->mkNode(MINUS, sLen, i)), + nm->mkNode(LEQ, l, nm->mkNode(SUB, sLen, i)), }); Node body = nm->mkNode( OR, @@ -293,10 +290,9 @@ Node StringsPreprocess::reduce(Node t, // ~in_re(substr(s, i, l), r) Node firstMatch = utils::mkForallInternal(bvl, body); Node bvll = nm->mkNode(BOUND_VAR_LIST, l); - Node validLen = - nm->mkNode(AND, - nm->mkNode(GEQ, l, zero), - nm->mkNode(LEQ, l, nm->mkNode(MINUS, sLen, skk))); + Node validLen = nm->mkNode(AND, + nm->mkNode(GEQ, l, zero), + nm->mkNode(LEQ, l, nm->mkNode(SUB, sLen, skk))); Node matchBody = nm->mkNode( AND, validLen, @@ -362,7 +358,7 @@ Node StringsPreprocess::reduce(Node t, Node ux = nm->mkNode(APPLY_UF, u, x); Node ux1 = nm->mkNode(APPLY_UF, u, xPlusOne); Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0"))); - Node c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0); + Node c = nm->mkNode(SUB, nm->mkNode(STRING_TO_CODE, sx), c0); Node ten = nm->mkConstInt(Rational(10)); Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux))); @@ -428,7 +424,7 @@ Node StringsPreprocess::reduce(Node t, Node kc2 = nm->mkNode(LT, k, lens); Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0"))); Node codeSk = nm->mkNode( - MINUS, + SUB, nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, s, k, one)), c0); Node ten = nm->mkConstInt(Rational(10)); @@ -458,7 +454,7 @@ Node StringsPreprocess::reduce(Node t, Node sx = nm->mkNode(STRING_SUBSTR, s, x, one); Node ux = nm->mkNode(APPLY_UF, u, x); Node ux1 = nm->mkNode(APPLY_UF, u, nm->mkNode(PLUS, x, one)); - Node c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0); + Node c = nm->mkNode(SUB, nm->mkNode(STRING_TO_CODE, sx), c0); Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux))); Node cb = nm->mkNode(AND, nm->mkNode(GEQ, c, zero), nm->mkNode(LT, c, ten)); @@ -518,7 +514,7 @@ Node StringsPreprocess::reduce(Node t, // length of first skolem is second argument Node b12 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n); Node lsk2 = nm->mkNode(STRING_LENGTH, sk2); - Node b13 = nm->mkNode(EQUAL, lsk2, nm->mkNode(MINUS, lt0, t12)); + Node b13 = nm->mkNode(EQUAL, lsk2, nm->mkNode(SUB, lt0, t12)); Node b1 = nm->mkNode(AND, b11, b12, b13); // nodes for the case where `seq.nth` is undefined. @@ -571,7 +567,7 @@ Node StringsPreprocess::reduce(Node t, nm->mkNode(kind::STRING_SUBSTR, y, zero, - nm->mkNode(kind::MINUS, + nm->mkNode(kind::SUB, nm->mkNode(kind::STRING_LENGTH, y), one))), y) @@ -634,11 +630,11 @@ Node StringsPreprocess::reduce(Node t, Node ufi = nm->mkNode(APPLY_UF, uf, i); Node ufip1 = nm->mkNode(APPLY_UF, uf, nm->mkNode(PLUS, i, one)); Node ii = nm->mkNode(STRING_INDEXOF, x, y, ufi); - Node cc = nm->mkNode( - STRING_CONCAT, - nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(MINUS, ii, ufi)), - z, - nm->mkNode(APPLY_UF, us, nm->mkNode(PLUS, i, one))); + Node cc = + nm->mkNode(STRING_CONCAT, + nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(SUB, ii, ufi)), + z, + nm->mkNode(APPLY_UF, us, nm->mkNode(PLUS, i, one))); std::vector flem; flem.push_back(ii.eqNode(negOne).negate()); @@ -782,7 +778,7 @@ Node StringsPreprocess::reduce(Node t, Node ufip1 = nm->mkNode(APPLY_UF, uf, ip1); Node ulip1 = nm->mkNode(APPLY_UF, ul, ip1); // ii = Uf(i + 1) - Ul(i + 1) - Node ii = nm->mkNode(MINUS, ufip1, ulip1); + Node ii = nm->mkNode(SUB, ufip1, ulip1); std::vector flem; // Ul(i + 1) > 0 @@ -805,8 +801,7 @@ Node StringsPreprocess::reduce(Node t, // forall l. 0 < l < Ul(i + 1) => // ~in_re(substr(x, Uf(i + 1) - Ul(i + 1), l), y') flem.push_back(utils::mkForallInternal(bvll, shortestMatchBody)); - Node pfxMatch = - nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(MINUS, ii, ufi)); + Node pfxMatch = nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(SUB, ii, ufi)); // Us(i) = substr(x, Uf(i), ii - Uf(i)) ++ z ++ Us(i + 1) flem.push_back( nm->mkNode(APPLY_UF, us, i) @@ -907,8 +902,8 @@ Node StringsPreprocess::reduce(Node t, Node i = SkolemCache::mkIndexVar(t); Node bvi = nm->mkNode(BOUND_VAR_LIST, i); - Node revi = nm->mkNode( - MINUS, nm->mkNode(STRING_LENGTH, x), nm->mkNode(PLUS, i, one)); + Node revi = + nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, x), nm->mkNode(PLUS, i, one)); Node ssr = nm->mkNode(STRING_SUBSTR, r, i, one); Node ssx = nm->mkNode(STRING_SUBSTR, x, revi, one); @@ -941,7 +936,7 @@ Node StringsPreprocess::reduce(Node t, NodeManager::currentNM()->mkNode( kind::LEQ, b1, - NodeManager::currentNM()->mkNode(kind::MINUS, lenx, lens)), + NodeManager::currentNM()->mkNode(kind::SUB, lenx, lens)), NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, b1, lens), diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index abac46d37..a65f98e7e 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -150,7 +150,7 @@ Node mkSuffix(Node t, Node n) { NodeManager* nm = NodeManager::currentNM(); return nm->mkNode( - STRING_SUBSTR, t, n, nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, t), n)); + STRING_SUBSTR, t, n, nm->mkNode(SUB, nm->mkNode(STRING_LENGTH, t), n)); } Node getConstantComponent(Node t) diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index 71ce2d3e8..623a38c81 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -401,8 +401,8 @@ TEST_F(TestNodeBlackNode, getKind) n = d_nodeManager->mkNode(PLUS, x, y); ASSERT_EQ(PLUS, n.getKind()); - n = d_nodeManager->mkNode(UMINUS, x); - ASSERT_EQ(UMINUS, n.getKind()); + n = d_nodeManager->mkNode(NEG, x); + ASSERT_EQ(NEG, n.getKind()); } TEST_F(TestNodeBlackNode, getOperator) @@ -513,7 +513,7 @@ TEST_F(TestNodeBlackNode, kinded_iterator) Node y = d_skolemManager->mkDummySkolem("y", integerType); Node z = d_skolemManager->mkDummySkolem("z", integerType); Node plus_x_y_z = d_nodeManager->mkNode(kind::PLUS, x, y, z); - Node x_minus_y = d_nodeManager->mkNode(kind::MINUS, x, y); + Node x_minus_y = d_nodeManager->mkNode(kind::SUB, x, y); { // iterator Node::kinded_iterator i = plus_x_y_z.begin(PLUS); diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp index 779397e04..d9be92249 100644 --- a/test/unit/node/node_builder_black.cpp +++ b/test/unit/node/node_builder_black.cpp @@ -313,7 +313,7 @@ TEST_F(TestNodeBlackNodeBuilder, append) Node p = d_nodeManager->mkNode( EQUAL, d_nodeManager->mkConst(CONST_RATIONAL, 0), - d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(UMINUS, s), t)); + d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(NEG, s), t)); Node q = d_nodeManager->mkNode(AND, x, z, d_nodeManager->mkNode(NOT, y)); #ifdef CVC5_ASSERTIONS diff --git a/test/unit/theory/arith_poly_white.cpp b/test/unit/theory/arith_poly_white.cpp index 9127fadff..989651aee 100644 --- a/test/unit/theory/arith_poly_white.cpp +++ b/test/unit/theory/arith_poly_white.cpp @@ -79,16 +79,16 @@ TEST_F(TestTheoryWhiteArithPolyNorm, check_poly_norm_int) t2 = d_nodeManager->mkNode(PLUS, {w, y, y, z, x}); ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); - t1 = d_nodeManager->mkNode(MINUS, t1, t2); + t1 = d_nodeManager->mkNode(SUB, t1, t2); t2 = zero; ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); - t1 = d_nodeManager->mkNode(UMINUS, d_nodeManager->mkNode(PLUS, x, y)); - t2 = d_nodeManager->mkNode(MINUS, zero, d_nodeManager->mkNode(PLUS, y, x)); + t1 = d_nodeManager->mkNode(NEG, d_nodeManager->mkNode(PLUS, x, y)); + t2 = d_nodeManager->mkNode(SUB, zero, d_nodeManager->mkNode(PLUS, y, x)); ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); - t1 = d_nodeManager->mkNode(MULT, d_nodeManager->mkNode(UMINUS, x), y); - t2 = d_nodeManager->mkNode(MULT, d_nodeManager->mkNode(UMINUS, y), x); + t1 = d_nodeManager->mkNode(MULT, d_nodeManager->mkNode(NEG, x), y); + t2 = d_nodeManager->mkNode(MULT, d_nodeManager->mkNode(NEG, y), x); ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); t1 = d_nodeManager->mkNode(MULT, x, d_nodeManager->mkNode(PLUS, y, z)); diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp index 8ce982291..71f6c240c 100644 --- a/test/unit/theory/sequences_rewriter_white.cpp +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -196,7 +196,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_with_with_assumption) // x + 5 < 6 |= 0 > x --> false ASSERT_TRUE(!ae.checkWithAssumption(x_plus_five_lt_six, zero, x, true)); - Node neg_x = d_nodeManager->mkNode(kind::UMINUS, x); + Node neg_x = d_nodeManager->mkNode(kind::NEG, x); Node x_plus_five_lt_five = d_rewriter->rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, five)); diff --git a/test/unit/theory/theory_arith_rewriter_black.cpp b/test/unit/theory/theory_arith_rewriter_black.cpp index 3fcd74356..b3746db15 100644 --- a/test/unit/theory/theory_arith_rewriter_black.cpp +++ b/test/unit/theory/theory_arith_rewriter_black.cpp @@ -58,7 +58,7 @@ TEST_F(TestTheoryArithRewriterBlack, RealAlgebraicNumber) { RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 3); Node n = d_nodeManager->mkRealAlgebraicNumber(sqrt2); - n = d_nodeManager->mkNode(Kind::MINUS, n, n); + n = d_nodeManager->mkNode(Kind::SUB, n, n); n = d_slvEngine->getRewriter()->rewrite(n); EXPECT_EQ(n.getKind(), Kind::CONST_RATIONAL); EXPECT_EQ(n.getConst(), Rational(0)); @@ -68,8 +68,8 @@ TEST_F(TestTheoryArithRewriterBlack, RealAlgebraicNumber) RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 2); Node m = d_nodeManager->mkRealAlgebraicNumber(msqrt2); Node n = d_nodeManager->mkRealAlgebraicNumber(sqrt2); - Node mm = d_nodeManager->mkNode(Kind::UMINUS, m); - Node mn = d_nodeManager->mkNode(Kind::UMINUS, n); + Node mm = d_nodeManager->mkNode(Kind::NEG, m); + Node mn = d_nodeManager->mkNode(Kind::NEG, n); mm = d_slvEngine->getRewriter()->rewrite(mm); mn = d_slvEngine->getRewriter()->rewrite(mn); EXPECT_EQ(-msqrt2, sqrt2); -- 2.30.2