From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 5 Mar 2020 20:38:16 +0000 (-0600)
Subject: Fix issues with real to int (#3918)
X-Git-Tag: cvc5-1.0.0~3567
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d26ee67911fedfef966a0e4d64ffda02007d65a0;p=cvc5.git

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 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);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 34f7a8713..a7d931246 100644
--- 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
index 000000000..ad6ba3b33
--- /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
+; EXPECT: sat
+(set-logic UFNIA)
+(set-option :incremental true)
+(set-option :check-models true)
+(set-option :solve-real-as-int true)
+(declare-const v0 Bool)
+(declare-const v1 Bool)
+(declare-const v2 Bool)
+(declare-const v3 Bool)
+(declare-const v4 Bool)
+(declare-const v5 Bool)
+(declare-const v6 Bool)
+(declare-const v7 Bool)
+(declare-const v8 Bool)
+(declare-const v9 Bool)
+(declare-const v10 Bool)
+(declare-const v11 Bool)
+(declare-const v12 Bool)
+(declare-const v13 Bool)
+(declare-const v14 Bool)
+(declare-const i1 Int)
+(assert (forall ((q0 Int) (q1 Int) (q2 Int) (q3 Bool)) (=> (= v7 q3 v7 q3 v0 q3 q3 q3 q3 v3) (> q0 59))))
+(push 1)
+(declare-const v15 Bool)
+(declare-sort S0 0)
+(declare-sort S1 0)
+(declare-const i2 Int)
+(assert v13)
+(push 1)
+(declare-const S1-0 S1)
+(assert (forall ((q4 Int)) (not (distinct q4 q4))))
+(check-sat)
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
index 000000000..5d7b8d44e
--- /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)