From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 1 Apr 2021 20:44:34 +0000 (-0500)
Subject: Fix type rule for to_real (#6257)
X-Git-Tag: cvc5-1.0.0~1988
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=71699a551d207ab373c733d8ea83a5b071ed99ee;p=cvc5.git

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.
---

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;
diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp
index e0507e749..fa4b1cc9d 100644
--- a/test/unit/api/sort_black.cpp
+++ b/test/unit/api/sort_black.cpp
@@ -71,12 +71,14 @@ TEST_F(TestApiBlackSort, isBoolean)
 TEST_F(TestApiBlackSort, isInteger)
 {
   ASSERT_TRUE(d_solver.getIntegerSort().isInteger());
+  ASSERT_TRUE(!d_solver.getRealSort().isInteger());
   ASSERT_NO_THROW(Sort().isInteger());
 }
 
 TEST_F(TestApiBlackSort, isReal)
 {
   ASSERT_TRUE(d_solver.getRealSort().isReal());
+  ASSERT_TRUE(!d_solver.getIntegerSort().isReal());
   ASSERT_NO_THROW(Sort().isReal());
 }