From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 30 Jun 2022 04:54:56 +0000 (-0500)
Subject: Fix type issue in substitutions from covering solver (#8921)
X-Git-Tag: cvc5-1.0.1~25
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c501613c172412b579884b37ed3133a8bbb06f09;p=cvc5.git

Fix type issue in substitutions from covering solver (#8921)

Fixes #8895. The benchmark in that issue now times out.
---

diff --git a/src/theory/arith/nl/coverings_solver.cpp b/src/theory/arith/nl/coverings_solver.cpp
index dcc3cff94..23b773792 100644
--- a/src/theory/arith/nl/coverings_solver.cpp
+++ b/src/theory/arith/nl/coverings_solver.cpp
@@ -249,9 +249,19 @@ void CoveringsSolver::addToModel(TNode var, TNode value) const
   // reductions inference of the sine solver) may have introduced substitutions
   // internally during check.
   Node svalue = d_model.getSubstitutedForm(value);
-  if (var.getType().isInteger() && svalue.getKind() == Kind::TO_REAL)
+  // ensure the value has integer type if var has integer type
+  if (var.getType().isInteger())
   {
-    svalue = svalue[0];
+    if (svalue.getKind() == Kind::TO_REAL)
+    {
+      svalue = svalue[0];
+    }
+    else if (svalue.getKind() == Kind::CONST_RATIONAL)
+    {
+      Assert(svalue.getConst<Rational>().isIntegral());
+      svalue =
+          NodeManager::currentNM()->mkConstInt(svalue.getConst<Rational>());
+    }
   }
   Trace("nl-cov") << "-> " << var << " = " << svalue << std::endl;
   d_model.addSubstitution(var, svalue);
diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index 4dcade099..b0a498dc9 100644
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -274,6 +274,8 @@ bool NlModel::addSubstitution(TNode v, TNode s)
                         << std::endl;
   Assert(getSubstitutedForm(s) == s)
       << "Added a substitution whose range is not in substituted form " << s;
+  // cannot substitute real for integer
+  Assert(v.getType().isReal() || s.getType().isInteger());
   // should not substitute the same variable twice
   // should not set exact bound more than once
   if (d_substitutions.contains(v))
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 080a47d48..e47abdac7 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -337,7 +337,8 @@ bool TheoryArith::collectModelValues(TheoryModel* m,
       continue;
     }
     // maps to constant of same type
-    Assert(p.first.getType() == p.second.getType());
+    Assert(p.first.getType() == p.second.getType())
+        << "Bad type : " << p.first << " -> " << p.second;
     if (m->assertEquality(p.first, p.second, true))
     {
       continue;
@@ -438,7 +439,8 @@ bool TheoryArith::sanityCheckIntegerModel()
   {
     for (CVC5_UNUSED const auto& p : d_arithModelCache)
     {
-      Assert(p.first.getType() == p.second.getType());
+      Assert(p.first.getType() == p.second.getType())
+          << "Bad type: " << p.first << " -> " << p.second;
     }
   }
   bool addedLemma = false;