From d8f2b5ca0139d7f98fe7ed8d82e390f32a546ce1 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Feb 2026 10:54:39 -1000 Subject: [PATCH] add new polynomials from handle_nullified to m_todo Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 8 +- src/nlsat/nlsat_common.cpp | 21 +++++ src/nlsat/nlsat_common.h | 3 + src/test/nlsat.cpp | 161 ------------------------------------- 4 files changed, 31 insertions(+), 162 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index d728f40a0..e01aa15bc 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -1217,12 +1217,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) handle_nullified_poly(p); m_witnesses.push_back(w); + // 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); } } diff --git a/src/nlsat/nlsat_common.cpp b/src/nlsat/nlsat_common.cpp index 547d2660d..bdbef3293 100644 --- a/src/nlsat/nlsat_common.cpp +++ b/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 */ diff --git a/src/nlsat/nlsat_common.h b/src/nlsat/nlsat_common.h index c7864e991..9a3949533 100644 --- a/src/nlsat/nlsat_common.h +++ b/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) { diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 8e6261e70..4a6d65beb 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -2167,165 +2167,6 @@ static void tst_unsound_gh8397() { std::cout << "\n=== END tst_unsound_gh8397 ===\n\n"; } -// Test case for unsound lemma from p6236_terminationG_0.smt2 -// Levelwise produces cell that's too large when polynomial is nullified. -// Polynomials: -// p[0]: - x9 -// p[1]: - x9 x15 - x10 x14 + x5 x11 x13 + x3 x4 x11 + 2 -// p[2]: x15 + x6 x13 + x0 x4 -// Sample: x0=1, x1=-1, x2=1, x3=-1, x4=2, x5=0, x6=0, x7=0, x8=0, x9=1, x10=0, x11=1/2, x12=1, x13=-4, x14=2 -// Counterexample: x0=0, x3=-1, x4=1, x5=0, x6=0, x9=1, x10=0, x11=3, x13=0, x14=0, x15=0 -static void tst_unsound_lws_p6236() { - std::cout << "=== tst_unsound_lws_p6236 ===\n"; - - params_ref ps; - ps.set_bool("lws", true); - reslimit rlim; - nlsat::solver s(rlim, ps, false); - anum_manager & am = s.am(); - nlsat::pmanager & pm = s.pm(); - nlsat::assignment sample_as(am); - nlsat::assignment counter_as(am); - polynomial::cache cache(pm); - - // Create 16 variables x0-x15 - nlsat::var x0 = s.mk_var(false); - nlsat::var x1 = s.mk_var(false); - nlsat::var x2 = s.mk_var(false); - nlsat::var x3 = s.mk_var(false); - nlsat::var x4 = s.mk_var(false); - nlsat::var x5 = s.mk_var(false); - nlsat::var x6 = s.mk_var(false); - nlsat::var x7 = s.mk_var(false); - nlsat::var x8 = s.mk_var(false); - nlsat::var x9 = s.mk_var(false); - nlsat::var x10 = s.mk_var(false); - nlsat::var x11 = s.mk_var(false); - nlsat::var x12 = s.mk_var(false); - nlsat::var x13 = s.mk_var(false); - nlsat::var x14 = s.mk_var(false); - nlsat::var x15 = s.mk_var(false); - - polynomial_ref _x0(pm), _x1(pm), _x2(pm), _x3(pm), _x4(pm), _x5(pm), _x6(pm), _x7(pm); - polynomial_ref _x8(pm), _x9(pm), _x10(pm), _x11(pm), _x12(pm), _x13(pm), _x14(pm), _x15(pm); - _x0 = pm.mk_polynomial(x0); - _x1 = pm.mk_polynomial(x1); - _x2 = pm.mk_polynomial(x2); - _x3 = pm.mk_polynomial(x3); - _x4 = pm.mk_polynomial(x4); - _x5 = pm.mk_polynomial(x5); - _x6 = pm.mk_polynomial(x6); - _x7 = pm.mk_polynomial(x7); - _x8 = pm.mk_polynomial(x8); - _x9 = pm.mk_polynomial(x9); - _x10 = pm.mk_polynomial(x10); - _x11 = pm.mk_polynomial(x11); - _x12 = pm.mk_polynomial(x12); - _x13 = pm.mk_polynomial(x13); - _x14 = pm.mk_polynomial(x14); - _x15 = pm.mk_polynomial(x15); - (void)_x1; (void)_x2; (void)_x7; (void)_x8; (void)_x12; - - // p[0]: -x9 - polynomial_ref p0(pm); - p0 = -_x9; - - // p[1]: -x9*x15 - x10*x14 + x5*x11*x13 + x3*x4*x11 + 2 - polynomial_ref p1(pm); - p1 = -_x9 * _x15 - _x10 * _x14 + _x5 * _x11 * _x13 + _x3 * _x4 * _x11 + 2; - - // p[2]: x15 + x6*x13 + x0*x4 - polynomial_ref p2(pm); - p2 = _x15 + _x6 * _x13 + _x0 * _x4; - - std::cout << "Input polynomials:\n"; - std::cout << " p0: " << p0 << "\n"; - std::cout << " p1: " << p1 << "\n"; - std::cout << " p2: " << p2 << "\n\n"; - - // Sample: x0=1, x1=-1, x2=1, x3=-1, x4=2, x5=0, x6=0, x7=0, x8=0, x9=1, x10=0, x11=1/2, x12=1, x13=-4, x14=2 - scoped_anum val(am); - rational half(1, 2); - am.set(val, 1); sample_as.set(x0, val); - am.set(val, -1); sample_as.set(x1, val); - am.set(val, 1); sample_as.set(x2, val); - am.set(val, -1); sample_as.set(x3, val); - am.set(val, 2); sample_as.set(x4, val); - am.set(val, 0); sample_as.set(x5, val); - am.set(val, 0); sample_as.set(x6, val); - am.set(val, 0); sample_as.set(x7, val); - am.set(val, 0); sample_as.set(x8, val); - am.set(val, 1); sample_as.set(x9, val); - am.set(val, 0); sample_as.set(x10, val); - am.set(val, half.to_mpq()); sample_as.set(x11, val); - am.set(val, 1); sample_as.set(x12, val); - am.set(val, -4); sample_as.set(x13, val); - am.set(val, 2); sample_as.set(x14, val); - - // Counterexample: x0=0, x3=-1, x4=1, x5=0, x6=0, x9=1, x10=0, x11=3, x13=0, x14=0, x15=0 - // (use sample values for variables not mentioned in counterexample) - am.set(val, 0); counter_as.set(x0, val); - am.set(val, -1); counter_as.set(x1, val); - am.set(val, 1); counter_as.set(x2, val); - am.set(val, -1); counter_as.set(x3, val); - am.set(val, 1); counter_as.set(x4, val); - am.set(val, 0); counter_as.set(x5, val); - am.set(val, 0); counter_as.set(x6, val); - am.set(val, 0); counter_as.set(x7, val); - am.set(val, 0); counter_as.set(x8, val); - am.set(val, 1); counter_as.set(x9, val); - am.set(val, 0); counter_as.set(x10, val); - am.set(val, 3); counter_as.set(x11, val); - am.set(val, 1); counter_as.set(x12, val); - am.set(val, 0); counter_as.set(x13, val); - am.set(val, 0); counter_as.set(x14, val); - am.set(val, 0); counter_as.set(x15, val); - - std::cout << "Sample: x0=1,x1=-1,x2=1,x3=-1,x4=2,x5=0,x6=0,x7=0,x8=0,x9=1,x10=0,x11=1/2,x12=1,x13=-4,x14=2\n"; - std::cout << "Counterexample: x0=0,x3=-1,x4=1,x5=0,x6=0,x9=1,x10=0,x11=3,x13=0,x14=0,x15=0\n\n"; - - // Verify polynomial signs differ between sample and counterexample - // At counterexample: p2 = x15 + x6*x13 + x0*x4 = 0 + 0 + 0 = 0 - // The lemma says p2 > 0, but counterexample has p2 = 0 - std::cout << "Polynomial signs at COUNTEREXAMPLE:\n"; - std::cout << " p0 sign: " << am.eval_sign_at(p0, counter_as) << "\n"; - std::cout << " p1 sign: " << am.eval_sign_at(p1, counter_as) << "\n"; - std::cout << " p2 sign: " << am.eval_sign_at(p2, counter_as) << "\n\n"; - - // Set solver assignment for levelwise (x0..x14, not x15) - s.set_rvalues(sample_as); - - // Build polynomial vector - polynomial_ref_vector polys(pm); - polys.push_back(p0); - polys.push_back(p1); - polys.push_back(p2); - - nlsat::var max_x = x15; - - std::cout << "Running levelwise with max_x = x15\n"; - - // Run levelwise - nlsat::levelwise lws(s, polys, max_x, s.sample(), pm, am, cache); - auto cell = lws.single_cell(); - - std::cout << "Cell intervals (count=" << cell.size() << "):\n"; - for (unsigned i = 0; i < cell.size(); ++i) { - std::cout << " Level " << i << ": "; - nlsat::display(std::cout, s, cell[i]) << "\n"; - } - - // Check if counterexample is inside the cell - std::cout << "\n--- Checking if counterexample is in cell ---\n"; - - bool counterexample_outside_cell = is_point_inside_cell(am, pm, cell, counter_as); - - // For a sound cell, the counterexample must be OUTSIDE the cell. - ENSURE(counterexample_outside_cell); - std::cout << "SUCCESS: Counterexample is OUTSIDE the cell (cell is sound)\n"; - - std::cout << "=== END tst_unsound_lws_p6236 ===\n\n"; -} // Test case for unsound lemma - nullified polynomial in levelwise // Polynomials: @@ -2653,8 +2494,6 @@ static void tst_explain_p6236() { void tst_nlsat() { tst_explain_p6236(); std::cout << "------------------\n"; - tst_unsound_lws_p6236(); - std::cout << "------------------\n"; tst_unsound_lws_disc_zero(); std::cout << "------------------\n"; tst_unsound_lws_nullified2();