Replace mkConst(CONST_RATIONAL) by mkConstReal (#8686)

This PR removes the usages of CONST_RATIONAL in the nonlinear arithmetic solver.

diff --git a/src/theory/arith/nl/coverings/cdcac.cpp b/src/theory/arith/nl/coverings/cdcac.cpp
index d358a34ef759f305013463114dad76a03aa60911..24171c8a3dc28840f97953a70d5f3c46950db732 100644 (file)
--- 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<Node> 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 6d394c52d1fbcb7507e493309c8297d840b47a73..4ffd88fa6006a1ee1f41c376b488dfc90df8c885 100644 (file)
--- 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<bool>(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 a913b64d68477cd57544c4925414ebb0d5300233..db92ce76329d81c126e7f12d474023b369d59243 100644 (file)
--- 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<CDProof>(

diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp
index b3a373703d5d9c921b70a9bb85903dfd23064fea..5c93be8cb24c5e9423f830e6445f1188b87d5e33 100644 (file)
--- 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<Node>& asserts,

diff --git a/src/theory/arith/nl/ext/monomial.cpp b/src/theory/arith/nl/ext/monomial.cpp
index c82d2664e2b261ac71b79b7d3de8956b8a1601e3..526d48778ef5cafaf14e6e6cfa6b2a587c55e2ee 100644 (file)
--- 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 c2919fca6529abb8313544d9a37b5fff2138feef..2d9ef5b8d35f315314dbb3d7c6b637f5cef2af2f 100644 (file)
--- 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<Node>& 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 cae590492813a0f2b5180f05b07ecf3ef5f50e76..0e3b06b49bfde013028a0d12644348a8ca7c2add 100644 (file)
--- 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<Rational>().isIntegral());
+    Assert(args[5].isConst() && args[5].getConst<Rational>().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 add09b67d78e05675b8a655d069e30b3712e07f7..02ad395630148e6e9de8a4fb767eb51703da3d16 100644 (file)
--- 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 4c97801f0f16447f0008cbc7017cf60a391a23c5..b7c09244cf63a2d6aa49587956fd9d1bb37e1839 100644 (file)
--- 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 254eb5b4f5500f3e9a3c8f30f4f590a074018f33..b8030ff843df54cf78bb2139dd775d21fec3b303 100644 (file)
--- 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 46f1a6a21202dfdf14a64576023ece3d46acf373..fad3a997e5826938771d5490cd7b5b0e7111a062 100644 (file)
--- 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<Rational>();
       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<Rational>();
       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<CollectMonomialData*>(data);
   // constant
-  Node term = d->d_nm->mkConst<Rational>(
-      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<Rational>(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<Rational>(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)