diff options
Diffstat (limited to 'src/theory/arith/nl/cad/cdcac.cpp')
| -rw-r--r-- | src/theory/arith/nl/cad/cdcac.cpp | 24 |
1 files changed, 22 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 |