diff options
-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. */ |