Be permissive for subtyping in function definitions (#8568)

This is to accommodate the Real theory in SMT-LIB, which says that numerals specify reals.

Instead of making our parser for numerals dependent on the logic, we are more permissive.

This fixes several spurious parsing issues in smtlib.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 610330b76d26a783af8df5f241e3597eb6054f5d..ec4585c2ce06b98d6b6ba629ea9bd870ee17c25c 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -6399,7 +6399,12 @@ Term Solver::defineFun(const std::string& symbol,
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort);
   CVC5_API_SOLVER_CHECK_TERM(term);
-  CVC5_API_CHECK(term.getSort() == sort)
+  // We are permissive with subtypes so that integers are allowed to define
+  // the body of a function whose codomain is real. This is to accomodate
+  // SMT-LIB inputs in the Reals theory, where NUMERAL can be used to specify
+  // reals. Instead of making our parser for numerals dependent on the logic,
+  // we instead allow integers here in this case.
+  CVC5_API_CHECK(term.d_node->getType().isSubtypeOf(*sort.d_type))
       << "Invalid sort of function body '" << term << "', expected '" << sort
       << "'";
 
@@ -6443,7 +6448,8 @@ Term Solver::defineFunRec(const std::string& symbol,
 
   CVC5_API_SOLVER_CHECK_TERM(term);
   CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort);
-  CVC5_API_CHECK(sort == term.getSort())
+  // we are permissive with subtypes, similar to defineFun
+  CVC5_API_CHECK(term.d_node->getType().isSubtypeOf(*sort.d_type))
       << "Invalid sort of function body '" << term << "', expected '" << sort
       << "'";
 
@@ -6492,7 +6498,8 @@ Term Solver::defineFunRec(const Term& fun,
     std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
     CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun, bound_vars, domain_sorts);
     Sort codomain = fun.getSort().getFunctionCodomainSort();
-    CVC5_API_CHECK(codomain == term.getSort())
+    // we are permissive with subtypes, similar to defineFun
+    CVC5_API_CHECK(codomain.d_type->isSubtypeOf(term.d_node->getType()))
         << "Invalid sort of function body '" << term << "', expected '"
         << codomain << "'";
   }

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 71d41259679d386938c584db2cece2d2e7049ebc..86fcbac906add60b3908b7e06461137f37a21ab7 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -887,6 +887,7 @@ set(regress_0_tests
   regress0/parser/named-attr.smt2
   regress0/parser/proj-issue370-push-pop-global.smt2
   regress0/parser/quoted-define-fun.smt2
+  regress0/parser/real-numerals.smt2
   regress0/parser/shadow_fun_symbol_all.smt2
   regress0/parser/shadow_fun_symbol_nirat.smt2
   regress0/parser/strings20.smt2

diff --git a/test/regress/cli/regress0/parser/real-numerals.smt2 b/test/regress/cli/regress0/parser/real-numerals.smt2
new file mode 100644 (file)
index 0000000..59e00b1
--- /dev/null
+++ b/test/regress/cli/regress0/parser/real-numerals.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_NRA)
+(set-info :status sat)
+; note according to SMT-LIB, a NUMERAL specifies a Real when the logic contains reals but not ints
+(define-fun x () Real 0)
+(assert (<= (- 1) x 3))
+(check-sat)