From 7ae818d54bedc96b6fb0000fa17f41ee30f1f8a0 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 29 Apr 2022 13:30:07 -0700 Subject: [PATCH] Replace mkConst(CONST_RATIONAL) by mkConstReal (#8686) This PR removes the usages of CONST_RATIONAL in the nonlinear arithmetic solver. --- src/theory/arith/nl/coverings/cdcac.cpp | 2 +- .../arith/nl/coverings/proof_generator.cpp | 4 +- src/theory/arith/nl/ext/ext_state.cpp | 6 +- src/theory/arith/nl/ext/factoring_check.cpp | 2 +- src/theory/arith/nl/ext/monomial.cpp | 2 +- .../arith/nl/ext/monomial_bounds_check.cpp | 4 +- src/theory/arith/nl/ext/proof_checker.cpp | 3 +- .../arith/nl/ext/tangent_plane_check.cpp | 19 ++- src/theory/arith/nl/nl_model.cpp | 6 +- src/theory/arith/nl/nonlinear_extension.cpp | 6 +- src/theory/arith/nl/poly_conversion.cpp | 149 ++++++++---------- 11 files changed, 91 insertions(+), 112 deletions(-) diff --git a/src/theory/arith/nl/coverings/cdcac.cpp b/src/theory/arith/nl/coverings/cdcac.cpp index d358a34ef..24171c8a3 100644 --- a/src/theory/arith/nl/coverings/cdcac.cpp +++ b/src/theory/arith/nl/coverings/cdcac.cpp @@ -269,7 +269,7 @@ PolyVector requiredCoefficientsLazardModified( // construct phi := (and (= p_i 0)) with p_i the coefficients of p std::vector conditions; - auto zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); + auto zero = NodeManager::currentNM()->mkConstReal(Rational(0)); for (const auto& coeff : poly::coefficients(p)) { conditions.emplace_back(NodeManager::currentNM()->mkNode( diff --git a/src/theory/arith/nl/coverings/proof_generator.cpp b/src/theory/arith/nl/coverings/proof_generator.cpp index 6d394c52d..4ffd88fa6 100644 --- a/src/theory/arith/nl/coverings/proof_generator.cpp +++ b/src/theory/arith/nl/coverings/proof_generator.cpp @@ -95,8 +95,8 @@ CoveringsProofGenerator::CoveringsProofGenerator(context::Context* ctx, ProofNodeManager* pnm) : d_pnm(pnm), d_proofs(pnm, ctx), d_current(nullptr) { - d_false = NodeManager::currentNM()->mkConst(false); - d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); + d_false = NodeManager::currentNM()->mkConst(false); + d_zero = NodeManager::currentNM()->mkConstReal(Rational(0)); } void CoveringsProofGenerator::startNewProof() diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp index a913b64d6..db92ce763 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -37,9 +37,9 @@ ExtState::ExtState(InferenceManager& im, NlModel& model, Env& env) { d_false = NodeManager::currentNM()->mkConst(false); d_true = NodeManager::currentNM()->mkConst(true); - 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( diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index b3a373703..5c93be8cb 100644 --- a/src/theory/arith/nl/ext/factoring_check.cpp +++ b/src/theory/arith/nl/ext/factoring_check.cpp @@ -35,7 +35,7 @@ namespace nl { FactoringCheck::FactoringCheck(Env& env, ExtState* data) : EnvObj(env), d_data(data) { - d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1)); + d_one = NodeManager::currentNM()->mkConstReal(Rational(1)); } void FactoringCheck::check(const std::vector& asserts, diff --git a/src/theory/arith/nl/ext/monomial.cpp b/src/theory/arith/nl/ext/monomial.cpp index c82d2664e..526d48778 100644 --- a/src/theory/arith/nl/ext/monomial.cpp +++ b/src/theory/arith/nl/ext/monomial.cpp @@ -124,7 +124,7 @@ void MonomialIndex::addTerm(Node n, MonomialDb::MonomialDb() { - d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1)); + d_one = NodeManager::currentNM()->mkConstReal(Rational(1)); } void MonomialDb::registerMonomial(Node n) diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp index c2919fca6..2d9ef5b8d 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp +++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp @@ -363,11 +363,11 @@ void MonomialBoundsCheck::checkBounds(const std::vector& asserts, proof->addStep(exp[1][0], PfRule::AND_ELIM, {exp[1]}, - {nm->mkConst(CONST_RATIONAL, Rational(0))}); + {nm->mkConstReal(Rational(0))}); proof->addStep(exp[1][1], PfRule::AND_ELIM, {exp[1]}, - {nm->mkConst(CONST_RATIONAL, Rational(1))}); + {nm->mkConstReal(Rational(1))}); Node lb = nm->mkNode(Kind::GEQ, simpleeq[0], simpleeq[1]); Node rb = nm->mkNode(Kind::LEQ, simpleeq[0], simpleeq[1]); if (rew->rewrite(lb) == rew->rewrite(exp[1][0])) diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp index cae590492..0e3b06b49 100644 --- a/src/theory/arith/nl/ext/proof_checker.cpp +++ b/src/theory/arith/nl/ext/proof_checker.cpp @@ -123,8 +123,7 @@ Node ExtProofRuleChecker::checkInternal(PfRule id, Assert(args[2].getType().isRealOrInt()); Assert(args[3].getType().isRealOrInt()); Assert(args[4].getType().isRealOrInt()); - Assert(args[5].isConst() && args[5].getKind() == Kind::CONST_RATIONAL - && args[5].getConst().isIntegral()); + Assert(args[5].isConst() && args[5].getConst().isIntegral()); Node t = args[0]; Node x = args[1]; Node y = args[2]; diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp index add09b67d..02ad39563 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.cpp +++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp @@ -148,16 +148,15 @@ void TangentPlaneCheck::check(bool asWaitingLemmas) if (d_data->isProofEnabled()) { proof = d_data->getProof(); - proof->addStep( - tlem, - PfRule::ARITH_MULT_TANGENT, - {}, - {t, - a, - b, - a_v, - b_v, - nm->mkConst(CONST_RATIONAL, Rational(d == 0 ? -1 : 1))}); + proof->addStep(tlem, + PfRule::ARITH_MULT_TANGENT, + {}, + {t, + a, + b, + a_v, + b_v, + nm->mkConstReal(Rational(d == 0 ? -1 : 1))}); } d_data->d_im.addPendingLemma(tlem, InferenceId::ARITH_NL_TANGENT_PLANE, diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index 4c97801f0..b7c09244c 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -36,9 +36,9 @@ NlModel::NlModel(Env& env) : EnvObj(env), d_used_approx(false) { 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_two = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(2)); + d_zero = NodeManager::currentNM()->mkConstReal(Rational(0)); + d_one = NodeManager::currentNM()->mkConstReal(Rational(1)); + d_two = NodeManager::currentNM()->mkConstReal(Rational(2)); } NlModel::~NlModel() {} diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 254eb5b4f..b8030ff84 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -71,9 +71,9 @@ NonlinearExtension::NonlinearExtension(Env& env, d_extTheory.addFunctionKind(kind::IAND); d_extTheory.addFunctionKind(kind::POW2); d_true = NodeManager::currentNM()->mkConst(true); - 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()) { diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp index 46f1a6a21..fad3a997e 100644 --- a/src/theory/arith/nl/poly_conversion.cpp +++ b/src/theory/arith/nl/poly_conversion.cpp @@ -72,14 +72,13 @@ cvc5::internal::Node as_cvc_upolynomial(const poly::UPolynomial& p, const cvc5:: auto* nm = NodeManager::currentNM(); - Node res = nm->mkConst(CONST_RATIONAL, Rational(0)); - Node monomial = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node res = nm->mkConstReal(Rational(0)); + Node monomial = nm->mkConstReal(Rational(1)); for (std::size_t i = 0, n = coeffs.size(); i < n; ++i) { if (!is_zero(coeffs[i])) { - Node coeff = - nm->mkConst(CONST_RATIONAL, poly_utils::toRational(coeffs[i])); + Node coeff = nm->mkConstReal(poly_utils::toRational(coeffs[i])); Node term = nm->mkNode(Kind::MULT, coeff, monomial); res = nm->mkNode(Kind::ADD, res, term); } @@ -100,14 +99,14 @@ poly::UPolynomial as_poly_upolynomial_impl(const cvc5::internal::Node& n, << n; return poly::UPolynomial({0, 1}); } - switch (n.getKind()) + if (n.isConst()) { - case Kind::CONST_RATIONAL: - { Rational r = n.getConst(); denominator = poly_utils::toInteger(r.getDenominator()); return poly::UPolynomial(poly_utils::toInteger(r.getNumerator())); - } + } + switch (n.getKind()) + { case Kind::ADD: { poly::UPolynomial res; @@ -158,14 +157,14 @@ poly::Polynomial as_poly_polynomial_impl(const cvc5::internal::Node& n, { return poly::Polynomial(vm(n)); } - switch (n.getKind()) + if (n.isConst()) { - case Kind::CONST_RATIONAL: - { Rational r = n.getConst(); denominator = poly_utils::toInteger(r.getDenominator()); return poly::Polynomial(poly_utils::toInteger(r.getNumerator())); - } + } + switch (n.getKind()) + { case Kind::ADD: { poly::Polynomial res; @@ -238,15 +237,15 @@ void collect_monomials(const lp_polynomial_context_t* ctx, { CollectMonomialData* d = static_cast(data); // constant - Node term = d->d_nm->mkConst( - CONST_RATIONAL, poly_utils::toRational(poly::Integer(&m->a))); + Node term = + d->d_nm->mkConstReal(poly_utils::toRational(poly::Integer(&m->a))); for (std::size_t i = 0; i < m->n; ++i) { // variable exponent pair Node var = d->d_vm(m->p[i].x); if (m->p[i].d > 1) { - Node exp = d->d_nm->mkConst(CONST_RATIONAL, m->p[i].d); + Node exp = d->d_nm->mkConstReal(m->p[i].d); term = d->d_nm->mkNode( Kind::NONLINEAR_MULT, term, d->d_nm->mkNode(Kind::POW, var, exp)); } @@ -267,7 +266,7 @@ cvc5::internal::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper if (cmd.d_terms.empty()) { - return cmd.d_nm->mkConst(CONST_RATIONAL, 0); + return cmd.d_nm->mkConstReal(0); } if (cmd.d_terms.size() == 1) { @@ -374,26 +373,23 @@ Node ran_to_node(const poly::AlgebraicNumber& an, const Node& ran_variable) const poly::DyadicInterval& di = get_isolating_interval(an); if (is_point(di)) { - return nm->mkConst(CONST_RATIONAL, poly_utils::toRational(get_point(di))); + return nm->mkConstReal(poly_utils::toRational(get_point(di))); } Assert(di.get_internal()->a_open && di.get_internal()->b_open) << "We assume an open interval here."; Node poly = as_cvc_upolynomial(get_defining_polynomial(an), ran_variable); - Node lower = - nm->mkConst(CONST_RATIONAL, poly_utils::toRational(get_lower(di))); - Node upper = - nm->mkConst(CONST_RATIONAL, poly_utils::toRational(get_upper(di))); + Node lower = nm->mkConstReal(poly_utils::toRational(get_lower(di))); + Node upper = nm->mkConstReal(poly_utils::toRational(get_upper(di))); // Construct witness: - return nm->mkNode( - Kind::AND, - // poly(var) == 0 - nm->mkNode(Kind::EQUAL, poly, nm->mkConst(CONST_RATIONAL, Rational(0))), - // lower_bound < var - nm->mkNode(Kind::LT, lower, ran_variable), - // var < upper_bound - nm->mkNode(Kind::LT, ran_variable, upper)); + return nm->mkNode(Kind::AND, + // poly(var) == 0 + nm->mkNode(Kind::EQUAL, poly, nm->mkConstReal(Rational(0))), + // lower_bound < var + nm->mkNode(Kind::LT, lower, ran_variable), + // var < upper_bound + nm->mkNode(Kind::LT, ran_variable, upper)); } Node value_to_node(const poly::Value& v, const Node& ran_variable) @@ -410,19 +406,18 @@ Node value_to_node(const poly::Value& v, const Node& ran_variable) } if (is_dyadic_rational(v)) { - return nm->mkConst(CONST_RATIONAL, - poly_utils::toRational(as_dyadic_rational(v))); + return nm->mkConstReal(poly_utils::toRational(as_dyadic_rational(v))); } if (is_integer(v)) { - return nm->mkConst(CONST_RATIONAL, poly_utils::toRational(as_integer(v))); + return nm->mkConstReal(poly_utils::toRational(as_integer(v))); } if (is_rational(v)) { - return nm->mkConst(CONST_RATIONAL, poly_utils::toRational(as_rational(v))); + return nm->mkConstReal(poly_utils::toRational(as_rational(v))); } Assert(false) << "All cases should be covered."; - return nm->mkConst(CONST_RATIONAL, Rational(0)); + return nm->mkConstReal(Rational(0)); } Node lower_bound_as_node(const Node& var, @@ -433,18 +428,16 @@ Node lower_bound_as_node(const Node& var, auto* nm = NodeManager::currentNM(); if (!poly::is_algebraic_number(lower)) { - return nm->mkNode( - open ? Kind::LEQ : Kind::LT, - var, - nm->mkConst(CONST_RATIONAL, poly_utils::toRationalAbove(lower))); + return nm->mkNode(open ? Kind::LEQ : Kind::LT, + var, + nm->mkConstReal(poly_utils::toRationalAbove(lower))); } if (poly::represents_rational(lower)) { - return nm->mkNode( - open ? Kind::LEQ : Kind::LT, - var, - nm->mkConst(CONST_RATIONAL, - poly_utils::toRationalAbove(poly::get_rational(lower)))); + return nm->mkNode(open ? Kind::LEQ : Kind::LT, + var, + nm->mkConstReal(poly_utils::toRationalAbove( + poly::get_rational(lower)))); } if (!allowNonlinearLemma) { @@ -479,12 +472,10 @@ Node lower_bound_as_node(const Node& var, } return nm->mkNode( Kind::OR, - nm->mkNode(Kind::LEQ, var, nm->mkConst(CONST_RATIONAL, l)), - nm->mkNode( - Kind::AND, - nm->mkNode(Kind::LT, var, nm->mkConst(CONST_RATIONAL, u)), - nm->mkNode( - relation, poly, nm->mkConst(CONST_RATIONAL, Rational(0))))); + nm->mkNode(Kind::LEQ, var, nm->mkConstReal(l)), + nm->mkNode(Kind::AND, + nm->mkNode(Kind::LT, var, nm->mkConstReal(u)), + nm->mkNode(relation, poly, nm->mkConstReal(Rational(0))))); } Node upper_bound_as_node(const Node& var, @@ -495,18 +486,16 @@ Node upper_bound_as_node(const Node& var, auto* nm = NodeManager::currentNM(); if (!poly::is_algebraic_number(upper)) { - return nm->mkNode( - open ? Kind::GEQ : Kind::GT, - var, - nm->mkConst(CONST_RATIONAL, poly_utils::toRationalAbove(upper))); + return nm->mkNode(open ? Kind::GEQ : Kind::GT, + var, + nm->mkConstReal(poly_utils::toRationalAbove(upper))); } if (poly::represents_rational(upper)) { - return nm->mkNode( - open ? Kind::GEQ : Kind::GT, - var, - nm->mkConst(CONST_RATIONAL, - poly_utils::toRationalAbove(poly::get_rational(upper)))); + return nm->mkNode(open ? Kind::GEQ : Kind::GT, + var, + nm->mkConstReal(poly_utils::toRationalAbove( + poly::get_rational(upper)))); } if (!allowNonlinearLemma) { @@ -541,12 +530,10 @@ Node upper_bound_as_node(const Node& var, } return nm->mkNode( Kind::OR, - nm->mkNode(Kind::GEQ, var, nm->mkConst(CONST_RATIONAL, u)), - nm->mkNode( - Kind::AND, - nm->mkNode(Kind::GT, var, nm->mkConst(CONST_RATIONAL, l)), - nm->mkNode( - relation, poly, nm->mkConst(CONST_RATIONAL, Rational(0))))); + nm->mkNode(Kind::GEQ, var, nm->mkConstReal(u)), + nm->mkNode(Kind::AND, + nm->mkNode(Kind::GT, var, nm->mkConstReal(l)), + nm->mkNode(relation, poly, nm->mkConstReal(Rational(0))))); } Node excluding_interval_to_lemma(const Node& variable, @@ -568,12 +555,10 @@ Node excluding_interval_to_lemma(const Node& variable, if (poly::is_rational(alg)) { Trace("nl-cov") << "Rational point interval: " << interval << std::endl; - return nm->mkNode( - Kind::DISTINCT, - variable, - nm->mkConst( - CONST_RATIONAL, - poly_utils::toRational(poly::to_rational_approximation(alg)))); + return nm->mkNode(Kind::DISTINCT, + variable, + nm->mkConstReal(poly_utils::toRational( + poly::to_rational_approximation(alg)))); } Trace("nl-cov") << "Algebraic point interval: " << interval << std::endl; // p(x) != 0 or x <= lb or ub <= x @@ -582,26 +567,22 @@ Node excluding_interval_to_lemma(const Node& variable, Node poly = as_cvc_upolynomial(get_defining_polynomial(alg), variable); return nm->mkNode( Kind::OR, - nm->mkNode( - Kind::DISTINCT, poly, nm->mkConst(CONST_RATIONAL, Rational(0))), - nm->mkNode( - Kind::LT, - variable, - nm->mkConst(CONST_RATIONAL, poly_utils::toRationalBelow(lv))), - nm->mkNode( - Kind::GT, - variable, - nm->mkConst(CONST_RATIONAL, poly_utils::toRationalAbove(lv)))); + nm->mkNode(Kind::DISTINCT, poly, nm->mkConstReal(Rational(0))), + nm->mkNode(Kind::LT, + variable, + nm->mkConstReal(poly_utils::toRationalBelow(lv))), + nm->mkNode(Kind::GT, + variable, + nm->mkConstReal(poly_utils::toRationalAbove(lv)))); } return Node(); } else { Trace("nl-cov") << "Rational point interval: " << interval << std::endl; - return nm->mkNode( - Kind::DISTINCT, - variable, - nm->mkConst(CONST_RATIONAL, poly_utils::toRationalBelow(lv))); + return nm->mkNode(Kind::DISTINCT, + variable, + nm->mkConstReal(poly_utils::toRationalBelow(lv))); } } if (li) -- 2.30.2