From ad340126a7adbb9840cca1d082c57b43995987a4 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 12 Nov 2021 06:14:49 -0800
Subject: Remove `ConstantMap<Rational>` (#7635)

This is in preparation of having two different kinds (CONST_RATIONAL
and CONST_INT) share the same payload. To do so, we cannot rely on
ConstantMap<Rational> anymore to map the payload type to a kind. This
commit extends support in the mkmetakind script to deal with such
payloads by adding a + suffix to the type. The commit also does some
minor refactoring of NodeManager::mkConst() and
NodeManager::mkConstInternal() to support setting the kind explicitly.
Finally, the commit addresses all instances where mkConst<Rational>()
is used, including the API.
---
 src/theory/arith/constraint.cpp | 28 +++++++++++++++-------------
 1 file changed, 15 insertions(+), 13 deletions(-)

(limited to 'src/theory/arith/constraint.cpp')

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 2958b5f48..cffacdc39 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -1122,10 +1122,11 @@ TrustNode Constraint::split()
     auto nGeqPf = d_database->d_pnm->mkAssume(geqNode.negate());
     auto ltPf = d_database->d_pnm->mkNode(
         PfRule::MACRO_SR_PRED_TRANSFORM, {nGeqPf}, {ltNode});
-    auto sumPf = d_database->d_pnm->mkNode(
-        PfRule::MACRO_ARITH_SCALE_SUM_UB,
-        {gtPf, ltPf},
-        {nm->mkConst<Rational>(-1), nm->mkConst<Rational>(1)});
+    auto sumPf =
+        d_database->d_pnm->mkNode(PfRule::MACRO_ARITH_SCALE_SUM_UB,
+                                  {gtPf, ltPf},
+                                  {nm->mkConst(CONST_RATIONAL, Rational(-1)),
+                                   nm->mkConst(CONST_RATIONAL, Rational(1))});
     auto botPf = d_database->d_pnm->mkNode(
         PfRule::MACRO_SR_PRED_TRANSFORM, {sumPf}, {nm->mkConst(false)});
     std::vector<Node> a = {leqNode.negate(), geqNode.negate()};
@@ -1808,7 +1809,7 @@ std::shared_ptr<ProofNode> Constraint::externalExplain(
           std::vector<Node> farkasCoeffs;
           for (Rational r : *getFarkasCoefficients())
           {
-            farkasCoeffs.push_back(nm->mkConst<Rational>(r));
+            farkasCoeffs.push_back(nm->mkConst(CONST_RATIONAL, Rational(r)));
           }
 
           // Apply the scaled-sum rule.
@@ -2088,7 +2089,8 @@ Node Constraint::getProofLiteral() const
     default: Unreachable() << d_type;
   }
   NodeManager* nm = NodeManager::currentNM();
-  Node constPart = nm->mkConst<Rational>(d_value.getNoninfinitesimalPart());
+  Node constPart =
+      nm->mkConst(CONST_RATIONAL, Rational(d_value.getNoninfinitesimalPart()));
   Node posLit = nm->mkNode(cmp, varPart, constPart);
   return neg ? posLit.negate() : posLit;
 }
@@ -2112,13 +2114,13 @@ void ConstraintDatabase::proveOr(std::vector<TrustNode>& out,
                                    {d_pnm->mkAssume(lb.negate())},
                                    {b->getNegation()->getProofLiteral()});
     int sndSign = negateSecond ? -1 : 1;
-    auto bot_pf =
-        d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM,
-                      {d_pnm->mkNode(PfRule::MACRO_ARITH_SCALE_SUM_UB,
-                                     {pf_neg_la, pf_neg_lb},
-                                     {nm->mkConst<Rational>(-1 * sndSign),
-                                      nm->mkConst<Rational>(sndSign)})},
-                      {nm->mkConst(false)});
+    auto bot_pf = d_pnm->mkNode(
+        PfRule::MACRO_SR_PRED_TRANSFORM,
+        {d_pnm->mkNode(PfRule::MACRO_ARITH_SCALE_SUM_UB,
+                       {pf_neg_la, pf_neg_lb},
+                       {nm->mkConst(CONST_RATIONAL, Rational(-1 * sndSign)),
+                        nm->mkConst(CONST_RATIONAL, Rational(sndSign))})},
+        {nm->mkConst(false)});
     std::vector<Node> as;
     std::transform(orN.begin(), orN.end(), std::back_inserter(as), [](Node n) {
       return n.negate();
-- 
cgit v1.2.3