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 9e55cdaf03c5f3a3aeb8a4ec257baffd058e21d6..f304ae5a063511311affe0c2c13aeffba02a6a91 100644 (file)
--- 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 136319225a54e75ef6bd116972b95b905b52a4ad..7a3a47ec9823795f0188e4396fac903982edb253 100644 (file)
--- 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 e192270ffee9b527fce48572afab6bfac2c23971..e8769064a8e785e5ebae6c65b462902711628a3a 100644 (file)
--- 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 e0507e74972065b3081065395cf85faea60ef7bc..fa4b1cc9d87d5c59b97204482a6c0ab6cbae2a21 100644 (file)
--- 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());
 }