Make sure polynomials are properly factorized in nl-cad (#5733)

CAD theory (used in nl-cad) requires that polynomials are properly factorized (a finest square-free basis). This PR replaces usage of raw std::vector by a new wrapper PolyVector that ensures proper factorization whenever a polynomial is added. This fixes one piece of code that omitted factorization, leading to soundness issues as in #5726.
Fixes #5726.

1 files changed, 39 insertions, 32 deletions

diff --git a/src/theory/arith/nl/cad/projections.cpp b/src/theory/arith/nl/cad/projections.cpp
index 162e9f7be..8d33bf794 100644
--- a/src/theory/arith/nl/cad/projections.cpp
+++ b/src/theory/arith/nl/cad/projections.cpp
@@ -18,6 +18,8 @@
 
 #ifdef CVC4_POLY_IMP
 
+#include "base/check.h"
+
 namespace CVC4 {
 namespace theory {
 namespace arith {
@@ -26,72 +28,77 @@ namespace cad {
 
 using namespace poly;
 
-void reduceProjectionPolynomials(std::vector<Polynomial>& polys)
+void PolyVector::add(const poly::Polynomial& poly, bool assertMain)
 {
-  std::sort(polys.begin(), polys.end());
-  auto it = std::unique(polys.begin(), polys.end());
-  polys.erase(it, polys.end());
-}
-
-void addPolynomial(std::vector<Polynomial>& polys, const Polynomial& poly)
-{
-  for (const auto& p : square_free_factors(poly))
+  for (const auto& p : poly::square_free_factors(poly))
   {
-    if (is_constant(p)) continue;
-    polys.emplace_back(p);
+    if (poly::is_constant(p)) continue;
+    if (assertMain)
+    {
+      Assert(main_variable(poly) == main_variable(p));
+    }
+    std::vector<poly::Polynomial>::emplace_back(p);
   }
 }
 
-void addPolynomials(std::vector<Polynomial>& polys,
-                    const std::vector<Polynomial>& p)
+void PolyVector::reduce()
 {
-  for (const auto& q : p) addPolynomial(polys, q);
+  std::sort(begin(), end());
+  erase(std::unique(begin(), end()), end());
 }
 
-void makeFinestSquareFreeBasis(std::vector<Polynomial>& polys)
+void PolyVector::makeFinestSquareFreeBasis()
 {
-  for (std::size_t i = 0, n = polys.size(); i < n; ++i)
+  for (std::size_t i = 0, n = size(); i < n; ++i)
   {
     for (std::size_t j = i + 1; j < n; ++j)
     {
-      Polynomial g = gcd(polys[i], polys[j]);
+      Polynomial g = gcd((*this)[i], (*this)[j]);
       if (!is_constant(g))
       {
-        polys[i] = div(polys[i], g);
-        polys[j] = div(polys[j], g);
-        polys.emplace_back(g);
+        (*this)[i] = div((*this)[i], g);
+        (*this)[j] = div((*this)[j], g);
+        add(g);
       }
     }
   }
-  auto it = std::remove_if(polys.begin(), polys.end(), [](const Polynomial& p) {
-    return is_constant(p);
-  });
-  polys.erase(it, polys.end());
-  reduceProjectionPolynomials(polys);
+  auto it = std::remove_if(
+      begin(), end(), [](const Polynomial& p) { return is_constant(p); });
+  erase(it, end());
+  reduce();
+}
+void PolyVector::pushDownPolys(PolyVector& down, poly::Variable var)
+{
+  auto it =
+      std::remove_if(begin(), end(), [&down, &var](const poly::Polynomial& p) {
+        if (main_variable(p) == var) return false;
+        down.add(p);
+        return true;
+      });
+  erase(it, end());
 }
 
-std::vector<Polynomial> projection_mccallum(
-    const std::vector<Polynomial>& polys)
+PolyVector projection_mccallum(const std::vector<Polynomial>& polys)
 {
-  std::vector<Polynomial> res;
+  PolyVector res;
 
   for (const auto& p : polys)
   {
     for (const auto& coeff : coefficients(p))
     {
-      addPolynomial(res, coeff);
+      res.add(coeff);
     }
-    addPolynomial(res, discriminant(p));
+    res.add(discriminant(p));
   }
   for (std::size_t i = 0, n = polys.size(); i < n; ++i)
   {
     for (std::size_t j = i + 1; j < n; ++j)
     {
-      addPolynomial(res, resultant(polys[i], polys[j]));
+      res.add(resultant(polys[i], polys[j]));
     }
   }
 
-  reduceProjectionPolynomials(res);
+  res.reduce();
   return res;
 }