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.

3 files changed, 0 insertions, 3 deletions

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 89d56a108..236eb534c 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -34,7 +34,6 @@
 using namespace std;
 using namespace cvc5;
 using namespace cvc5::parser;
-using namespace cvc5::kind;
 
 namespace cvc5 {
 namespace parser {
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index c8c005b36..0fb44b4a9 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -26,7 +26,6 @@
 using namespace std;
 using namespace cvc5;
 using namespace cvc5::parser;
-using namespace cvc5::kind;
 
 namespace cvc5 {
 namespace parser {
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 83b1f5025..570f1369a 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -31,7 +31,6 @@
 #include "smt/command.h"
 
 using namespace std;
-using namespace cvc5::kind;
 
 namespace cvc5 {
 namespace parser {