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 9bfb34cf713030535fa613a434ff70859f83f927..af683ffc6cbe97815b2f447f27aa1d3176f220ab 100644 (file)
--- 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<Node> new_children = {vp1, children[0]};
-      new_args.push_back(nm->mkConst<Rational>(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<Node> new_children = {vp1, children[0]};
-      new_args.push_back(nm->mkConst<Rational>(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<Node> sanitized_args{
-        res,
-        res,
-        nm->mkConst<Rational>(CONST_RATIONAL,
-                              static_cast<unsigned>(AletheRule::ASSUME))};
+        res, res, nm->mkConstInt(static_cast<uint32_t>(AletheRule::ASSUME))};
     for (const Node& arg : args)
     {
       sanitized_args.push_back(d_anc.convert(arg));
@@ -1940,8 +1937,8 @@ bool AletheProofPostprocessCallback::addAletheStep(
   }
 
   std::vector<Node> new_args = std::vector<Node>();
-  new_args.push_back(NodeManager::currentNM()->mkConst(
-      CONST_RATIONAL, Rational(static_cast<unsigned>(rule))));
+  new_args.push_back(NodeManager::currentNM()->mkConstInt(
+      Rational(static_cast<uint32_t>(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 06d6aeaab3501f777a1c86b945300301a1ff1572..32b630fa8ea5f609b030af08ec6956ccb69a5d8e 100644 (file)
--- 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<Node>& 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 4752d45ffef5fc122f9b06b406e3ece4d41f1266..59bf89151fad1376502529cc628bedc5d1e44fd7 100644 (file)
--- 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 c4f7f6ca96b309260665bfa2b32c4ca2b9c3655b..77e5f9f3f666f1b47affb4de32182a49a2f368c3 100644 (file)
--- 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 dc55632f45ac9d1aa81a9673a46d03f8f2bf2577..3bf1ace987b6a6b57b967f6c688da41468e4f0a2 100644 (file)
--- 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<Node>& children, const std::vector<Node>& args)
 {
   NodeManager* nm = NodeManager::currentNM();
-  auto zero = nm->mkConst<Rational>(CONST_RATIONAL, 0);
-  auto one = nm->mkConst<Rational>(CONST_RATIONAL, 1);
-  auto mone = nm->mkConst<Rational>(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<Rational>().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<Rational>().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<Rational>().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<Rational>().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<Rational>().isIntegral());
+    Assert(args[0].isConst() && args[0].getType().isInteger());
     Assert(args[1].getType().isReal());
     std::uint64_t d =
         args[0].getConst<Rational>().getNumerator().toUnsignedInt();
@@ -238,10 +235,7 @@ Node TranscendentalProofRuleChecker::checkInternal(
             x.eqNode(
                 nm->mkNode(Kind::PLUS,
                            y,
-                           nm->mkNode(Kind::MULT,
-                                      nm->mkConst<Rational>(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<Rational>().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<Rational>().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<Rational>().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<Rational>().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<Rational>().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<Rational>().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 338e37baa24239828c7688e6148d94757bcc88e1..6c1bec647b78f6cac3d55f0d65d824776021536c 100644 (file)
--- 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 898d81c27c2aa923a1279c0e2038dbe3c45270ec..c9e0015e2ca5200550a7f3d46bdfc9d136c510ff 100644 (file)
--- a/src/theory/arith/nl/transcendental/taylor_generator.cpp
+++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp
@@ -51,7 +51,7 @@ std::pair<Node, Node> 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<Node> sum;
   for (std::uint64_t counter = 1; counter <= n; ++counter)
   {
@@ -60,9 +60,7 @@ std::pair<Node, Node> 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<Rational>(CONST_RATIONAL, factorial)));
+          nm->mkNode(Kind::DIVISION, varpow, nm->mkConstReal(factorial)));
     }
     else if (k == Kind::SINE)
     {
@@ -71,20 +69,19 @@ std::pair<Node, Node> 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<Rational>(CONST_RATIONAL, sign),
-                       nm->mkConst<Rational>(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<Rational>(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<Node, Node> 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<Node, Node>(zero, zero);
     }
     Assert(k == Kind::EXPONENTIAL);
-    Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
+    Node one = nm->mkConstReal(Rational(1));
     return std::pair<Node, Node>(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 7c2f1a0587b981b67cef49663a630051c5a7ab69..e32f336ac5985d6b3d6ae3b9f4a4c8ece8731566 100644 (file)
--- 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<CDProof>(
@@ -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<Rational>(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<Rational>(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<Rational>(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<Rational>(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 17efa53a524434f49d0549479258888e35d107d3..99f5621d6b4959c445fee9257993a0cae92eaca8 100644 (file)
--- 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<ArithWitnessVarAttribute>(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 69fe9873404f5dc785cf12362d8ff6b4b729060a..c05f6ae0a9b52e74039d94e1a25b1dcda3a80b2f 100644 (file)
--- 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<Node>& args)
 {
   NodeManager* nm = NodeManager::currentNM();
-  auto zero = nm->mkConst<Rational>(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<Node>{
                             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<Node>{
                             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<Rational>(CONST_RATIONAL, scalar),
-                              children[i][0]);
-        rightSum << nm->mkNode(Kind::MULT,
-                               nm->mkConst<Rational>(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>();
         Rational newBound = leastIntGreaterThan(originalBound);
-        Node rational = nm->mkConst<Rational>(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>();
         Rational newBound = greatestIntLessThan(originalBound);
-        Node rational = nm->mkConst<Rational>(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 6e1b4c1a5e7007357da4122be713aebe8340cbcc..3e6544882212e45e551c55f2527067b8a64c3a42 100644 (file)
--- 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<Node>& 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 71ce13c69e167928c7565ea6288a8458bc384701..58c12ceffa1896cc5fd6ea85c2d057f6708f9cba 100644 (file)
--- 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<Node> 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 4c4540366cb1c0f34d4f183c6bb5c50c20481b30..aa69f9ecf9993a7bb8dcaae89ed6666c4e4f3735 100644 (file)
--- 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<Node>& 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<Rational>();
       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)