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.

1 files changed, 12 insertions, 0 deletions

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);
   }