From 255d19b17351335bfec73ecc10d5c40770a3f17b Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 26 Apr 2022 10:17:23 -0700 Subject: [PATCH] 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. --- src/theory/arith/nl/coverings/cdcac.cpp | 8 ++++++++ test/regress/cli/CMakeLists.txt | 1 + .../cli/regress0/nl/issue8638-cov-resultants.smt2 | 10 ++++++++++ 3 files changed, 19 insertions(+) create mode 100644 test/regress/cli/regress0/nl/issue8638-cov-resultants.smt2 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& 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 -- 2.30.2