diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-08-14 14:01:57 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-14 07:01:57 -0500 |
commit | 7b7246935910173c67917ee947639ac8ab450edc (patch) | |
tree | 08f83ed8c366e1c24e8d5a1ba451e8d3a4aceb22 /src/theory/arith | |
parent | 02fa1dea5a8335a6bd5a1f3e8718796a9489ac8e (diff) |
Inspect roots to avoid certain resultants (Algorithm 4, lines 8,9). (#4892)
This PR adds a small improvement to the CAD solver.
In Algorithm 4 of https://arxiv.org/pdf/2003.05633.pdf in lines 8 and 9, we only consider polynomials for resultant computations that have roots outside of the current interval.
This PR implements this check.
Fixes CVC4/cvc4-projects#210.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/nl/cad/cdcac.cpp | 24 | ||||
-rw-r--r-- | src/theory/arith/nl/cad/cdcac.h | 11 |
2 files changed, 33 insertions, 2 deletions
diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp index 907f7a7b6..4725eb198 100644 --- a/src/theory/arith/nl/cad/cdcac.cpp +++ b/src/theory/arith/nl/cad/cdcac.cpp @@ -170,18 +170,20 @@ std::vector<poly::Polynomial> CDCAC::constructCharacterization( Trace("cdcac") << "Coeff of " << p << " -> " << q << std::endl; addPolynomial(res, q); } - // TODO(cvc4-projects #210): Only add if p(s \times a) = 0 for some a <= l for (const auto& q : i.d_lowerPolys) { if (p == q) continue; + // Check whether p(s \times a) = 0 for some a <= l + if (!hasRootBelow(q, get_lower(i.d_interval))) continue; Trace("cdcac") << "Resultant of " << p << " and " << q << " -> " << resultant(p, q) << std::endl; addPolynomial(res, resultant(p, q)); } - // TODO(cvc4-projects #210): Only add if p(s \times a) = 0 for some a >= u for (const auto& q : i.d_upperPolys) { if (p == q) continue; + // Check whether p(s \times a) = 0 for some a >= u + if (!hasRootAbove(q, get_upper(i.d_interval))) continue; Trace("cdcac") << "Resultant of " << p << " and " << q << " -> " << resultant(p, q) << std::endl; addPolynomial(res, resultant(p, q)); @@ -419,6 +421,24 @@ CACInterval CDCAC::buildIntegralityInterval(std::size_t cur_variable, {}}; } +bool CDCAC::hasRootAbove(const poly::Polynomial& p, + const poly::Value& val) const +{ + auto roots = poly::isolate_real_roots(p, d_assignment); + return std::any_of(roots.begin(), roots.end(), [&val](const poly::Value& r) { + return r >= val; + }); +} + +bool CDCAC::hasRootBelow(const poly::Polynomial& p, + const poly::Value& val) const +{ + auto roots = poly::isolate_real_roots(p, d_assignment); + return std::any_of(roots.begin(), roots.end(), [&val](const poly::Value& r) { + return r <= val; + }); +} + } // namespace cad } // namespace nl } // namespace arith diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h index 17fef608f..bd64a9ceb 100644 --- a/src/theory/arith/nl/cad/cdcac.h +++ b/src/theory/arith/nl/cad/cdcac.h @@ -131,6 +131,17 @@ class CDCAC const poly::Value& value); /** + * Check whether the polynomial has a real root above the given value (when + * evaluated over the current assignment). + */ + bool hasRootAbove(const poly::Polynomial& p, const poly::Value& val) const; + /** + * Check whether the polynomial has a real root below the given value (when + * evaluated over the current assignment). + */ + bool hasRootBelow(const poly::Polynomial& p, const poly::Value& val) const; + + /** * The current assignment. When the method terminates with SAT, it contains a * model for the input constraints. */ |