From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Tue, 31 May 2022 19:28:52 +0000 (-0700)
Subject: Fix issues with to_real around coverings solver (#8837)
X-Git-Tag: cvc5-1.0.1~83
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=00ad2144c5f8717a84b1b6765a33744116f9bc9f;p=cvc5.git

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 9311c11fe..dcc3cff94 100644
--- 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 fcc10ec61..943f07ed2 100644
--- 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 fad3a997e..836ea5ba6 100644
--- 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 d8bdbe278..2d255d24c 100644
--- 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 614d5fc1b..5dd9a3342 100644
--- 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
index 000000000..313c68c26
--- /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)