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.

1 files changed, 9 insertions, 8 deletions

diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp
index 46b36986a..e4b91d4d8 100644
--- a/src/theory/strings/strings_rewriter.cpp
+++ b/src/theory/strings/strings_rewriter.cpp
@@ -100,11 +100,11 @@ Node StringsRewriter::rewriteStrToInt(Node node)
     String s = node[0].getConst<String>();
     if (s.isNumber())
     {
-      ret = nm->mkConst(s.toNumber());
+      ret = nm->mkConst(CONST_RATIONAL, s.toNumber());
     }
     else
     {
-      ret = nm->mkConst(Rational(-1));
+      ret = nm->mkConst(CONST_RATIONAL, Rational(-1));
     }
     return returnRewrite(node, ret, Rewrite::STOI_EVAL);
   }
@@ -117,7 +117,7 @@ Node StringsRewriter::rewriteStrToInt(Node node)
         String t = nc.getConst<String>();
         if (!t.isNumber())
         {
-          Node ret = nm->mkConst(Rational(-1));
+          Node ret = nm->mkConst(CONST_RATIONAL, Rational(-1));
           return returnRewrite(node, ret, Rewrite::STOI_CONCAT_NONNUM);
         }
       }
@@ -303,11 +303,11 @@ Node StringsRewriter::rewriteStringToCode(Node n)
     {
       std::vector<unsigned> vec = s.getVec();
       Assert(vec.size() == 1);
-      ret = nm->mkConst(Rational(vec[0]));
+      ret = nm->mkConst(CONST_RATIONAL, Rational(vec[0]));
     }
     else
     {
-      ret = nm->mkConst(Rational(-1));
+      ret = nm->mkConst(CONST_RATIONAL, Rational(-1));
     }
     return returnRewrite(n, ret, Rewrite::TO_CODE_EVAL);
   }
@@ -320,9 +320,10 @@ Node StringsRewriter::rewriteStringIsDigit(Node n)
   NodeManager* nm = NodeManager::currentNM();
   // eliminate str.is_digit(s) ----> 48 <= str.to_code(s) <= 57
   Node t = nm->mkNode(STRING_TO_CODE, n[0]);
-  Node retNode = nm->mkNode(AND,
-                            nm->mkNode(LEQ, nm->mkConst(Rational(48)), t),
-                            nm->mkNode(LEQ, t, nm->mkConst(Rational(57))));
+  Node retNode =
+      nm->mkNode(AND,
+                 nm->mkNode(LEQ, nm->mkConst(CONST_RATIONAL, Rational(48)), t),
+                 nm->mkNode(LEQ, t, nm->mkConst(CONST_RATIONAL, Rational(57))));
   return returnRewrite(n, retNode, Rewrite::IS_DIGIT_ELIM);
 }