From: Gereon Kremer Date: Wed, 2 Mar 2022 01:27:02 +0000 (+0100) Subject: Prune spurious roots in lazard evaluation of coverings solver (#8200) X-Git-Tag: cvc5-1.0.0~350 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b4f69d410aac45506603e159d70cabd366b05f6d;p=cvc5.git 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 971bb7ea1..af64c8844 100644 --- 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& Configuration::getDebugTags() { diff --git a/src/base/configuration.h b/src/base/configuration.h index ece91c4ae..5afb14090 100644 --- 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& 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 84b89cfba..7399d4412 100644 --- 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 cdb9bdeab..a0d0edfa3 100644 --- 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 3d60e8677..2332a8fa3 100644 --- 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 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 a773241b5..a495239dd 100644 --- 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 index 000000000..6b7cec346 --- /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)