Prune spurious roots in lazard evaluation of coverings solver (#8200)

This PR fixes a subtle issue in the Lazard evaluation used in the coverings solver if --nl-cov-lift=lazard is used.
When isolating real roots (over a partial assignment that contains real algebraic number), the core root solver may find roots that are spurious, i.e., they are not actually roots of the input polynomial. This is due to the way how the multivariate polynomial is "partially evaluated" before calling the univariate real root isolation.
When using the libpoly real root isolation, this is all done internally. For the Lazard evaluation, however, we explicitly call the libpoly real root isolation on a univariate polynomial that already has these spurious roots, hence we need to remove them ourselves.

While debugging this issue, another weird oversight was detected (and fixed): for some reason we expected the vanishing factor (after factoring the defining polynomial when constructing the next field extension) to only have two term. There is no reason for this restriction, and the code below works just fine.

diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index 971bb7ea154967b40fb186bddb9df4d72d5311cb..af64c88446c9d69c74851345cb62b11997b0e88b 100644 (file)
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -221,6 +221,7 @@ bool Configuration::isBuiltWithPoly()
 {
   return IS_POLY_BUILD;
 }
+bool Configuration::isBuiltWithCoCoA() { return IS_COCOA_BUILD; }
 
 const std::vector<std::string>& Configuration::getDebugTags()
 {

diff --git a/src/base/configuration.h b/src/base/configuration.h
index ece91c4ae71486b4d7cb60ca0e838be143f9edce..5afb1409098e8181ddd9cdee5a6ea4a02bf2e572 100644 (file)
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -107,6 +107,8 @@ public:
 
   static bool isBuiltWithPoly();
 
+  static bool isBuiltWithCoCoA();
+
   /* Return a sorted array of the debug tags name */
   static const std::vector<std::string>& getDebugTags();
   /* Test if the given argument is a known debug tag name */

diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index 84b89cfbad8a365caeb73143c823afde4da23c0b..7399d44125b36355028215ac4626b934ddac3f64 100644 (file)
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -102,6 +102,12 @@ namespace cvc5 {
 #define IS_POLY_BUILD false
 #endif /* CVC5_USE_POLY */
 
+#if CVC5_USE_COCOA
+#define IS_COCOA_BUILD true
+#else /* CVC5_USE_COCOA */
+#define IS_COCOA_BUILD false
+#endif /* CVC5_USE_COCOA */
+
 #if HAVE_LIBEDITLINE
 #define IS_EDITLINE_BUILD true
 #else /* HAVE_LIBEDITLINE */

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index cdb9bdeabbf090b882e275d95563832a431b47fb..a0d0edfa3bb051257aa5d1fa31fbbd53d35c04b6 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -447,6 +447,7 @@ void OptionsHandler::showConfiguration(const std::string& flag, bool value)
   print_config_cond("gmp", Configuration::isBuiltWithGmp());
   print_config_cond("kissat", Configuration::isBuiltWithKissat());
   print_config_cond("poly", Configuration::isBuiltWithPoly());
+  print_config_cond("cocoa", Configuration::isBuiltWithCoCoA());
   print_config_cond("editline", Configuration::isBuiltWithEditline());
 }
 

diff --git a/src/theory/arith/nl/coverings/lazard_evaluation.cpp b/src/theory/arith/nl/coverings/lazard_evaluation.cpp
index 3d60e86770a70322a5fef57cbe6041acc014f6a3..2332a8fa3a562c49ae2fe13236f0e5710196d290 100644 (file)
--- a/src/theory/arith/nl/coverings/lazard_evaluation.cpp
+++ b/src/theory/arith/nl/coverings/lazard_evaluation.cpp
@@ -760,7 +760,8 @@ void LazardEvaluation::add(const poly::Variable& var, const poly::Value& val)
     {
       if (d_state->evaluatesToZero(f))
       {
-        Assert(CoCoA::deg(f) > 0 && CoCoA::NumTerms(f) <= 2);
+        Trace("nl-cov::lazard") << "Found vanishing factor " << f << std::endl;
+        Assert(CoCoA::deg(f) > 0);
         if (CoCoA::deg(f) == 1)
         {
           auto rat = -CoCoA::ConstantCoeff(f) / CoCoA::LC(f);
@@ -840,7 +841,25 @@ std::vector<poly::Value> LazardEvaluation::isolateRealRoots(
       roots.emplace_back(r);
     }
   }
+  // now postprocess roots: sort, remove duplicates and spurious roots.
+  // the reduction to a univariate polynomial that happens within
+  // reducePolynomial() may introduce new (spurious) real roots that correspond
+  // to complex (non-real) roots in the original input. we need to remove such
+  // spurious roots, i.e., roots where the input polynomial does not actually
+  // vanish.
   std::sort(roots.begin(), roots.end());
+  auto endit = std::unique(roots.begin(), roots.end());
+  endit = std::remove_if(roots.begin(), endit, [this, &q](const auto& v) {
+    // evaluate q != 0 over the assignment
+    d_state->d_assignment.set(d_state->d_variables.back(), v);
+    bool res = poly::evaluate_constraint(
+        q, d_state->d_assignment, poly::SignCondition::NE);
+    // make sure the assignment is properly reset
+    d_state->d_assignment.unset(d_state->d_variables.back());
+    return res;
+  });
+  // now actually remove the roots we don't want.
+  roots.erase(endit, roots.end());
   return roots;
 }
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a773241b5577e6a2cd30b0053918884c77c77539..a495239dd1b5dea7cfc9600ab23590ab5e61bd5d 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -780,6 +780,7 @@ set(regress_0_tests
   regress0/nl/issue6547-ran-model.smt2
   regress0/nl/issue6619-ran-model.smt2
   regress0/nl/issue8135-icp-candidates.smt2
+  regress0/nl/lazard-spurious-root.smt2
   regress0/nl/magnitude-wrong-1020-m.smt2
   regress0/nl/mult-po.smt2
   regress0/nl/nia-wrong-tl.smt2

diff --git a/test/regress/regress0/nl/lazard-spurious-root.smt2 b/test/regress/regress0/nl/lazard-spurious-root.smt2
new file mode 100644 (file)
index 0000000..6b7cec3
--- /dev/null
+++ b/test/regress/regress0/nl/lazard-spurious-root.smt2
@@ -0,0 +1,23 @@
+; REQUIRES: cocoa
+; REQUIRES: poly
+; COMMAND-LINE: --nl-cov-lift=lazard
+; EXPECT: sat
+(set-logic QF_NRA)
+(declare-const d Real)
+(declare-const a Real)
+(declare-const m Real)
+(declare-const l Real)
+(declare-const t Real)
+(declare-const x Real)
+(declare-const y Real)
+(declare-const v Real)
+(assert (and
+    (< m 0)
+    (< d 0)
+    (> y 0)
+    (> t 0)
+    (= 0 (+ m x (* l v)))
+    (= 0 (+ x a (* a y)))
+    (= 0 (+ t (* d d) (* t t) (* a a y) (- (* d l v y y))))
+))
+(check-sat)