Fix type rule for to_real (#6257)

This fixes the type rule for to_real to match SMT-LIB: its argument must be an integer.

This required fixing the TPTP parser which has a more relaxed semantics for to_real / to_rat.

This also fixes Solver::isReal, which should return false if we are the integer type.

Fixes #6208.

3 files changed, 21 insertions, 3 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 9e55cdaf0..f304ae5a0 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1087,7 +1087,8 @@ bool Sort::isReal() const
 {
   CVC4_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
-  return d_type->isReal();
+  // notice that we do not expose internal subtyping to the user
+  return d_type->isReal() && !d_type->isInteger();
   ////////
   CVC4_API_TRY_CATCH_END;
 }
@@ -4432,7 +4433,7 @@ Term Solver::ensureTermSort(const Term& term, const Sort& sort) const
   }
 
   // Integers are reals, too
-  Assert(t.isReal());
+  Assert(t.d_type->isReal());
   Term res = term;
   if (t.isInteger())
   {
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 136319225..7a3a47ec9 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -340,6 +340,18 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     {
       return d_solver->mkTerm(api::UMINUS, args[0]);
     }
+    if (kind == api::TO_REAL)
+    {
+      // If the type is real, this is a no-op. We require this special
+      // case in the TPTP parser since TO_REAL is designed to match the
+      // SMT-LIB operator, meaning it can only be applied to integers, whereas
+      // the TPTP to_real / to_rat do not have the same semantics.
+      api::Sort s = args[0].getSort();
+      if (s.isReal())
+      {
+        return args[0];
+      }
+    }
     return d_solver->mkTerm(kind, args);
   }
 
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index e192270ff..e8769064a 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -46,6 +46,7 @@ public:
     TNode::iterator child_it = n.begin();
     TNode::iterator child_it_end = n.end();
     bool isInteger = true;
+    Kind k = n.getKind();
     for(; child_it != child_it_end; ++child_it) {
       TypeNode childType = (*child_it).getType(check);
       if (!childType.isInteger()) {
@@ -58,9 +59,13 @@ public:
         if(!childType.isReal()) {
           throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic subterm");
         }
+        if (k == kind::TO_REAL && !childType.isInteger())
+        {
+          throw TypeCheckingExceptionPrivate(n, "expecting an integer subterm");
+        }
       }
     }
-    switch (Kind k = n.getKind())
+    switch (k)
     {
       case kind::TO_REAL:
       case kind::CAST_TO_REAL: return realType;