Fix issues with to_real around coverings solver (#8837)

This PR fixes two issues with the (missing) handling of to_real.
The first is that equality substitution was not aware of to_real yet, possible introducing models for both x and (to_real x).
The second is that the conversion to libpoly polynomials would also not properly unpack to_real expressions.
Fixes #8835.

diff --git a/src/theory/arith/nl/coverings_solver.cpp b/src/theory/arith/nl/coverings_solver.cpp
index 9311c11fe6ae04fb2bbd9903916d73ffe826d245..dcc3cff945529895b78c31c8865e0c8e0dbee21a 100644 (file)
--- a/src/theory/arith/nl/coverings_solver.cpp
+++ b/src/theory/arith/nl/coverings_solver.cpp
@@ -249,6 +249,10 @@ 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)
+  {
+    svalue = svalue[0];
+  }
   Trace("nl-cov") << "-> " << var << " = " << svalue << std::endl;
   d_model.addSubstitution(var, svalue);
 }

diff --git a/src/theory/arith/nl/equality_substitution.cpp b/src/theory/arith/nl/equality_substitution.cpp
index fcc10ec614971e169659f0d948f46a6921461301..943f07ed2e99013813635c1964930b4ac65d4817 100644 (file)
--- a/src/theory/arith/nl/equality_substitution.cpp
+++ b/src/theory/arith/nl/equality_substitution.cpp
@@ -83,8 +83,8 @@ std::vector<Node> EqualitySubstitution::eliminateEqualities(
       Assert(o.getNumChildren() == 2);
       for (size_t i = 0; i < 2; ++i)
       {
-        const auto& l = o[i];
-        const auto& r = o[1 - i];
+        const auto& l = (o[i].getKind() == Kind::TO_REAL ? o[i][0] : o[i]);
+        const auto& r = (o[1-i].getKind() == Kind::TO_REAL ? o[1-i][0] : o[1-i]);
         // lhs can't be constant
         if (l.isConst()) continue;
         // types must match (otherwise we might have int/real issues)

diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp
index fad3a997e5826938771d5490cd7b5b0e7111a062..836ea5ba638091b7220074851d32fc74cf61e7a8 100644 (file)
--- a/src/theory/arith/nl/poly_conversion.cpp
+++ b/src/theory/arith/nl/poly_conversion.cpp
@@ -88,10 +88,11 @@ cvc5::internal::Node as_cvc_upolynomial(const poly::UPolynomial& p, const cvc5::
   return res;
 }
 
-poly::UPolynomial as_poly_upolynomial_impl(const cvc5::internal::Node& n,
+poly::UPolynomial as_poly_upolynomial_impl(cvc5::internal::Node n,
                                            poly::Integer& denominator,
                                            const cvc5::internal::Node& var)
 {
+  if (n.getKind() == Kind::TO_REAL) n = n[0];
   denominator = poly::Integer(1);
   if (n.isVar())
   {
@@ -148,10 +149,11 @@ poly::UPolynomial as_poly_upolynomial(const cvc5::internal::Node& n,
   return as_poly_upolynomial_impl(n, denom, var);
 }
 
-poly::Polynomial as_poly_polynomial_impl(const cvc5::internal::Node& n,
+poly::Polynomial as_poly_polynomial_impl(cvc5::internal::Node n,
                                          poly::Integer& denominator,
                                          VariableMapper& vm)
 {
+  if (n.getKind() == Kind::TO_REAL) n = n[0];
   denominator = poly::Integer(1);
   if (n.isVar())
   {

diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h
index d8bdbe278c5e388a9eb016713cd2992ef013d482..2d255d24c91e2415648f46b0b2dcece94550c5a4 100644 (file)
--- a/src/theory/arith/nl/poly_conversion.h
+++ b/src/theory/arith/nl/poly_conversion.h
@@ -55,7 +55,10 @@ struct VariableMapper
 cvc5::internal::Node as_cvc_upolynomial(const poly::UPolynomial& p,
                               const cvc5::internal::Node& var);
 
-/** Convert a cvc5::internal::Node to a poly univariate polynomial. */
+/**
+ * Convert a cvc5::internal::Node to a poly univariate polynomial. Is robust to
+ * n being a `Kind::TO_REAL` wrapper node.
+ */
 poly::UPolynomial as_poly_upolynomial(const cvc5::internal::Node& n,
                                       const cvc5::internal::Node& var);
 
@@ -71,6 +74,7 @@ poly::UPolynomial as_poly_upolynomial(const cvc5::internal::Node& n,
  * (like in the context of coverings). If we need the actual polynomial (for example
  * in the context of ICP) the second overload provides the denominator in the
  * third argument.
+ * The method is robust to n being a `Kind::TO_REAL` wrapper node.
  */
 poly::Polynomial as_poly_polynomial(const cvc5::internal::Node& n, VariableMapper& vm);
 poly::Polynomial as_poly_polynomial(const cvc5::internal::Node& n,

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 614d5fc1be3fc15bbdd3661ec5dba2702c80184f..5dd9a3342ec0d87a4c000213635249712af88f04 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -824,6 +824,7 @@ set(regress_0_tests
   regress0/nl/issue8744-real.smt2
   regress0/nl/issue8744-real-cov.smt2
   regress0/nl/issue8755-nl-logic-exception.smt2
+  regress0/nl/issue8835-int-second.smt2
   regress0/nl/lazard-spurious-root.smt2
   regress0/nl/magnitude-wrong-1020-m.smt2
   regress0/nl/mult-po.smt2

diff --git a/test/regress/cli/regress0/nl/issue8835-int-second.smt2 b/test/regress/cli/regress0/nl/issue8835-int-second.smt2
new file mode 100644 (file)
index 0000000..313c68c
--- /dev/null
+++ b/test/regress/cli/regress0/nl/issue8835-int-second.smt2
@@ -0,0 +1,10 @@
+; EXPECT: sat
+; REQUIRES: poly
+(set-logic ALL)
+(set-option :nl-cov true)
+(set-option :check-models true)
+(declare-fun a () Int) 
+(declare-fun b () Int) 
+(declare-fun c () Real) 
+(assert (= (* 1 (/ 1 69)) (+ b 1 (* b (* (* 2 c) a)) (- 1)))) 
+(check-sat)