Allow mixed int/real equalities in non-strict parsing mode (#8865)

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index cbf699f6b3ac787703f2f933b4160caf85483663..122f7dbba892c220b94b76e79f06c0172b1f45b1 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1149,17 +1149,39 @@ cvc5::Term Smt2::applyParseOp(ParseOp& p, std::vector<cvc5::Term>& args)
   }
   else if (isBuiltinOperator)
   {
-    if (!isHoEnabled() && (kind == cvc5::EQUAL || kind == cvc5::DISTINCT))
+    if (kind == cvc5::EQUAL || kind == cvc5::DISTINCT)
     {
+      bool isReal = false;
       // need hol if these operators are applied over function args
-      for (std::vector<cvc5::Term>::iterator i = args.begin(); i != args.end();
-           ++i)
+      for (const Term& i : args)
       {
-        if ((*i).getSort().isFunction())
+        Sort s = i.getSort();
+        if (!isHoEnabled())
         {
-          parseError(
-              "Cannot apply equality to functions unless logic is prefixed by "
-              "HO_.");
+          if (s.isFunction())
+          {
+            parseError(
+                "Cannot apply equality to functions unless logic is prefixed "
+                "by HO_.");
+          }
+        }
+        if (s.isReal())
+        {
+          isReal = true;
+        }
+      }
+      // If strict mode is not enabled, we are permissive for Int and Real
+      // subtyping. Note that other arithmetic operators and relations are
+      // already permissive, e.g. <=, +.
+      if (isReal && !strictModeEnabled())
+      {
+        for (Term& i : args)
+        {
+          Sort s = i.getSort();
+          if (s.isInteger())
+          {
+            i = d_solver->mkTerm(cvc5::TO_REAL, {i});
+          }
         }
       }
     }
@@ -1197,14 +1219,7 @@ cvc5::Term Smt2::applyParseOp(ParseOp& p, std::vector<cvc5::Term>& args)
                       << std::endl;
       return ret;
     }
-    if (kind == cvc5::SET_SINGLETON && args.size() == 1)
-    {
-      cvc5::Term ret = d_solver->mkTerm(cvc5::SET_SINGLETON, {args[0]});
-      Trace("parser") << "applyParseOp: return set.singleton " << ret
-                      << std::endl;
-      return ret;
-    }
-    else if (kind == cvc5::CARDINALITY_CONSTRAINT)
+    if (kind == cvc5::CARDINALITY_CONSTRAINT)
     {
       if (args.size() != 2)
       {

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 763270a6f9776b1340b213877b2ad623f12e77c1..4a11a6f2fdb21b360af5c7e31bde057d5c43e5a5 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -915,6 +915,7 @@ set(regress_0_tests
   regress0/parser/linear_arithmetic_err3.smt2
   regress0/parser/named-attr-error.smt2
   regress0/parser/named-attr.smt2
+  regress0/parser/non-strict-real-vs-int.smt2 
   regress0/parser/proj-issue370-push-pop-global.smt2
   regress0/parser/quoted-define-fun.smt2
   regress0/parser/real-numerals.smt2

diff --git a/test/regress/cli/regress0/parser/non-strict-real-vs-int.smt2 b/test/regress/cli/regress0/parser/non-strict-real-vs-int.smt2
new file mode 100644 (file)
index 0000000..84122e8
--- /dev/null
+++ b/test/regress/cli/regress0/parser/non-strict-real-vs-int.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --no-strict-parsing
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () Real)
+(assert (= x 10))
+(assert (<= (+ x 1) 20))
+(check-sat)