Add some missing resultants in the coverings solver (#8662)

This PR fixes a subtle corner case in the generalization within the coverings solver. When generalizing a single interval that spans the whole real line (i.e. from -infty to infty) that is based on multiple polynomials (most likely because the origin constraint factored) we did not include their pairwise resultants.
This detail is arguably missing in the paper, or rather hidden in a very vague notion of "performing standard CAD simplifications".
Fixes #8638.

diff --git a/src/theory/arith/nl/coverings/cdcac.cpp b/src/theory/arith/nl/coverings/cdcac.cpp
index e0816cf20e19a672fed49d17d08db209461998ba..6c3f97c6c93b38b4fdbccfa00ff459c4a352140e 100644 (file)
--- a/src/theory/arith/nl/coverings/cdcac.cpp
+++ b/src/theory/arith/nl/coverings/cdcac.cpp
@@ -353,6 +353,14 @@ PolyVector CDCAC::constructCharacterization(std::vector<CACInterval>& intervals)
       // Add all discriminants
       res.add(discriminant(p));
 
+      // Add pairwise resultants
+      for (const auto& q : i.d_mainPolys)
+      {
+        // avoid symmetric duplicates
+        if (p >= q) continue;
+        res.add(resultant(p, q));
+      }
+
       for (const auto& q : requiredCoefficients(p))
       {
         // Add all required coefficients

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index d94adb44f1cefcd305661c50af55bdf92eeb9910..464304bcbc2b6ffe8b75637aa96af1fe7300f80d 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -806,6 +806,7 @@ set(regress_0_tests
   regress0/nl/issue8414-ran-rational.smt2
   regress0/nl/issue8515-cov-iand.smt2
   regress0/nl/issue8516-cov-sin.smt2
+  regress0/nl/issue8638-cov-resultants.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/issue8638-cov-resultants.smt2 b/test/regress/cli/regress0/nl/issue8638-cov-resultants.smt2
new file mode 100644 (file)
index 0000000..92d4408
--- /dev/null
+++ b/test/regress/cli/regress0/nl/issue8638-cov-resultants.smt2
@@ -0,0 +1,10 @@
+; REQUIRES: poly
+; EXPECT: sat
+(set-logic QF_NRA)
+(declare-fun y () Real)
+(declare-fun p () Real)
+(declare-fun c () Real)
+(assert (< 1 c))
+(assert (< 0.0 (/ (+ y p 1.0) c)))
+(assert (and (> (* y y y y) 0) (> (* y y y p) 0)))
+(check-sat)
\ No newline at end of file