From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Tue, 26 Apr 2022 17:17:23 +0000 (-0700)
Subject: Add some missing resultants in the coverings solver (#8662)
X-Git-Tag: cvc5-1.0.1~222
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=255d19b17351335bfec73ecc10d5c40770a3f17b;p=cvc5.git

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 e0816cf20..6c3f97c6c 100644
--- 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 d94adb44f..464304bcb 100644
--- 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
index 000000000..92d4408cf
--- /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