From: Andrew Reynolds Date: Mon, 13 Dec 2021 22:42:38 +0000 (-0600) Subject: Distinguishing more uses of CONST_RATIONAL (#7802) X-Git-Tag: cvc5-1.0.0~673 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f66ed2f3f12b82c99f0dc8620acdd313b62b840e;p=cvc5.git Distinguishing more uses of CONST_RATIONAL (#7802) Towards eliminating subtyping Int/Real. --- diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 9bfb34cf7..af683ffc6 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -466,7 +466,7 @@ bool AletheProofPostprocessCallback::update(Node res, res, nm->mkNode(kind::SEXPR, d_cl, res), children, - {nm->mkConst(CONST_RATIONAL, Rational(1))}, + {nm->mkConstInt(Rational(1))}, *cdp); } default: @@ -1352,7 +1352,7 @@ bool AletheProofPostprocessCallback::update(Node res, { Node vp1 = nm->mkNode(kind::SEXPR, d_cl, children[0], res); std::vector new_children = {vp1, children[0]}; - new_args.push_back(nm->mkConst(CONST_RATIONAL, 1)); + new_args.push_back(nm->mkConstInt(Rational(1))); return addAletheStep(AletheRule::LA_GENERIC, vp1, vp1, {}, new_args, *cdp) && addAletheStep(AletheRule::RESOLUTION, res, @@ -1375,7 +1375,7 @@ bool AletheProofPostprocessCallback::update(Node res, { Node vp1 = nm->mkNode(kind::SEXPR, d_cl, children[0], res); std::vector new_children = {vp1, children[0]}; - new_args.push_back(nm->mkConst(CONST_RATIONAL, 1)); + new_args.push_back(nm->mkConstInt(Rational(1))); return addAletheStep(AletheRule::LA_GENERIC, vp1, vp1, {}, new_args, *cdp) && addAletheStep(AletheRule::RESOLUTION, res, @@ -1874,10 +1874,7 @@ bool AletheProofPostprocessCallback::finalStep( if (id != PfRule::ALETHE_RULE) { std::vector sanitized_args{ - res, - res, - nm->mkConst(CONST_RATIONAL, - static_cast(AletheRule::ASSUME))}; + res, res, nm->mkConstInt(static_cast(AletheRule::ASSUME))}; for (const Node& arg : args) { sanitized_args.push_back(d_anc.convert(arg)); @@ -1940,8 +1937,8 @@ bool AletheProofPostprocessCallback::addAletheStep( } std::vector new_args = std::vector(); - new_args.push_back(NodeManager::currentNM()->mkConst( - CONST_RATIONAL, Rational(static_cast(rule)))); + new_args.push_back(NodeManager::currentNM()->mkConstInt( + Rational(static_cast(rule)))); new_args.push_back(res); new_args.push_back(sanitized_conclusion); new_args.insert(new_args.end(), args.begin(), args.end()); diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index 06d6aeaab..32b630fa8 100644 --- a/src/theory/arith/nl/ext/factoring_check.cpp +++ b/src/theory/arith/nl/ext/factoring_check.cpp @@ -35,7 +35,6 @@ namespace nl { FactoringCheck::FactoringCheck(Env& env, ExtState* data) : EnvObj(env), d_data(data) { - d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1)); } @@ -155,7 +154,8 @@ void FactoringCheck::check(const std::vector& asserts, poly.size() == 1 ? poly[0] : nm->mkNode(Kind::PLUS, poly); Trace("nl-ext-factor") << "...factored polynomial : " << polyn << std::endl; - Node conc_lit = nm->mkNode(atom.getKind(), polyn, d_zero); + Node zero = nm->mkConstRealOrInt(polyn.getType(), Rational(0)); + Node conc_lit = nm->mkNode(atom.getKind(), polyn, zero); conc_lit = rewrite(conc_lit); if (!polarity) { diff --git a/src/theory/arith/nl/pow2_solver.cpp b/src/theory/arith/nl/pow2_solver.cpp index 4752d45ff..59bf89151 100644 --- a/src/theory/arith/nl/pow2_solver.cpp +++ b/src/theory/arith/nl/pow2_solver.cpp @@ -42,9 +42,9 @@ Pow2Solver::Pow2Solver(Env& env, NodeManager* nm = NodeManager::currentNM(); d_false = nm->mkConst(false); d_true = nm->mkConst(true); - d_zero = nm->mkConst(CONST_RATIONAL, Rational(0)); - d_one = nm->mkConst(CONST_RATIONAL, Rational(1)); - d_two = nm->mkConst(CONST_RATIONAL, Rational(2)); + d_zero = nm->mkConstInt(Rational(0)); + d_one = nm->mkConstInt(Rational(1)); + d_two = nm->mkConstInt(Rational(2)); } Pow2Solver::~Pow2Solver() {} diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index c4f7f6ca9..77e5f9f3f 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -230,7 +230,7 @@ void ExponentialSolver::doTangentLemma(TNode e, proof->addStep(lem, PfRule::ARITH_TRANS_EXP_APPROX_BELOW, {}, - {nm->mkConst(CONST_RATIONAL, Rational(d)), e[0]}); + {nm->mkConstInt(Rational(d)), e[0]}); } d_data->d_im.addPendingLemma( lem, InferenceId::ARITH_NL_T_TANGENT, proof, true); diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp index dc55632f4..3bf1ace98 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.cpp +++ b/src/theory/arith/nl/transcendental/proof_checker.cpp @@ -83,11 +83,11 @@ Node TranscendentalProofRuleChecker::checkInternal( PfRule id, const std::vector& children, const std::vector& args) { NodeManager* nm = NodeManager::currentNM(); - auto zero = nm->mkConst(CONST_RATIONAL, 0); - auto one = nm->mkConst(CONST_RATIONAL, 1); - auto mone = nm->mkConst(CONST_RATIONAL, -1); - auto pi = nm->mkNullaryOperator(nm->realType(), Kind::PI); - auto mpi = nm->mkNode(Kind::MULT, mone, pi); + Node zero = nm->mkConstReal(Rational(0)); + Node one = nm->mkConstReal(Rational(1)); + Node mone = nm->mkConstReal(Rational(-1)); + Node pi = nm->mkNullaryOperator(nm->realType(), Kind::PI); + Node mpi = nm->mkNode(Kind::MULT, mone, pi); Trace("nl-trans-checker") << "Checking " << id << std::endl; Trace("nl-trans-checker") << "Children:" << std::endl; for (const auto& c : children) @@ -141,11 +141,10 @@ Node TranscendentalProofRuleChecker::checkInternal( { Assert(children.empty()); Assert(args.size() == 4); - Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL - && args[0].getConst().isIntegral()); + Assert(args[0].isConst() && args[0].getType().isInteger()); Assert(args[1].getType().isReal()); - Assert(args[2].isConst() && args[2].getKind() == Kind::CONST_RATIONAL); - Assert(args[3].isConst() && args[3].getKind() == Kind::CONST_RATIONAL); + Assert(args[2].isConst() && args[2].getType().isRealOrInt()); + Assert(args[3].isConst() && args[3].getType().isRealOrInt()); std::uint64_t d = args[0].getConst().getNumerator().toUnsignedInt(); Node t = args[1]; @@ -168,11 +167,10 @@ Node TranscendentalProofRuleChecker::checkInternal( { Assert(children.empty()); Assert(args.size() == 4); - Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL - && args[0].getConst().isIntegral()); + Assert(args[0].isConst() && args[0].getType().isInteger()); Assert(args[1].getType().isReal()); - Assert(args[2].isConst() && args[2].getKind() == Kind::CONST_RATIONAL); - Assert(args[3].isConst() && args[3].getKind() == Kind::CONST_RATIONAL); + Assert(args[2].isConst() && args[2].getType().isRealOrInt()); + Assert(args[3].isConst() && args[3].getType().isRealOrInt()); std::uint64_t d = args[0].getConst().getNumerator().toUnsignedInt(); Node t = args[1]; @@ -195,8 +193,7 @@ Node TranscendentalProofRuleChecker::checkInternal( { Assert(children.empty()); Assert(args.size() == 2); - Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL - && args[0].getConst().isIntegral()); + Assert(args[0].isConst() && args[0].getType().isInteger()); Assert(args[1].getType().isReal()); std::uint64_t d = args[0].getConst().getNumerator().toUnsignedInt(); @@ -238,10 +235,7 @@ Node TranscendentalProofRuleChecker::checkInternal( x.eqNode( nm->mkNode(Kind::PLUS, y, - nm->mkNode(Kind::MULT, - nm->mkConst(CONST_RATIONAL, 2), - s, - pi)))), + nm->mkNode(Kind::MULT, nm->mkConstReal(2), s, pi)))), nm->mkNode(Kind::SINE, y).eqNode(nm->mkNode(Kind::SINE, x))}); } else if (id == PfRule::ARITH_TRANS_SINE_SYMMETRY) @@ -286,13 +280,12 @@ Node TranscendentalProofRuleChecker::checkInternal( { Assert(children.empty()); Assert(args.size() == 6); - Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL - && args[0].getConst().isIntegral()); + Assert(args[0].isConst() && args[0].getType().isInteger()); Assert(args[1].getType().isReal()); Assert(args[2].getType().isReal()); Assert(args[3].getType().isReal()); - Assert(args[4].isConst() && args[4].getKind() == Kind::CONST_RATIONAL); - Assert(args[5].isConst() && args[5].getKind() == Kind::CONST_RATIONAL); + Assert(args[4].isConst() && args[4].getType().isRealOrInt()); + Assert(args[5].isConst() && args[5].getType().isRealOrInt()); std::uint64_t d = args[0].getConst().getNumerator().toUnsignedInt(); Node t = args[1]; @@ -317,8 +310,7 @@ Node TranscendentalProofRuleChecker::checkInternal( { Assert(children.empty()); Assert(args.size() == 5); - Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL - && args[0].getConst().isIntegral()); + Assert(args[0].isConst() && args[0].getType().isInteger()); Assert(args[1].getType().isReal()); Assert(args[2].getType().isReal()); Assert(args[3].getType().isReal()); @@ -341,13 +333,12 @@ Node TranscendentalProofRuleChecker::checkInternal( { Assert(children.empty()); Assert(args.size() == 6); - Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL - && args[0].getConst().isIntegral()); + Assert(args[0].isConst() && args[0].getType().isInteger()); Assert(args[1].getType().isReal()); Assert(args[2].getType().isReal()); Assert(args[3].getType().isReal()); - Assert(args[4].isConst() && args[4].getKind() == Kind::CONST_RATIONAL); - Assert(args[5].isConst() && args[5].getKind() == Kind::CONST_RATIONAL); + Assert(args[4].isConst() && args[4].getType().isRealOrInt()); + Assert(args[5].isConst() && args[5].getType().isRealOrInt()); std::uint64_t d = args[0].getConst().getNumerator().toUnsignedInt(); Node t = args[1]; @@ -372,8 +363,7 @@ Node TranscendentalProofRuleChecker::checkInternal( { Assert(children.empty()); Assert(args.size() == 5); - Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL - && args[0].getConst().isIntegral()); + Assert(args[0].isConst() && args[0].getType().isInteger()); Assert(args[1].getType().isReal()); Assert(args[2].getType().isReal()); Assert(args[3].getType().isReal()); diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 338e37baa..6c1bec647 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -75,13 +75,12 @@ void SineSolver::doPhaseShift(TNode a, TNode new_a, TNode y) nm->mkNode(Kind::ITE, mkValidPhase(a[0], d_data->d_pi), a[0].eqNode(y), - a[0].eqNode(nm->mkNode( - Kind::PLUS, - y, - nm->mkNode(Kind::MULT, - nm->mkConst(CONST_RATIONAL, Rational(2)), - shift, - d_data->d_pi)))), + a[0].eqNode(nm->mkNode(Kind::PLUS, + y, + nm->mkNode(Kind::MULT, + nm->mkConstReal(Rational(2)), + shift, + d_data->d_pi)))), new_a.eqNode(a)); CDProof* proof = nullptr; if (d_data->isProofEnabled()) @@ -409,7 +408,7 @@ void SineSolver::doTangentLemma( proof->addStep(lem, PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG, {}, - {nm->mkConst(CONST_RATIONAL, Rational(2 * d)), + {nm->mkConstInt(Rational(2 * d)), e[0], c, regionToLowerBound(region), @@ -420,7 +419,7 @@ void SineSolver::doTangentLemma( proof->addStep(lem, PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG, {}, - {nm->mkConst(CONST_RATIONAL, Rational(2 * d)), + {nm->mkConstInt(Rational(2 * d)), e[0], c, c, @@ -434,7 +433,7 @@ void SineSolver::doTangentLemma( proof->addStep(lem, PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS, {}, - {nm->mkConst(CONST_RATIONAL, Rational(2 * d)), + {nm->mkConstInt(Rational(2 * d)), e[0], c, regionToLowerBound(region), @@ -445,7 +444,7 @@ void SineSolver::doTangentLemma( proof->addStep(lem, PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS, {}, - {nm->mkConst(CONST_RATIONAL, Rational(2 * d)), + {nm->mkConstInt(Rational(2 * d)), e[0], c, c, diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp index 898d81c27..c9e0015e2 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.cpp +++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp @@ -51,7 +51,7 @@ std::pair TaylorGenerator::getTaylor(Kind k, std::uint64_t n) // the current factorial `counter!` Integer factorial = 1; // the current variable power `x^counter` - Node varpow = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node varpow = nm->mkConstReal(Rational(1)); std::vector sum; for (std::uint64_t counter = 1; counter <= n; ++counter) { @@ -60,9 +60,7 @@ std::pair TaylorGenerator::getTaylor(Kind k, std::uint64_t n) // Maclaurin series for exponential: // \sum_{n=0}^\infty x^n / n! sum.push_back( - nm->mkNode(Kind::DIVISION, - varpow, - nm->mkConst(CONST_RATIONAL, factorial))); + nm->mkNode(Kind::DIVISION, varpow, nm->mkConstReal(factorial))); } else if (k == Kind::SINE) { @@ -71,20 +69,19 @@ std::pair TaylorGenerator::getTaylor(Kind k, std::uint64_t n) if (counter % 2 == 0) { int sign = (counter % 4 == 0 ? -1 : 1); - sum.push_back(nm->mkNode( - Kind::MULT, - nm->mkNode(Kind::DIVISION, - nm->mkConst(CONST_RATIONAL, sign), - nm->mkConst(CONST_RATIONAL, factorial)), - varpow)); + sum.push_back(nm->mkNode(Kind::MULT, + nm->mkNode(Kind::DIVISION, + nm->mkConstReal(sign), + nm->mkConstReal(factorial)), + varpow)); } } factorial *= counter; varpow = nm->mkNode(Kind::MULT, d_taylor_real_fv, varpow); } Node taylor_sum = (sum.size() == 1 ? sum[0] : nm->mkNode(Kind::PLUS, sum)); - Node taylor_rem = nm->mkNode( - Kind::DIVISION, varpow, nm->mkConst(CONST_RATIONAL, factorial)); + Node taylor_rem = + nm->mkNode(Kind::DIVISION, varpow, nm->mkConstReal(factorial)); auto res = std::make_pair(taylor_sum, taylor_rem); @@ -116,10 +113,10 @@ void TaylorGenerator::getPolynomialApproximationBounds( { pbounds.d_lower = taylor_sum; pbounds.d_upperNeg = nm->mkNode(Kind::PLUS, taylor_sum, ru); - pbounds.d_upperPos = nm->mkNode( - Kind::MULT, - taylor_sum, - nm->mkNode(Kind::PLUS, nm->mkConst(CONST_RATIONAL, Rational(1)), ru)); + pbounds.d_upperPos = + nm->mkNode(Kind::MULT, + taylor_sum, + nm->mkNode(Kind::PLUS, nm->mkConstReal(Rational(1)), ru)); } else { @@ -201,11 +198,11 @@ std::pair TaylorGenerator::getTfModelBounds(Node tf, // at zero, its trivial if (k == Kind::SINE) { - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); + Node zero = nm->mkConstReal(Rational(0)); return std::pair(zero, zero); } Assert(k == Kind::EXPONENTIAL); - Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node one = nm->mkConstReal(Rational(1)); return std::pair(one, one); } bool isNeg = csign == -1; diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index 7c2f1a058..e32f336ac 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -37,9 +37,9 @@ TranscendentalState::TranscendentalState(Env& env, { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); - d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); - d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1)); - d_neg_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(-1)); + d_zero = NodeManager::currentNM()->mkConstReal(Rational(0)); + d_one = NodeManager::currentNM()->mkConstReal(Rational(1)); + d_neg_one = NodeManager::currentNM()->mkConstReal(Rational(-1)); if (d_env.isTheoryProofProducing()) { d_proof.reset(new CDProofSet( @@ -204,21 +204,15 @@ void TranscendentalState::mkPi() if (d_pi.isNull()) { d_pi = nm->mkNullaryOperator(nm->realType(), Kind::PI); - d_pi_2 = rewrite( - nm->mkNode(Kind::MULT, - d_pi, - nm->mkConst(CONST_RATIONAL, Rational(1) / Rational(2)))); - d_pi_neg_2 = rewrite( - nm->mkNode(Kind::MULT, - d_pi, - nm->mkConst(CONST_RATIONAL, Rational(-1) / Rational(2)))); - d_pi_neg = rewrite(nm->mkNode( - Kind::MULT, d_pi, nm->mkConst(CONST_RATIONAL, Rational(-1)))); + d_pi_2 = rewrite(nm->mkNode( + Kind::MULT, d_pi, nm->mkConstReal(Rational(1) / Rational(2)))); + d_pi_neg_2 = rewrite(nm->mkNode( + Kind::MULT, d_pi, nm->mkConstReal(Rational(-1) / Rational(2)))); + d_pi_neg = + rewrite(nm->mkNode(Kind::MULT, d_pi, nm->mkConstReal(Rational(-1)))); // initialize bounds - d_pi_bound[0] = - nm->mkConst(CONST_RATIONAL, Rational(103993) / Rational(33102)); - d_pi_bound[1] = - nm->mkConst(CONST_RATIONAL, Rational(104348) / Rational(33215)); + d_pi_bound[0] = nm->mkConstReal(Rational(103993) / Rational(33102)); + d_pi_bound[1] = nm->mkConstReal(Rational(104348) / Rational(33215)); } } @@ -344,44 +338,34 @@ NlLemma TranscendentalState::mkSecantLemma(TNode lower, proof->addStep(lem, PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS, {}, - {nm->mkConst(CONST_RATIONAL, 2 * actual_d), - tf[0], - lower, - upper}); + {nm->mkConstInt(2 * actual_d), tf[0], lower, upper}); } else { proof->addStep(lem, PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG, {}, - {nm->mkConst(CONST_RATIONAL, 2 * actual_d), - tf[0], - lower, - upper}); + {nm->mkConstInt(2 * actual_d), tf[0], lower, upper}); } } else if (tf.getKind() == Kind::SINE) { if (convexity == Convexity::CONCAVE) { - proof->addStep(lem, - PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS, - {}, - {nm->mkConst(CONST_RATIONAL, 2 * actual_d), - tf[0], - lower, - upper, - lapprox, - uapprox + proof->addStep( + lem, + PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS, + {}, + {nm->mkConstInt(2 * actual_d), tf[0], lower, upper, lapprox, uapprox - }); + }); } else { proof->addStep(lem, PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG, {}, - {nm->mkConst(CONST_RATIONAL, 2 * actual_d), + {nm->mkConstInt(2 * actual_d), tf[0], lower, upper, diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index 17efa53a5..99f5621d6 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -173,22 +173,20 @@ Node OperatorElim::eliminateOperators(Node node, nm->mkNode( MULT, den, - nm->mkNode( - PLUS, v, nm->mkConst(CONST_RATIONAL, Rational(1)))))); + nm->mkNode(PLUS, v, nm->mkConstInt(Rational(1)))))); } else { lem = nm->mkNode( AND, leqNum, - nm->mkNode(LT, - num, - nm->mkNode(MULT, - den, - nm->mkNode(PLUS, - v, - nm->mkConst(CONST_RATIONAL, - Rational(-1)))))); + nm->mkNode( + LT, + num, + nm->mkNode( + MULT, + den, + nm->mkNode(PLUS, v, nm->mkConstInt(Rational(-1)))))); } } else @@ -198,34 +196,32 @@ Node OperatorElim::eliminateOperators(Node node, AND, nm->mkNode( IMPLIES, - nm->mkNode(GT, den, nm->mkConst(CONST_RATIONAL, Rational(0))), + nm->mkNode(GT, den, nm->mkConstInt(Rational(0))), nm->mkNode( AND, leqNum, nm->mkNode( LT, num, - nm->mkNode(MULT, - den, - nm->mkNode(PLUS, - v, - nm->mkConst(CONST_RATIONAL, - Rational(1))))))), + nm->mkNode( + MULT, + den, + nm->mkNode( + PLUS, v, nm->mkConstInt(Rational(1))))))), nm->mkNode( IMPLIES, - nm->mkNode(LT, den, nm->mkConst(CONST_RATIONAL, Rational(0))), + nm->mkNode(LT, den, nm->mkConstInt(Rational(0))), nm->mkNode( AND, leqNum, nm->mkNode( LT, num, - nm->mkNode(MULT, - den, - nm->mkNode(PLUS, - v, - nm->mkConst(CONST_RATIONAL, - Rational(-1)))))))); + nm->mkNode( + MULT, + den, + nm->mkNode( + PLUS, v, nm->mkConstInt(Rational(-1)))))))); } Node intVar = mkWitnessTerm( v, lem, "linearIntDiv", "the result of an intdiv-by-k term", lems); @@ -259,10 +255,9 @@ Node OperatorElim::eliminateOperators(Node node, checkNonLinearLogic(node); Node rw = nm->mkNode(k, num, den); Node v = bvm->mkBoundVar(rw, nm->realType()); - Node lem = nm->mkNode( - IMPLIES, - den.eqNode(nm->mkConst(CONST_RATIONAL, Rational(0))).negate(), - nm->mkNode(MULT, den, v).eqNode(num)); + Node lem = nm->mkNode(IMPLIES, + den.eqNode(nm->mkConstReal(Rational(0))).negate(), + nm->mkNode(MULT, den, v).eqNode(num)); return mkWitnessTerm( v, lem, "nonlinearDiv", "the result of a non-linear div term", lems); break; @@ -276,8 +271,7 @@ Node OperatorElim::eliminateOperators(Node node, { checkNonLinearLogic(node); Node divByZeroNum = getArithSkolemApp(num, SkolemFunId::DIV_BY_ZERO); - Node denEq0 = - nm->mkNode(EQUAL, den, nm->mkConst(CONST_RATIONAL, Rational(0))); + Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConstReal(Rational(0))); ret = nm->mkNode(ITE, denEq0, divByZeroNum, ret); } return ret; @@ -295,8 +289,7 @@ Node OperatorElim::eliminateOperators(Node node, checkNonLinearLogic(node); Node intDivByZeroNum = getArithSkolemApp(num, SkolemFunId::INT_DIV_BY_ZERO); - Node denEq0 = - nm->mkNode(EQUAL, den, nm->mkConst(CONST_RATIONAL, Rational(0))); + Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConstInt(Rational(0))); ret = nm->mkNode(ITE, denEq0, intDivByZeroNum, ret); } return ret; @@ -313,8 +306,7 @@ Node OperatorElim::eliminateOperators(Node node, { checkNonLinearLogic(node); Node modZeroNum = getArithSkolemApp(num, SkolemFunId::MOD_BY_ZERO); - Node denEq0 = - nm->mkNode(EQUAL, den, nm->mkConst(CONST_RATIONAL, Rational(0))); + Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConstInt(Rational(0))); ret = nm->mkNode(ITE, denEq0, modZeroNum, ret); } return ret; @@ -325,7 +317,9 @@ Node OperatorElim::eliminateOperators(Node node, { return nm->mkNode( ITE, - nm->mkNode(LT, node[0], nm->mkConst(CONST_RATIONAL, Rational(0))), + nm->mkNode(LT, + node[0], + nm->mkConstRealOrInt(node[0].getType(), Rational(0))), nm->mkNode(UMINUS, node[0]), node[0]); break; @@ -363,11 +357,10 @@ Node OperatorElim::eliminateOperators(Node node, // satisfiable. On the original formula, this would require that we // simultaneously interpret sqrt(1) as 1 and -1, which is not a valid // model. - lem = nm->mkNode( - ITE, - nm->mkNode(GEQ, node[0], nm->mkConst(CONST_RATIONAL, Rational(0))), - nonNeg, - uf); + lem = nm->mkNode(ITE, + nm->mkNode(GEQ, node[0], nm->mkConstReal(Rational(0))), + nonNeg, + uf); } else { @@ -377,10 +370,9 @@ Node OperatorElim::eliminateOperators(Node node, Node rlem; if (k == ARCSINE || k == ARCTANGENT || k == ARCCOSECANT) { - Node half = nm->mkConst(CONST_RATIONAL, Rational(1) / Rational(2)); + Node half = nm->mkConstReal(Rational(1) / Rational(2)); Node pi2 = nm->mkNode(MULT, half, pi); - Node npi2 = - nm->mkNode(MULT, nm->mkConst(CONST_RATIONAL, Rational(-1)), pi2); + Node npi2 = nm->mkNode(MULT, nm->mkConstReal(Rational(-1)), pi2); // -pi/2 < var <= pi/2 rlem = nm->mkNode( AND, nm->mkNode(LT, npi2, var), nm->mkNode(LEQ, var, pi2)); @@ -388,10 +380,9 @@ Node OperatorElim::eliminateOperators(Node node, else { // 0 <= var < pi - rlem = nm->mkNode( - AND, - nm->mkNode(LEQ, nm->mkConst(CONST_RATIONAL, Rational(0)), var), - nm->mkNode(LT, var, pi)); + rlem = nm->mkNode(AND, + nm->mkNode(LEQ, nm->mkConstReal(Rational(0)), var), + nm->mkNode(LT, var, pi)); } Kind rk = diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp index 69fe98734..c05f6ae0a 100644 --- a/src/theory/arith/proof_checker.cpp +++ b/src/theory/arith/proof_checker.cpp @@ -49,7 +49,6 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, const std::vector& args) { NodeManager* nm = NodeManager::currentNM(); - auto zero = nm->mkConst(CONST_RATIONAL, 0); if (Debug.isOn("arith::pf::check")) { Debug("arith::pf::check") << "Arith PfRule:" << id << std::endl; @@ -76,6 +75,7 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, || rel == Kind::LEQ || rel == Kind::GT || rel == Kind::GEQ); Node lhs = args[1][0]; Node rhs = args[1][1]; + Node zero = nm->mkConstRealOrInt(mult.getType(), Rational(0)); return nm->mkNode(Kind::IMPLIES, nm->mkAnd(std::vector{ nm->mkNode(Kind::GT, mult, zero), args[1]}), @@ -94,6 +94,7 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, Kind rel_inv = (rel == Kind::DISTINCT ? rel : reverseRelationKind(rel)); Node lhs = args[1][0]; Node rhs = args[1][1]; + Node zero = nm->mkConstRealOrInt(mult.getType(), Rational(0)); return nm->mkNode(Kind::IMPLIES, nm->mkAnd(std::vector{ nm->mkNode(Kind::LT, mult, zero), args[1]}), @@ -243,12 +244,8 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, << "Bad kind: " << children[i].getKind() << std::endl; } } - leftSum << nm->mkNode(Kind::MULT, - nm->mkConst(CONST_RATIONAL, scalar), - children[i][0]); - rightSum << nm->mkNode(Kind::MULT, - nm->mkConst(CONST_RATIONAL, scalar), - children[i][1]); + leftSum << nm->mkNode(Kind::MULT, args[i], children[i][0]); + rightSum << nm->mkNode(Kind::MULT, args[i], children[i][1]); } Node r = nm->mkNode(strict ? Kind::LT : Kind::LEQ, leftSum.constructNode(), @@ -265,8 +262,7 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, if (children.size() != 1 || (children[0].getKind() != Kind::GT && children[0].getKind() != Kind::GEQ) - || !children[0][0].getType().isInteger() - || children[0][1].getKind() != Kind::CONST_RATIONAL) + || !children[0][0].getType().isInteger() || !children[0][1].isConst()) { Debug("arith::pf::check") << "Illformed input: " << children; return Node::null(); @@ -275,7 +271,7 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, { Rational originalBound = children[0][1].getConst(); Rational newBound = leastIntGreaterThan(originalBound); - Node rational = nm->mkConst(CONST_RATIONAL, newBound); + Node rational = nm->mkConstInt(newBound); return nm->mkNode(kind::GEQ, children[0][0], rational); } } @@ -290,8 +286,7 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, if (children.size() != 1 || (children[0].getKind() != Kind::LT && children[0].getKind() != Kind::LEQ) - || !children[0][0].getType().isInteger() - || children[0][1].getKind() != Kind::CONST_RATIONAL) + || !children[0][0].getType().isInteger() || !children[0][1].isConst()) { Debug("arith::pf::check") << "Illformed input: " << children; return Node::null(); @@ -300,7 +295,7 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, { Rational originalBound = children[0][1].getConst(); Rational newBound = greatestIntLessThan(originalBound); - Node rational = nm->mkConst(CONST_RATIONAL, newBound); + Node rational = nm->mkConstInt(newBound); return nm->mkNode(kind::LEQ, children[0][0], rational); } } diff --git a/src/theory/bags/bag_reduction.cpp b/src/theory/bags/bag_reduction.cpp index 6e1b4c1a5..3e6544882 100644 --- a/src/theory/bags/bag_reduction.cpp +++ b/src/theory/bags/bag_reduction.cpp @@ -65,8 +65,8 @@ Node BagReduction::reduceFoldOperator(Node node, std::vector& asserts) Node f = node[0]; Node t = node[1]; Node A = node[2]; - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); - Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node zero = nm->mkConstInt(Rational(0)); + Node one = nm->mkConstInt(Rational(1)); // types TypeNode bagType = A.getType(); TypeNode elementType = A.getType().getBagElementType(); diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp index 71ce13c69..58c12ceff 100644 --- a/src/theory/bv/int_blaster.cpp +++ b/src/theory/bv/int_blaster.cpp @@ -591,7 +591,7 @@ Node IntBlaster::uts(Node x, uint64_t bvsize) { Node powNode = pow2(bvsize - 1); Node modNode = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, x, powNode); - Node two = d_nm->mkConst(CONST_RATIONAL, Rational(2)); + Node two = d_nm->mkConstInt(Rational(2)); Node twoTimesNode = d_nm->mkNode(kind::MULT, two, modNode); return d_nm->mkNode(kind::MINUS, twoTimesNode, x); } @@ -618,7 +618,7 @@ Node IntBlaster::createSignExtendNode(Node x, uint64_t bvsize, uint64_t amount) Rational max_of_amount = intpow2(amount) - 1; Rational mul = max_of_amount * intpow2(bvsize); Rational sum = mul + c; - returnNode = d_nm->mkConst(CONST_RATIONAL, sum); + returnNode = d_nm->mkConstInt(sum); } } else @@ -630,7 +630,7 @@ Node IntBlaster::createSignExtendNode(Node x, uint64_t bvsize, uint64_t amount) else { Rational twoToKMinusOne(intpow2(bvsize - 1)); - Node minSigned = d_nm->mkConst(CONST_RATIONAL, twoToKMinusOne); + Node minSigned = d_nm->mkConstInt(twoToKMinusOne); /* condition checks whether the msb is 1. * This holds when the integer value is smaller than * 100...0, which is 2^{bvsize-1}. @@ -899,9 +899,7 @@ Node IntBlaster::createShiftNode(std::vector children, ite = d_nm->mkNode( kind::ITE, d_nm->mkNode( - kind::EQUAL, - y, - d_nm->mkConst(CONST_RATIONAL, Rational(Integer(i), Integer(1)))), + kind::EQUAL, y, d_nm->mkConstInt(Rational(Integer(i), Integer(1)))), body, ite); } diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp index 4c4540366..aa69f9ecf 100644 --- a/src/theory/strings/regexp_entail.cpp +++ b/src/theory/strings/regexp_entail.cpp @@ -30,8 +30,8 @@ namespace strings { RegExpEntail::RegExpEntail(Rewriter* r) : d_rewriter(r), d_aent(r) { - d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); - d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1)); + d_zero = NodeManager::currentNM()->mkConstInt(Rational(0)); + d_one = NodeManager::currentNM()->mkConstInt(Rational(1)); } Node RegExpEntail::simpleRegexpConsume(std::vector& mchildren, @@ -749,7 +749,7 @@ Node RegExpEntail::getConstantBoundLengthForRegexp(TNode n, bool isLower) const continue; } } - Assert(bc.getKind() == CONST_RATIONAL); + Assert(bc.isConst() && bc.getType().isInteger()); Rational r = bc.getConst(); if (k == REGEXP_CONCAT) { @@ -772,7 +772,7 @@ Node RegExpEntail::getConstantBoundLengthForRegexp(TNode n, bool isLower) const // if we were successful and didn't ignore all components if (success && !firstTime) { - ret = nm->mkConst(CONST_RATIONAL, rr); + ret = nm->mkConstInt(rr); } } if (ret.isNull() && isLower)