Fix issues with real to int (#3918)

This fixes a few issues in the real to int preprocessing pass. Previously it was not robust to cases where the input had constraints that were not over the reals.

Fixes #3915 and fixes #3913 and fixes #3916.

diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index ca47e3ea04b593d59679f463468f608d4395bcc7..dba7ccbe3d3e823518c89b2bc2fad6ceb9c28b22 100644 (file)
--- a/src/preprocessing/passes/real_to_int.cpp
+++ b/src/preprocessing/passes/real_to_int.cpp
@@ -38,13 +38,13 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
   }
   else
   {
+    NodeManager* nm = NodeManager::currentNM();
     Node ret = n;
     if (n.getNumChildren() > 0)
     {
-      if (n.getKind() == kind::EQUAL || n.getKind() == kind::GEQ
-          || n.getKind() == kind::LT
-          || n.getKind() == kind::GT
-          || n.getKind() == kind::LEQ)
+      if ((n.getKind() == kind::EQUAL && n[0].getType().isReal())
+          || n.getKind() == kind::GEQ || n.getKind() == kind::LT
+          || n.getKind() == kind::GT || n.getKind() == kind::LEQ)
       {
         ret = Rewriter::rewrite(n);
         Trace("real-as-int-debug") << "Now looking at : " << ret << std::endl;
@@ -137,11 +137,6 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
             Trace("real-as-int") << "   " << n << std::endl;
             Trace("real-as-int") << "   " << ret << std::endl;
           }
-          else
-          {
-            throw TypeCheckingException(
-                n.toExpr(), string("Cannot translate to Int: ") + n.toString());
-          }
         }
       }
       else
@@ -162,14 +157,19 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
     }
     else
     {
-      if (n.isVar())
+      TypeNode tn = n.getType();
+      if (tn.isReal() && !tn.isInteger())
       {
-        if (!n.getType().isInteger())
+        if (n.getKind() == kind::BOUND_VARIABLE)
+        {
+          // special case for bound variables (must call mkBoundVar)
+          ret = nm->mkBoundVar(nm->integerType());
+        }
+        else if (n.isVar())
         {
-          ret = NodeManager::currentNM()->mkSkolem(
-              "__realToIntInternal_var",
-              NodeManager::currentNM()->integerType(),
-              "Variable introduced in realToIntInternal pass");
+          ret = nm->mkSkolem("__realToIntInternal_var",
+                             nm->integerType(),
+                             "Variable introduced in realToIntInternal pass");
           var_eq.push_back(n.eqNode(ret));
           TheoryModel* m = d_preprocContext->getTheoryEngine()->getModel();
           m->addSubstitution(n, ret);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 34f7a87130e44f9a647c85141b6d3664c5323415..a7d93124678c2948fc0c0ddabcbde816a1c3da6d 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -682,6 +682,7 @@ set(regress_0_tests
   regress0/push-pop/incremental-subst-bug.cvc
   regress0/push-pop/issue1986.smt2
   regress0/push-pop/issue2137.min.smt2
+  regress0/push-pop/issue3915-real-as-int.smt2
   regress0/push-pop/quant-fun-proc-unfd.smt2
   regress0/push-pop/simple_unsat_cores.smt2
   regress0/push-pop/test.00.cvc
@@ -1508,6 +1509,7 @@ set(regress_1_tests
   regress1/quantifiers/qe.smt2
   regress1/quantifiers/quant-wf-int-ind.smt2
   regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2
+  regress1/quantifiers/real-to-int-quant.smt2
   regress1/quantifiers/recfact.cvc
   regress1/quantifiers/rel-trigger-unusable.smt2
   regress1/quantifiers/repair-const-nterm.smt2

diff --git a/test/regress/regress0/push-pop/issue3915-real-as-int.smt2 b/test/regress/regress0/push-pop/issue3915-real-as-int.smt2
new file mode 100644 (file)
index 0000000..ad6ba3b
--- /dev/null
+++ b/test/regress/regress0/push-pop/issue3915-real-as-int.smt2
@@ -0,0 +1,33 @@
+; COMMAND-LINE: --incremental --check-models --solve-real-as-int\r
+; EXPECT: sat\r
+(set-logic UFNIA)\r
+(set-option :incremental true)\r
+(set-option :check-models true)\r
+(set-option :solve-real-as-int true)\r
+(declare-const v0 Bool)\r
+(declare-const v1 Bool)\r
+(declare-const v2 Bool)\r
+(declare-const v3 Bool)\r
+(declare-const v4 Bool)\r
+(declare-const v5 Bool)\r
+(declare-const v6 Bool)\r
+(declare-const v7 Bool)\r
+(declare-const v8 Bool)\r
+(declare-const v9 Bool)\r
+(declare-const v10 Bool)\r
+(declare-const v11 Bool)\r
+(declare-const v12 Bool)\r
+(declare-const v13 Bool)\r
+(declare-const v14 Bool)\r
+(declare-const i1 Int)\r
+(assert (forall ((q0 Int) (q1 Int) (q2 Int) (q3 Bool)) (=> (= v7 q3 v7 q3 v0 q3 q3 q3 q3 v3) (> q0 59))))\r
+(push 1)\r
+(declare-const v15 Bool)\r
+(declare-sort S0 0)\r
+(declare-sort S1 0)\r
+(declare-const i2 Int)\r
+(assert v13)\r
+(push 1)\r
+(declare-const S1-0 S1)\r
+(assert (forall ((q4 Int)) (not (distinct q4 q4))))\r
+(check-sat)\r

diff --git a/test/regress/regress1/quantifiers/real-to-int-quant.smt2 b/test/regress/regress1/quantifiers/real-to-int-quant.smt2
new file mode 100644 (file)
index 0000000..5d7b8d4
--- /dev/null
+++ b/test/regress/regress1/quantifiers/real-to-int-quant.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --solve-real-as-int
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(assert (forall ((x Real) (y Real)) (=> (< x y) (exists ((z Real)) (and (< x z) (< z (+ y 2)))))) )
+(check-sat)