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.

2 files changed, 4 insertions, 4 deletions

diff --git a/src/smt/difficulty_post_processor.cpp b/src/smt/difficulty_post_processor.cpp
index 748092238..31797ba5e 100644
--- a/src/smt/difficulty_post_processor.cpp
+++ b/src/smt/difficulty_post_processor.cpp
@@ -69,7 +69,7 @@ void DifficultyPostprocessCallback::getDifficultyMap(
   NodeManager* nm = NodeManager::currentNM();
   for (const std::pair<const Node, uint64_t>& d : d_accMap)
   {
-    dmap[d.first] = nm->mkConst(Rational(d.second));
+    dmap[d.first] = nm->mkConst(CONST_RATIONAL, Rational(d.second));
   }
 }
 
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 56a759866..a292fec8f 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -855,7 +855,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
         for (size_t j = 0, nchildi = children[i].getNumChildren(); j < nchildi;
              j++)
         {
-          Node nodej = nm->mkConst(Rational(j));
+          Node nodej = nm->mkConst(CONST_RATIONAL, Rational(j));
           cdp->addStep(
               children[i][j], PfRule::AND_ELIM, {children[i]}, {nodej});
         }
@@ -1086,8 +1086,8 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
       TNode child = children[i];
       TNode scalar = args[i];
       bool isPos = scalar.getConst<Rational>() > 0;
-      Node scalarCmp =
-          nm->mkNode(isPos ? GT : LT, scalar, nm->mkConst(Rational(0)));
+      Node scalarCmp = nm->mkNode(
+          isPos ? GT : LT, scalar, nm->mkConst(CONST_RATIONAL, Rational(0)));
       // (= scalarCmp true)
       Node scalarCmpOrTrue = steps.tryStep(PfRule::EVALUATE, {}, {scalarCmp});
       Assert(!scalarCmpOrTrue.isNull());