Add mkInteger to the API (#5274)

This PR adds mkInteger to the API and update mkReal to ensure that the returned term has real sort.
The parsers are modified to parse numbers like "0" "5" as integers and "0.0" and "15.0" as reals.
This means subtyping is effectively eliminated from all theories except arithmetic.
Other changes:

Term::isValue is removed which was introduced to support parsing for constant arrays. It is no longer needed after this PR.
Benchmarks are updated to match the changes in the parsers
Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu

14 files changed, 192 insertions, 108 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index be82a517f..507e270bb 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -34,6 +34,7 @@
 #include "api/cvc4cpp.h"
 
 #include <cstring>
+#include <regex>
 #include <sstream>
 
 #include "base/check.h"
@@ -1603,7 +1604,7 @@ Kind Term::getKindHelper() const
   // (string) versions back to sequence. All operators where this is
   // necessary are such that their first child is of sequence type, which
   // we check here.
-  if (getNumChildren() > 0 && (*this)[0].getSort().isSequence())
+  if (d_node->getNumChildren() > 0 && (*d_node)[0].getType().isSequence())
   {
     switch (d_node->getKind())
     {
@@ -1626,9 +1627,22 @@ Kind Term::getKindHelper() const
   }
   // Notice that kinds like APPLY_TYPE_ASCRIPTION will be converted to
   // INTERNAL_KIND.
+  if(isCastedReal())
+  {
+    return CONST_RATIONAL;
+  }
   return intToExtKind(d_node->getKind());
 }
 
+bool Term::isCastedReal() const
+{
+  if(d_node->getKind() == kind::CAST_TO_REAL)
+  {
+    return (*d_node)[0].isConst() && (*d_node)[0].getType().isInteger();
+  }
+  return false;
+}
+
 bool Term::operator==(const Term& t) const { return *d_node == *t.d_node; }
 
 bool Term::operator!=(const Term& t) const { return *d_node != *t.d_node; }
@@ -1649,12 +1663,20 @@ size_t Term::getNumChildren() const
   {
     return d_node->getNumChildren() + 1;
   }
+  if(isCastedReal())
+  {
+    return 0;
+  }
   return d_node->getNumChildren();
 }
 
 Term Term::operator[](size_t index) const
 {
   CVC4_API_CHECK_NOT_NULL;
+
+  // check the index within the number of children
+  CVC4_API_CHECK(index < getNumChildren()) << "index out of bound";
+
   // special cases for apply kinds
   if (isApplyKind(d_node->getKind()))
   {
@@ -1763,12 +1785,6 @@ Op Term::getOp() const
 
 bool Term::isNull() const { return isNullHelper(); }
 
-bool Term::isValue() const
-{
-  CVC4_API_CHECK_NOT_NULL;
-  return d_node->isConst();
-}
-
 Term Term::getConstArrayBase() const
 {
   CVC4::ExprManagerScope exmgrs(*(d_solver->getExprManager()));
@@ -3109,16 +3125,20 @@ Term Solver::mkValHelper(T t) const
 
 Term Solver::mkRealFromStrHelper(const std::string& s) const
 {
-  /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
-   * throws an std::invalid_argument exception. For consistency, we treat it
-   * as invalid. */
-  CVC4_API_ARG_CHECK_EXPECTED(s != ".", s)
-      << "a string representing an integer, real or rational value.";
-
-  CVC4::Rational r = s.find('/') != std::string::npos
-                         ? CVC4::Rational(s)
-                         : CVC4::Rational::fromDecimal(s);
-  return mkValHelper<CVC4::Rational>(r);
+  try
+  {
+    CVC4::Rational r = s.find('/') != std::string::npos
+                           ? CVC4::Rational(s)
+                           : CVC4::Rational::fromDecimal(s);
+    return mkValHelper<CVC4::Rational>(r);
+  }
+  catch (const std::invalid_argument& e)
+  {
+    std::stringstream message;
+    message << "Cannot construct Real or Int from string argument '" << s << "'"
+            << std::endl;
+    throw std::invalid_argument(message.str());
+  }
 }
 
 Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const
@@ -3725,24 +3745,66 @@ Term Solver::mkPi() const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+Term Solver::mkInteger(const std::string& s) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_ARG_CHECK_EXPECTED(std::regex_match(s, std::regex("-?\\d+")), s)
+      << " an integer ";
+  Term integer = mkRealFromStrHelper(s);
+  CVC4_API_ARG_CHECK_EXPECTED(integer.getSort() == getIntegerSort(), s)
+      << " an integer";
+  return integer;
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
+Term Solver::mkInteger(int64_t val) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  Term integer = mkValHelper<CVC4::Rational>(CVC4::Rational(val));
+  Assert(integer.getSort() == getIntegerSort());
+  return integer;
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
 Term Solver::mkReal(const std::string& s) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return mkRealFromStrHelper(s);
+  /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
+   * throws an std::invalid_argument exception. For consistency, we treat it
+   * as invalid. */
+  CVC4_API_ARG_CHECK_EXPECTED(s != ".", s)
+      << "a string representing a real or rational value.";
+  Term rational = mkRealFromStrHelper(s);
+  return ensureRealSort(rational);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+Term Solver::ensureRealSort(const Term t) const
+{
+  CVC4_API_ARG_CHECK_EXPECTED(
+      t.getSort() == getIntegerSort() || t.getSort() == getRealSort(),
+      " an integer or real term");
+  if (t.getSort() == getIntegerSort())
+  {
+    Node n = getNodeManager()->mkNode(kind::CAST_TO_REAL, *t.d_node);
+    return Term(this, n);
+  }
+  return t;
+}
+
 Term Solver::mkReal(int64_t val) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
+  Term rational = mkValHelper<CVC4::Rational>(CVC4::Rational(val));
+  return ensureRealSort(rational);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Term Solver::mkReal(int64_t num, int64_t den) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
+  Term rational = mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
+  return ensureRealSort(rational);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -3918,10 +3980,17 @@ Term Solver::mkConstArray(Sort sort, Term val) const
   CVC4_API_SOLVER_CHECK_SORT(sort);
   CVC4_API_SOLVER_CHECK_TERM(val);
   CVC4_API_CHECK(sort.isArray()) << "Not an array sort.";
-  CVC4_API_CHECK(sort.getArrayElementSort().isComparableTo(val.getSort()))
+  CVC4_API_CHECK(val.getSort().isSubsortOf(sort.getArrayElementSort()))
       << "Value does not match element sort.";
-  Term res = mkValHelper<CVC4::ArrayStoreAll>(CVC4::ArrayStoreAll(
-      TypeNode::fromType(*sort.d_type), Node::fromExpr(val.d_node->toExpr())));
+  // handle the special case of (CAST_TO_REAL n) where n is an integer
+  Node n = *val.d_node;
+  if (val.isCastedReal())
+  {
+    // this is safe because the constant array stores its type
+    n = n[0];
+  }
+  Term res = mkValHelper<CVC4::ArrayStoreAll>(
+      CVC4::ArrayStoreAll(TypeNode::fromType(*sort.d_type), n));
   return res;
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 646695c64..c05390e42 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -982,13 +982,6 @@ class CVC4_PUBLIC Term
   bool isNull() const;
 
   /**
-   * Check if this is a Term representing a value.
-   *
-   * @return true if this is a Term representing a value
-   */
-  bool isValue() const;
-
-  /**
    *  Return the base (element stored at all indices) of a constant array
    *  throws an exception if the kind is not CONST_ARRAY
    *  @return the base value
@@ -1176,6 +1169,11 @@ class CVC4_PUBLIC Term
   Kind getKindHelper() const;
 
   /**
+   * returns true if the current term is a constant integer that is casted into
+   * real using the operator CAST_TO_REAL, and returns false otherwise
+   */
+  bool isCastedReal() const;
+  /**
    * The internal expression wrapped by this term.
    * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
    * memory allocation (CVC4::Expr is already ref counted, so this could be
@@ -2580,12 +2578,26 @@ class CVC4_PUBLIC Solver
    * @return a constant representing Pi
    */
   Term mkPi() const;
+  /**
+   * Create an integer constant from a string.
+   * @param s the string representation of the constant, may represent an
+   *          integer (e.g., "123").
+   * @return a constant of sort Integer assuming 's' represents an integer)
+   */
+  Term mkInteger(const std::string& s) const;
+
+  /**
+   * Create an integer constant from a c++ int.
+   * @param val the value of the constant
+   * @return a constant of sort Integer
+   */
+  Term mkInteger(int64_t val) const;
 
   /**
    * Create a real constant from a string.
    * @param s the string representation of the constant, may represent an
    *          integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").
-   * @return a constant of sort Real or Integer (if 's' represents an integer)
+   * @return a constant of sort Real
    */
   Term mkReal(const std::string& s) const;
 
@@ -2600,7 +2612,7 @@ class CVC4_PUBLIC Solver
    * Create a real constant from a rational.
    * @param num the value of the numerator
    * @param den the value of the denominator
-   * @return a constant of sort Real or Integer (if 'num' is divisible by 'den')
+   * @return a constant of sort Real
    */
   Term mkReal(int64_t num, int64_t den) const;
 
@@ -3461,10 +3473,10 @@ class CVC4_PUBLIC Solver
   /**
    * Helper function that ensures that a given term is of sort real (as opposed
    * to being of sort integer).
-   * @param term a term of sort integer or real
+   * @param t a term of sort integer or real
    * @return a term of sort real
    */
-  Term ensureRealSort(Term expr) const;
+  Term ensureRealSort(Term t) const;
 
   /**
    * Create n-ary term of given kind. This handles the cases of left/right
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 73ccde14a..113895ad7 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -173,6 +173,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         Term mkFalse() except +
         Term mkBoolean(bint val) except +
         Term mkPi() except +
+        Term mkInteger(const string& s) except +
         Term mkReal(const string& s) except +
         Term mkRegexpEmpty() except +
         Term mkRegexpSigma() except +
@@ -329,7 +330,6 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         bint hasOp() except +
         Op getOp() except +
         bint isNull() except +
-        bint isValue() except +
         Term getConstArrayBase() except +
         vector[Term] getConstSequenceElements() except +
         Term notTerm() except +
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index 188b678d1..4cdd60893 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -664,6 +664,12 @@ cdef class Solver:
         term.cterm = self.csolver.mkPi()
         return term
 
+    def mkInteger(self, val):
+        cdef Term term = Term(self)
+        integer = int(val)
+        term.cterm = self.csolver.mkInteger("{}".format(integer).encode())
+        return term
+
     def mkReal(self, val, den=None):
         cdef Term term = Term(self)
         if den is None:
@@ -1448,9 +1454,6 @@ cdef class Term:
     def isNull(self):
         return self.cterm.isNull()
 
-    def isValue(self):
-        return self.cterm.isValue()
-
     def getConstArrayBase(self):
         cdef Term term = Term(self.solver)
         term.cterm = self.cterm.getConstArrayBase()
@@ -1502,7 +1505,6 @@ cdef class Term:
     def toPythonObj(self):
         '''
         Converts a constant value Term to a Python object.
-        Requires isValue to hold.
 
         Currently supports:
           Boolean -- returns a Python bool
@@ -1514,9 +1516,6 @@ cdef class Term:
           String  -- returns a Python Unicode string
         '''
 
-        if not self.isValue():
-            raise RuntimeError("Cannot call toPythonObj on a non-const Term")
-
         string_repr = self.cterm.toString().decode()
         assert string_repr
         sort = self.getSort()
diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp
index 92383dcd1..ed21f8f9c 100644
--- a/src/expr/array_store_all.cpp
+++ b/src/expr/array_store_all.cpp
@@ -45,7 +45,8 @@ ArrayStoreAll::ArrayStoreAll(const TypeNode& type, const Node& value)
       "expr type `%s' does not match constituent type of array type `%s'",
       value.getType().toString().c_str(),
       type.toString().c_str());
-
+  Trace("arrays") << "constructing constant array of type: '" << type
+                  << "' and value: '" << value << "'" << std::endl;
   PrettyCheckArgument(
       value.isConst(), value, "ArrayStoreAll requires a constant expression");
 
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 292871d2a..0bb41b483 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -2177,13 +2177,6 @@ simpleTerm[CVC4::api::Term& f]
        * literals, we can use the push/pop scope. */
       /* PARSER_STATE->popScope(); */
       t = SOLVER->mkArraySort(t, t2);
-      if(!f.isValue()) {
-        std::stringstream ss;
-        ss << "expected constant term inside array constant, but found "
-           << "nonconstant term" << std::endl
-           << "the term: " << f;
-        PARSER_STATE->parseError(ss.str());
-      }
       if(!t2.isComparableTo(f.getSort())) {
         std::stringstream ss;
         ss << "type mismatch inside array constant term:" << std::endl
@@ -2207,18 +2200,12 @@ simpleTerm[CVC4::api::Term& f]
       std::stringstream strRat;
       strRat << r;
       f = SOLVER->mkReal(strRat.str());
-      if(f.getSort().isInteger()) {
-        // Must cast to Real to ensure correct type is passed to parametric type constructors.
-        // We do this cast using division with 1.
-        // This has the advantage wrt using TO_REAL since (constant) division is always included in the theory.
-        f = MK_TERM(api::DIVISION, f, SOLVER->mkReal(1));
-      }
     }
   | INTEGER_LITERAL {
       Rational r = AntlrInput::tokenToRational($INTEGER_LITERAL);
       std::stringstream strRat;
       strRat << r;
-      f = SOLVER->mkReal(strRat.str());
+      f = SOLVER->mkInteger(strRat.str());
     }
     /* bitvector literals */
   | HEX_LITERAL
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 7c1c5dc3e..7647f8e53 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1710,7 +1710,7 @@ identifier[CVC4::ParseOp& p]
         // we adopt a special syntax (_ tupSel n)
         p.d_kind = api::APPLY_SELECTOR;
         // put m in expr so that the caller can deal with this case
-        p.d_expr = SOLVER->mkReal(AntlrInput::tokenToUnsigned($m));
+        p.d_expr = SOLVER->mkInteger(AntlrInput::tokenToUnsigned($m));
       }
     | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
       {
@@ -1735,7 +1735,7 @@ termAtomic[CVC4::api::Term& atomTerm]
   : INTEGER_LITERAL
     {
       std::string intStr = AntlrInput::tokenText($INTEGER_LITERAL);
-      atomTerm = SOLVER->mkReal(intStr);
+      atomTerm = SOLVER->mkInteger(intStr);
     }
   | DECIMAL_LITERAL
     {
@@ -1830,7 +1830,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
     {
       std::stringstream sIntLit;
       sIntLit << $INTEGER_LITERAL;
-      api::Term n = SOLVER->mkReal(sIntLit.str());
+      api::Term n = SOLVER->mkInteger(sIntLit.str());
       std::vector<api::Term> values;
       values.push_back( n );
       std::string attr_name(AntlrInput::tokenText($tok));
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 629164593..edeb47f06 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1055,33 +1055,22 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       parseError("Too many arguments to array constant.");
     }
     api::Term constVal = args[0];
-    if (!constVal.isValue())
+
+    // To parse array constants taking reals whose values are specified by
+    // rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle
+    // the fact that (/ 1 3) is the division of constants 1 and 3, and not
+    // the resulting constant rational value. Thus, we must construct the
+    // resulting rational here. This also is applied for integral real values
+    // like 5.0 which are converted to (/ 5 1) to distinguish them from
+    // integer constants. We must ensure numerator and denominator are
+    // constant and the denominator is non-zero.
+    if (constVal.getKind() == api::DIVISION)
     {
-      // To parse array constants taking reals whose values are specified by
-      // rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle
-      // the fact that (/ 1 3) is the division of constants 1 and 3, and not
-      // the resulting constant rational value. Thus, we must construct the
-      // resulting rational here. This also is applied for integral real values
-      // like 5.0 which are converted to (/ 5 1) to distinguish them from
-      // integer constants. We must ensure numerator and denominator are
-      // constant and the denominator is non-zero.
-      if (constVal.getKind() == api::DIVISION && constVal[0].isValue()
-          && constVal[1].isValue()
-          && !constVal[1].getExpr().getConst<Rational>().isZero())
-      {
-        std::stringstream sdiv;
-        sdiv << constVal[0] << "/" << constVal[1];
-        constVal = d_solver->mkReal(sdiv.str());
-      }
-      if (!constVal.isValue())
-      {
-        std::stringstream ss;
-        ss << "expected constant term inside array constant, but found "
-           << "nonconstant term:" << std::endl
-           << "the term: " << constVal;
-        parseError(ss.str());
-      }
+      std::stringstream sdiv;
+      sdiv << constVal[0] << "/" << constVal[1];
+      constVal = d_solver->mkReal(sdiv.str());
     }
+
     if (!p.d_type.getArrayElementSort().isComparableTo(constVal.getSort()))
     {
       std::stringstream ss;
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index b99376685..8e29c25f1 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -477,7 +477,7 @@ definedPred[CVC4::ParseOp& p]
       api::Term body =
           MK_TERM(api::AND,
                   MK_TERM(api::NOT,
-                          MK_TERM(api::EQUAL, r, SOLVER->mkReal(0))),
+                          MK_TERM(api::EQUAL, r, SOLVER->mkInteger(0))),
                   MK_TERM(api::EQUAL, qr, MK_TERM(api::MULT, n, rr)));
       api::Term bvl = MK_TERM(api::BOUND_VAR_LIST, q, r);
       body = MK_TERM(api::EXISTS, bvl, body);
@@ -537,7 +537,7 @@ thfDefinedPred[CVC4::ParseOp& p]
       api::Term body = MK_TERM(
           api::AND,
           MK_TERM(api::NOT,
-                  MK_TERM(api::EQUAL, r, SOLVER->mkReal(0))),
+                  MK_TERM(api::EQUAL, r, SOLVER->mkInteger(0))),
           MK_TERM(api::EQUAL, qr, MK_TERM(api::MULT, n, rr)));
       api::Term bvl = MK_TERM(api::BOUND_VAR_LIST, q, r);
       body = MK_TERM(api::EXISTS, bvl, body);
@@ -708,7 +708,7 @@ definedFun[CVC4::ParseOp& p]
                                                   n,
                                                   SOLVER->mkReal(2)),
                                           SOLVER->mkReal(1, 2))),
-                          SOLVER->mkReal(2))));
+                          SOLVER->mkInteger(2))));
       p.d_kind = api::LAMBDA;
       p.d_expr = MK_TERM(api::LAMBDA, formals, expr);
       }
@@ -1747,7 +1747,15 @@ NUMBER
   : ( SIGN[pos]? num=DECIMAL
       { std::stringstream ss;
         ss << ( pos ? "" : "-" ) << AntlrInput::tokenText($num);
-        PARSER_STATE->d_tmp_expr = SOLVER->mkReal(ss.str());
+        std::string str = ss.str();
+        if (str.find(".") == std::string::npos)
+        {
+          PARSER_STATE->d_tmp_expr = SOLVER->mkInteger(str);
+        }
+        else
+        {
+          PARSER_STATE->d_tmp_expr = SOLVER->mkReal(str);
+        }
       }
     | SIGN[pos]? num=DECIMAL DOT den=DECIMAL (EXPONENT SIGN[posE]? e=DECIMAL)?
       {
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index bab619dce..9ccf02301 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -644,6 +644,8 @@ void CvcPrinter::toStream(
       opType = PREFIX;
       break;
     case kind::TO_REAL:
+    case kind::CAST_TO_REAL:
+    {
       if (n[0].getKind() == kind::CONST_RATIONAL)
       {
         // print the constant as a rational
@@ -655,6 +657,7 @@ void CvcPrinter::toStream(
         toStream(out, n[0], depth, types, false);
       }
       return;
+    }
     case kind::DIVISIBLE:
       out << "DIVISIBLE(";
       toStream(out, n[0], depth, types, false);
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8815f9632..a0cd8cf9c 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -477,10 +477,10 @@ void Smt2Printer::toStream(std::ostream& out,
   bool typeChildren = false;  // operators (op t1...tn) where at least one of t1...tn may require a type cast e.g. Int -> Real
   // operator
   Kind k = n.getKind();
-  if(n.getNumChildren() != 0 &&
-     k != kind::INST_PATTERN_LIST &&
-     k != kind::APPLY_TYPE_ASCRIPTION &&
-     k != kind::CONSTRUCTOR_TYPE) {
+  if (n.getNumChildren() != 0 && k != kind::INST_PATTERN_LIST
+      && k != kind::APPLY_TYPE_ASCRIPTION && k != kind::CONSTRUCTOR_TYPE
+      && k != kind::CAST_TO_REAL)
+  {
     out << '(';
   }
   switch(k) {
@@ -603,11 +603,17 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::ABS:
   case kind::IS_INTEGER:
   case kind::TO_INTEGER:
-  case kind::TO_REAL:
   case kind::POW: 
     parametricTypeChildren = true;
     out << smtKindString(k, d_variant) << " ";
     break;
+  case kind::TO_REAL:
+  case kind::CAST_TO_REAL:
+  {
+    // (to_real 5) is printed as 5.0
+    out << n[0] << ".0";
+    return;
+  }
   case kind::IAND:
     out << "(_ iand " << n.getOperator().getConst<IntAnd>().d_size << ") ";
     stillNeedToPrintParams = false;
@@ -1029,7 +1035,8 @@ void Smt2Printer::toStream(std::ostream& out,
       }
     }
   }
-  if(n.getNumChildren() != 0) {
+  if (n.getNumChildren() != 0)
+  {
     out << parens.str() << ')';
   }
 }/* Smt2Printer::toStream(TNode) */
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index dc91d678e..a65fbd961 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -138,7 +138,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
     case kind::TO_INTEGER:
       return RewriteResponse(REWRITE_DONE, t);
     case kind::TO_REAL:
-      return RewriteResponse(REWRITE_DONE, t[0]);
+    case kind::CAST_TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]);
     case kind::POW:
       return RewriteResponse(REWRITE_DONE, t);
     case kind::PI:
@@ -198,7 +198,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
       }
       return RewriteResponse(REWRITE_DONE, t);
     case kind::TO_REAL:
-      return RewriteResponse(REWRITE_DONE, t[0]);
+    case kind::CAST_TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]);
     case kind::TO_INTEGER:
       if(t[0].isConst()) {
         return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(Rational(t[0].getConst<Rational>().floor())));
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index e563d8f66..fc8f76ee4 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -80,9 +80,16 @@ operator LEQ 2 "less than or equal, x <= y"
 operator GT 2 "greater than, x > y"
 operator GEQ 2 "greater than or equal, x >= y"
 
-operator IS_INTEGER 1 "term-is-integer predicate (parameter is a real-sorted term)"
-operator TO_INTEGER 1 "convert term to integer by the floor function (parameter is a real-sorted term)"
-operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term; this is a no-op in CVC4, as integer is a subtype of real)"
+operator IS_INTEGER   1 "term-is-integer predicate (parameter is a real-sorted term)"
+operator TO_INTEGER   1 "convert term to integer by the floor function (parameter is a real-sorted term)"
+operator TO_REAL      1 "cast term to real (parameter is an integer-sorted term; this is a no-op in CVC4, as integer is a subtype of real)"
+
+# CAST_TO_REAL is added to distinguish between integers casted to reals internally, and
+# integers casted to reals or using the API \
+# Solver::mkReal(int val) would return an internal node (CAST_TO_REAL val), but in the api it appears as term (val) \
+# Solver::mkTerm(TO_REAL, Solver::mkInteger(int val)) would return both term and node (TO_REAL val) \
+# This way, we avoid having 2 nested TO_REAL nodess as a result of Solver::mkTerm(TO_REAL, Solver::mkReal(int val))
+operator CAST_TO_REAL 1 "cast term to real same as TO_REAL, but it is used internally, whereas TO_REAL is accessible in the API"
 
 typerule PLUS ::CVC4::theory::arith::ArithOperatorTypeRule
 typerule MULT ::CVC4::theory::arith::ArithOperatorTypeRule
@@ -99,9 +106,10 @@ typerule LEQ "SimpleTypeRule<RBool, AReal, AReal>"
 typerule GT "SimpleTypeRule<RBool, AReal, AReal>"
 typerule GEQ "SimpleTypeRule<RBool, AReal, AReal>"
 
-typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule
-typerule TO_INTEGER ::CVC4::theory::arith::ArithOperatorTypeRule
-typerule IS_INTEGER "SimpleTypeRule<RBool, AReal>"
+typerule TO_REAL      ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule CAST_TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule TO_INTEGER   ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule IS_INTEGER   "SimpleTypeRule<RBool, AReal>"
 
 typerule ABS "SimpleTypeRule<RInteger, AInteger>"
 typerule INTS_DIVISION "SimpleTypeRule<RInteger, AInteger, AInteger>"
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 9dd18d84b..0aa9cd4b3 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -60,12 +60,13 @@ public:
         }
       }
     }
-    switch(Kind k = n.getKind()) {
+    switch (Kind k = n.getKind())
+    {
       case kind::TO_REAL:
-        return realType;
-      case kind::TO_INTEGER:
-        return integerType;
-      default: {
+      case kind::CAST_TO_REAL: return realType;
+      case kind::TO_INTEGER: return integerType;
+      default:
+      {
         bool isDivision = k == kind::DIVISION || k == kind::DIVISION_TOTAL;
         return (isInteger && !isDivision ? integerType : realType);
       }