From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Tue, 10 May 2022 21:23:20 +0000 (-0700)
Subject: Ensure substitutions in nonlinear solver are properly typed (#8748)
X-Git-Tag: cvc5-1.0.1~148
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b47d65698b514cfbe353182cab8e4261d74a020e;p=cvc5.git

Ensure substitutions in nonlinear solver are properly typed (#8748)

We would apply substitutions between int and real terms, effectively hiding the intness of variables from the coverings solver.
Fixes #8744.
The example from #8744 times out after the fix, thus no regression.
---

diff --git a/src/theory/arith/nl/equality_substitution.cpp b/src/theory/arith/nl/equality_substitution.cpp
index 3a53da94b..fcc10ec61 100644
--- a/src/theory/arith/nl/equality_substitution.cpp
+++ b/src/theory/arith/nl/equality_substitution.cpp
@@ -85,10 +85,17 @@ std::vector<Node> EqualitySubstitution::eliminateEqualities(
       {
         const auto& l = o[i];
         const auto& r = o[1 - i];
+        // lhs can't be constant
         if (l.isConst()) continue;
+        // types must match (otherwise we might have int/real issues)
+        if (r.getType() != l.getType()) continue;
+        // can't substitute stuff from other theories
         if (!Theory::isLeafOf(l, TheoryId::THEORY_ARITH)) continue;
+        // can't substitute the same thing twice
         if (d_substitutions->hasSubstitution(l)) continue;
+        // lhs can't be a subexpression of rhs, would leaf to recursion
         if (expr::hasSubterm(r, l)) continue;
+        // the same, but after substitution
         d_substitutions->invalidateCache();
         if (expr::hasSubterm(d_substitutions->apply(r, nullptr, nullptr, &stc), l)) continue;
         Trace("nl-eqs") << "Found substitution " << l << " -> " << r
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 7901da1c0..57fe6bf72 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -815,6 +815,9 @@ set(regress_0_tests
   regress0/nl/issue8691-3-msum-subtypes.smt2
   regress0/nl/issue8692-idem-flatten.smt2
   regress0/nl/issue8712-div-toreal-rew.smt2
+  regress0/nl/issue8744-int.smt2
+  regress0/nl/issue8744-real.smt2
+  regress0/nl/issue8744-real-cov.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/issue8744-int.smt2 b/test/regress/cli/regress0/nl/issue8744-int.smt2
new file mode 100644
index 000000000..80e9009e9
--- /dev/null
+++ b/test/regress/cli/regress0/nl/issue8744-int.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic NIRA)
+(declare-const x Bool)
+(declare-fun v () Int)
+(declare-fun r () Int)
+(assert (forall ((a Int)) (= (< v r) (= (= 0 (/ r v)) (distinct x (> (- r) 1))))))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/cli/regress0/nl/issue8744-real-cov.smt2 b/test/regress/cli/regress0/nl/issue8744-real-cov.smt2
new file mode 100644
index 000000000..16d3f8b70
--- /dev/null
+++ b/test/regress/cli/regress0/nl/issue8744-real-cov.smt2
@@ -0,0 +1,9 @@
+; REQUIRES: poly
+; COMMAND-LINE: -q --nl-cov
+; EXPECT: sat
+(set-logic NIRA)
+(declare-const x Bool)
+(declare-fun v () Real)
+(declare-fun r () Real)
+(assert (forall ((a Real)) (= (< v r) (= (= 0 (/ r v)) (distinct x (> (- r) 1))))))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/cli/regress0/nl/issue8744-real.smt2 b/test/regress/cli/regress0/nl/issue8744-real.smt2
new file mode 100644
index 000000000..3c3fee924
--- /dev/null
+++ b/test/regress/cli/regress0/nl/issue8744-real.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic NIRA)
+(declare-const x Bool)
+(declare-fun v () Real)
+(declare-fun r () Real)
+(assert (forall ((a Real)) (= (< v r) (= (= 0 (/ r v)) (distinct x (> (- r) 1))))))
+(check-sat)
\ No newline at end of file