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.

1 files changed, 15 insertions, 15 deletions

diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index ca47e3ea0..dba7ccbe3 100644
--- 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);