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.

diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index 907f7a7b68852c214e47c162d84dbac115bffbce..4725eb1984f4f10bdf52232eac4b2f1f75fd1e70 100644 (file)
--- 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 17fef608f8b44482099286e39fc84a0694fdef33..bd64a9ceb641256d9c1b63b35ea68eb457ece9ed 100644 (file)
--- a/src/theory/arith/nl/cad/cdcac.h
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -130,6 +130,17 @@ class CDCAC
   CACInterval buildIntegralityInterval(std::size_t cur_variable,
                                        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.