From c1fa82197bfec2bfb3f8655ebfde546d085e0fe4 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 17 Dec 2021 15:09:03 -0600
Subject: [PATCH] Minor refactoring of API for eliminating arithmetic subtypes
 (#7833)

---
 src/api/cpp/cvc5.cpp | 31 ++++++++++++++++++-------------
 src/api/cpp/cvc5.h   |  5 +++--
 2 files changed, 21 insertions(+), 15 deletions(-)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index e9998c72b..24b4500d5 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -27,7 +27,7 @@
  * Our Integer implementation, e.g., is such a special case since we support
  * two different back end implementations (GMP, CLN). Be aware that they do
  * not fully agree on what is (in)valid input, which requires extra checks for
- * consistent behavior (see Solver::mkRealFromStrHelper for an example).
+ * consistent behavior (see Solver::mkRealOrIntegerFromStrHelper for example).
  */
 
 #include "api/cpp/cvc5.h"
@@ -5088,15 +5088,23 @@ Term Solver::mkValHelper(const T& t) const
   return Term(this, res);
 }
 
-Term Solver::mkRationalValHelper(const Rational& r) const
+Term Solver::mkRationalValHelper(const Rational& r, bool isInt) const
 {
   //////// all checks before this line
-  Node res = getNodeManager()->mkConst(kind::CONST_RATIONAL, r);
+  NodeManager* nm = getNodeManager();
+  Node res = isInt ? nm->mkConstInt(r) : nm->mkConstReal(r);
   (void)res.getType(true); /* kick off type checking */
-  return Term(this, res);
+  api::Term t = Term(this, res);
+  // NOTE: this block will be eliminated when arithmetic subtyping is eliminated
+  if (!isInt)
+  {
+    t = ensureRealSort(t);
+  }
+  return t;
 }
 
-Term Solver::mkRealFromStrHelper(const std::string& s) const
+Term Solver::mkRealOrIntegerFromStrHelper(const std::string& s,
+                                          bool isInt) const
 {
   //////// all checks before this line
   try
@@ -5104,7 +5112,7 @@ Term Solver::mkRealFromStrHelper(const std::string& s) const
     cvc5::Rational r = s.find('/') != std::string::npos
                            ? cvc5::Rational(s)
                            : cvc5::Rational::fromDecimal(s);
-    return mkRationalValHelper(r);
+    return mkRationalValHelper(r, isInt);
   }
   catch (const std::invalid_argument& e)
   {
@@ -5837,7 +5845,7 @@ Term Solver::mkInteger(const std::string& s) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_ARG_CHECK_EXPECTED(isValidInteger(s), s) << " an integer ";
-  Term integer = mkRealFromStrHelper(s);
+  Term integer = mkRealOrIntegerFromStrHelper(s);
   CVC5_API_ARG_CHECK_EXPECTED(integer.getSort() == getIntegerSort(), s)
       << " a string representing an integer";
   //////// all checks before this line
@@ -5866,8 +5874,7 @@ Term Solver::mkReal(const std::string& s) const
   CVC5_API_ARG_CHECK_EXPECTED(s != ".", s)
       << "a string representing a real or rational value.";
   //////// all checks before this line
-  Term rational = mkRealFromStrHelper(s);
-  return ensureRealSort(rational);
+  return mkRealOrIntegerFromStrHelper(s, false);
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -5876,8 +5883,7 @@ Term Solver::mkReal(int64_t val) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
-  Term rational = mkRationalValHelper(cvc5::Rational(val));
-  return ensureRealSort(rational);
+  return mkRationalValHelper(cvc5::Rational(val), false);
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -5886,8 +5892,7 @@ Term Solver::mkReal(int64_t num, int64_t den) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
-  Term rational = mkRationalValHelper(cvc5::Rational(num, den));
-  return ensureRealSort(rational);
+  return mkRationalValHelper(cvc5::Rational(num, den), false);
   ////////
   CVC5_API_TRY_CATCH_END;
 }
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index e29729c06..f2bfb48e2 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -4870,9 +4870,10 @@ class CVC5_EXPORT Solver
   template <typename T>
   Term mkValHelper(const T& t) const;
   /** Helper for making rational values. */
-  Term mkRationalValHelper(const Rational& r) const;
+  Term mkRationalValHelper(const Rational& r, bool isInt = true) const;
   /** Helper for mkReal functions that take a string as argument. */
-  Term mkRealFromStrHelper(const std::string& s) const;
+  Term mkRealOrIntegerFromStrHelper(const std::string& s,
+                                    bool isInt = true) const;
   /** Helper for mkBitVector functions that take a string as argument. */
   Term mkBVFromStrHelper(const std::string& s, uint32_t base) const;
   /**
-- 
2.30.2