Merge pull request #8691 from Z3Prover/no_fail

Disable failure on a nullified polynomial in levelwise

src/nlsat/levelwise.cpp

@@ -4,7 +4,6 @@
 #include "math/polynomial/algebraic_numbers.h"
 #include "math/polynomial/polynomial.h"
 #include "nlsat_common.h"
-#include "util/z3_exception.h"
 #include "util/vector.h"
 #include "util/trace.h"
 
@@ -44,7 +43,6 @@ namespace nlsat {
         sector_spanning_tree
     };
 
-    struct nullified_poly_exception {};
 
     struct levelwise::impl {
         solver&                      m_solver;
@@ -67,7 +65,6 @@ namespace nlsat {
         std_vector<bool>                m_poly_has_roots;
 
         polynomial_ref_vector  m_psc_tmp;        // scratch for PSC chains
-        bool                   m_fail = false;
 
         // Vectors indexed by position in m_level_ps (more cache-friendly than maps)
         mutable std_vector<uint8_t> m_side_mask;       // bit0 = lower, bit1 = upper, 3 = both
@@ -265,7 +262,53 @@ namespace nlsat {
             m_spanning_tree_threshold = m_solver.lws_spt_threshold();
         }
 
-        void fail() { throw nullified_poly_exception(); }
+        // Handle a polynomial whose every coefficient evaluates to zero at the sample.
+        // Compute partial derivatives level by level. If all derivatives at a level vanish,
+        // request_factorized each of them and continue to the next level.
+        // When a non-vanishing derivative is found, request_factorized it and stop.
+        void handle_nullified_poly(polynomial_ref const& p) {
+            // Add all coefficients of p as a polynomial of x_{m_level} to m_todo.
+            unsigned deg = m_pm.degree(p, m_level);
+            for (unsigned j = 0; j <= deg; ++j) {
+                polynomial_ref coeff(m_pm.coeff(p, m_level, j), m_pm);
+                if (!coeff || is_zero(coeff) || is_const(coeff))
+                    continue;
+                request_factorized(coeff);
+            }
+
+            // Compute partial derivatives level by level. If all derivatives at a level vanish,
+            // request_factorized each of them and continue to the next level.
+            // When a non-vanishing derivative is found, request_factorized it and stop.
+            polynomial_ref_vector current(m_pm);
+            current.push_back(p);
+            while (!current.empty()) {
+                polynomial_ref_vector next_derivs(m_pm);
+                for (unsigned i = 0; i < current.size(); ++i) {
+                    polynomial_ref q(current.get(i), m_pm);
+                    unsigned mv = m_pm.max_var(q);
+                    if (mv == null_var)
+                        continue;
+                    for (unsigned x = 0; x <= mv; ++x) {
+                        if (m_pm.degree(q, x) == 0)
+                            continue;
+                        polynomial_ref dq = derivative(q, x);
+                        if (!dq || is_zero(dq) || is_const(dq))
+                            continue;
+                        if (m_am.eval_sign_at(dq, sample()) != 0) {
+                            request_factorized(dq);
+                            return;
+                        }
+                        next_derivs.push_back(dq);
+                    }
+                }
+                for (unsigned i = 0; i < next_derivs.size(); ++i) {
+                    polynomial_ref dq(next_derivs.get(i), m_pm);
+                    request_factorized(dq);
+                }
+                current = std::move(next_derivs);
+            }
+            
+        }
 
         static void reset_interval(root_function_interval& I) {
             I.section = false;
@@ -1067,8 +1110,8 @@ namespace nlsat {
                     add_projection_for_poly(p, m_level, witness, true, true); // section poly: full projection
                 else if (has_roots.find(i) == has_roots.end())
                     add_projection_for_poly(p, m_level, witness, true, true); // no roots: need LC+disc for delineability
-                else if (witness && !is_const(witness))
+                else 
-                    request_factorized(witness); // has roots: witness only
+                    add_projection_for_poly(p, m_level, witness, false, true);
             }
         }
 
@@ -1176,12 +1219,18 @@ namespace nlsat {
             // Line 10/11: detect nullification + pick a non-zero coefficient witness per p.
             m_witnesses.clear();
             m_witnesses.reserve(m_level_ps.size());
-            for (unsigned i = 0; i < m_level_ps.size(); ++i) {
+            // Fixpoint loop: handle_nullified_poly may add more polynomials back at m_level
+            // via request_factorized. Drain them from m_todo into m_level_ps and
+            // compute witnesses for the new entries until no more appear.
+            for (unsigned i = 0; i < m_level_ps.size(); i++) {
                 polynomial_ref p(m_level_ps.get(i), m_pm);
                 polynomial_ref w = choose_nonzero_coeff(p, m_level);
                 if (!w)
-                    fail();
+                    handle_nullified_poly(p);
-                m_witnesses.push_back(w);
+                m_witnesses.push_back(w); // need to push anyway since m_witnesses is accessed by the index
+                // Absorb any same-level polys that handle_nullified_poly added to m_todo
+                if (i + 1 == m_level_ps.size())
+                    m_todo.extract_polys_at_level(m_level, m_level_ps);
             }
         }
 
@@ -1246,7 +1295,7 @@ namespace nlsat {
             }
         }
 
-        std_vector<root_function_interval> single_cell_work() {
+        std_vector<root_function_interval> single_cell() {
             TRACE(lws,             
                   tout << "Input polynomials (" << m_P.size() << "):\n";
                   for (unsigned i = 0; i < m_P.size(); ++i)
@@ -1294,15 +1343,6 @@ namespace nlsat {
             return m_I;
         }
 
-        std_vector<root_function_interval> single_cell() {
-            try {
-                return single_cell_work();
-            }
-            catch (nullified_poly_exception&) {
-                m_fail = true;
-                return m_I;
-            }
-        }
     };
 
     levelwise::levelwise(
@@ -1320,9 +1360,6 @@ namespace nlsat {
     std_vector<levelwise::root_function_interval> levelwise::single_cell() {
         return m_impl->single_cell();
     }
-
-    bool levelwise::failed() const { return m_impl->m_fail; }
-
 } // namespace nlsat
 
 // Free pretty-printer for symbolic_interval

src/nlsat/levelwise.h

@@ -46,7 +46,6 @@ namespace nlsat {
         levelwise(levelwise const&) = delete;
         levelwise& operator=(levelwise const&) = delete;
         std_vector<root_function_interval> single_cell();
-        bool failed() const;
     };
 
     //

src/nlsat/nlsat_common.cpp

@@ -112,6 +112,27 @@ namespace nlsat {
         return x;
     }
 
+    unsigned todo_set::extract_polys_at_level(var x, polynomial_ref_vector& out) {
+        pmanager& pm = m_set.m();
+        unsigned sz = m_set.size();
+        unsigned j = 0;
+        unsigned count = 0;
+        for (unsigned i = 0; i < sz; i++) {
+            poly* p = m_set.get(i);
+            if (pm.max_var(p) == x) {
+                out.push_back(p);
+                m_in_set[pm.id(p)] = false;
+                ++count;
+            }
+            else {
+                m_set.set(j, p);
+                j++;
+            }
+        }
+        m_set.shrink(j);
+        return count;
+    }
+
     /**
        \brief Wrapper for factorization
     */

src/nlsat/nlsat_common.h

@@ -44,6 +44,9 @@ namespace nlsat {
            them in max_polys. Return the maximal variable
          */
         var extract_max_polys(polynomial_ref_vector& max_polys);
+        // Extract polynomials whose max_var equals \c x, appending them to \c out.
+        // Returns the number of polynomials extracted.
+        unsigned extract_polys_at_level(var x, polynomial_ref_vector& out);
     };
 
     inline std::ostream& display(std::ostream& out, pmanager& pm, polynomial_ref const& p, display_var_proc const& proc) {

src/nlsat/nlsat_explain.cpp

@@ -1048,9 +1048,6 @@ namespace nlsat {
             
             levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am, cache);
             auto cell = lws.single_cell();
-            if (lws.failed())
-                return false;
-
             TRACE(lws, for (unsigned i = 0; i < cell.size(); i++)
                                  display(tout << "I[" << i << "]:", m_solver, cell[i]) << "\n";);
             // Enumerate all intervals in the computed cell and add literals for each non-trivial interval.
@@ -1087,7 +1084,7 @@ namespace nlsat {
          * "Solving Satisfiability of Polynomial Formulas By Sample - Cell Projection"
          * https://arxiv.org/abs/2003.00409 
          */
-        void project_cdcac(polynomial_ref_vector & ps, var max_x) {
+        void project(polynomial_ref_vector & ps, var max_x) {
             bool first = true;
             if (ps.empty())
                 return;
@@ -1145,10 +1142,6 @@ namespace nlsat {
             
         }
 
-        void project(polynomial_ref_vector & ps, var max_x) {
-            project_cdcac(ps, max_x);
-        }
-
         bool check_already_added() const {
             for (bool b : m_already_added_literal) {
                 (void)b;

src/nlsat/nlsat_solver.cpp

@@ -1092,7 +1092,7 @@ namespace nlsat {
         }
 
         // Helper: Display unsound lemma failure information
-        void display_unsound_lemma(imp& checker, scoped_bool_vars& tr, unsigned n, literal const* cls) {
+        void display_unsound_lemma(imp& checker, scoped_bool_vars& tr, unsigned n, literal const* cls, lazy_justification const* jst = nullptr) {
             verbose_stream() << "\n";
             verbose_stream() << "========== UNSOUND LEMMA DETECTED ==========\n";
             verbose_stream() << "Levelwise used for this conflict: " << (m_last_conflict_used_lws ? "YES" : "NO") << "\n";
@@ -1134,10 +1134,26 @@ namespace nlsat {
                 verbose_stream() << " = " << checker.value(tlit) << "\n";
             }
             verbose_stream() << "=============================================\n";
+            if (jst) {
+                verbose_stream() << "Initial justification (lazy_justification):\n";
+                verbose_stream() << "  Num literals: " << jst->num_lits() << "\n";
+                for (unsigned i = 0; i < jst->num_lits(); ++i) {
+                    verbose_stream() << "  jst lit[" << i << "]: ";
+                    display(verbose_stream(), jst->lit(i));
+                    verbose_stream() << "\n";
+                }
+                verbose_stream() << "  Num clauses: " << jst->num_clauses() << "\n";
+                for (unsigned i = 0; i < jst->num_clauses(); ++i) {
+                    verbose_stream() << "  jst clause[" << i << "]: ";
+                    display(verbose_stream(), jst->clause(i));
+                    verbose_stream() << "\n";
+                }
+                verbose_stream() << "=============================================\n";
+            }
             verbose_stream() << "ABORTING: Unsound lemma detected!\n";
         }
 
-        void check_lemma(unsigned n, literal const* cls, assumption_set a) {
+        void check_lemma(unsigned n, literal const* cls, assumption_set a, lazy_justification const* jst = nullptr) {
             TRACE(nlsat, display(tout << "check lemma: ", n, cls) << "\n";
                   display(tout););
             
@@ -1180,7 +1196,7 @@ namespace nlsat {
                     verbose_stream() << "Dumping lemma that internal checker thinks is not a tautology:\n";
                     verbose_stream() << "Checker levelwise calls: " << checker.m_stats.m_levelwise_calls << "\n";
                     log_lemma(verbose_stream(), n, cls, true, "internal-check-fail");
-                    display_unsound_lemma(checker, tr, n, cls);
+                    display_unsound_lemma(checker, tr, n, cls, jst);
                     exit(1);
                 }
             }
@@ -2402,7 +2418,7 @@ namespace nlsat {
             if (m_check_lemmas) {
                 TRACE(nlsat, tout << "Checking lazy clause with " << m_lazy_clause.size() << " literals:\n";
                       display(tout, m_lazy_clause.size(), m_lazy_clause.data()) << "\n";);
-                check_lemma(m_lazy_clause.size(), m_lazy_clause.data(), nullptr);
+                check_lemma(m_lazy_clause.size(), m_lazy_clause.data(), nullptr, &jst);
                 m_valids.push_back(mk_clause_core(m_lazy_clause.size(), m_lazy_clause.data(), false, nullptr));
             }
             
@@ -4700,9 +4716,6 @@ namespace nlsat {
     assumption solver::join(assumption a, assumption b) {
         return (m_imp->m_asm.mk_join(static_cast<imp::_assumption_set>(a), static_cast<imp::_assumption_set>(b)));
     }
-
     bool solver::apply_levelwise() const { return m_imp->m_apply_lws; }
-
     unsigned solver::lws_spt_threshold() const { return m_imp->m_lws_spt_threshold; }
-
 };

src/test/main.cpp

@@ -227,7 +227,7 @@ int main(int argc, char ** argv) {
     TST(prime_generator);
     TST(permutation);
     TST(nlsat);
-    TST(nlsat_mv);
+    TST(13);
     TST(zstring);
     if (test_all) return 0;
     TST(ext_numeral);