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 3a53da94bc2a6d1321854f40e3046b141ee91b6a..fcc10ec614971e169659f0d948f46a6921461301 100644 (file)
--- 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 7901da1c03fd9cb52a5469bbabc73f68e59d6281..57fe6bf721c445cc84c8e6b2a0b166c26b344862 100644 (file)
--- 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 (file)
index 0000000..80e9009
--- /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 (file)
index 0000000..16d3f8b
--- /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 (file)
index 0000000..3c3fee9
--- /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