From 2d8e866e19317b5b81345a6c70261a8eca15331b Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 17 Feb 2026 13:20:50 -1000 Subject: [PATCH 01/16] try replace fail with a adding partial derivatives Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 52 +++++++++++++++++++++++++++++------------ 1 file changed, 37 insertions(+), 15 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index d1d5ca938..a7057c73c 100644 --- a/src/nlsat/levelwise.cpp +++ b/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; @@ -265,7 +263,41 @@ 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) { + m_fail = true; + 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; @@ -1180,7 +1212,7 @@ namespace nlsat { 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); } } @@ -1246,7 +1278,7 @@ namespace nlsat { } } - std_vector single_cell_work() { + std_vector single_cell() { TRACE(lws, tout << "Input polynomials (" << m_P.size() << "):\n"; for (unsigned i = 0; i < m_P.size(); ++i) @@ -1293,16 +1325,6 @@ namespace nlsat { return m_I; } - - std_vector single_cell() { - try { - return single_cell_work(); - } - catch (nullified_poly_exception&) { - m_fail = true; - return m_I; - } - } }; levelwise::levelwise( From a781f9c0a0adfad827c0e5028b1a2681131d14b8 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 17 Feb 2026 14:11:16 -1000 Subject: [PATCH 02/16] remove an obsolete m_fail and related from levelwise Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 3 --- src/nlsat/levelwise.h | 1 - src/nlsat/nlsat_explain.cpp | 3 --- src/test/nlsat.cpp | 46 +++++++++++++++---------------------- 4 files changed, 18 insertions(+), 35 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index a7057c73c..66089bdae 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -65,7 +65,6 @@ namespace nlsat { std_vector 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 m_side_mask; // bit0 = lower, bit1 = upper, 3 = both @@ -268,7 +267,6 @@ namespace nlsat { // 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) { - m_fail = true; polynomial_ref_vector current(m_pm); current.push_back(p); while (!current.empty()) { @@ -1343,7 +1341,6 @@ namespace nlsat { return m_impl->single_cell(); } - bool levelwise::failed() const { return m_impl->m_fail; } } // namespace nlsat diff --git a/src/nlsat/levelwise.h b/src/nlsat/levelwise.h index 27e379374..950bee641 100644 --- a/src/nlsat/levelwise.h +++ b/src/nlsat/levelwise.h @@ -46,7 +46,6 @@ namespace nlsat { levelwise(levelwise const&) = delete; levelwise& operator=(levelwise const&) = delete; std_vector single_cell(); - bool failed() const; }; // diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index dcc79bc2a..48e23c81d 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/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. diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index f26995462..33eca3172 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -491,7 +491,6 @@ static void tst_vandermond() { 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); am.set(one, 1); am.set(two, 2); as.set(x0, one); @@ -1164,7 +1163,6 @@ static void tst_nullified_polynomial() { nlsat::levelwise lws(s, polys, max_x, s.sample(), pm, am, cache); auto cell = lws.single_cell(); - ENSURE(lws.failed()); } // Test case for unsound lemma lws2380 - comparing standard projection vs levelwise @@ -1473,7 +1471,6 @@ static void tst_unsound_lws_x3() { nlsat::levelwise lws(s, polys, max_x, s.sample(), pm, am, cache); auto cell = lws.single_cell(); - std::cout << "Levelwise " << (lws.failed() ? "FAILED" : "succeeded") << "\n"; std::cout << "Cell intervals (count=" << cell.size() << "):\n"; for (auto const& interval : cell) { nlsat::display(std::cout << " ", s, interval) << "\n"; @@ -1682,7 +1679,6 @@ static void tst_unsound_lws_n46() { nlsat::levelwise lws(s, polys, max_x, s.sample(), pm, am, cache); auto cell = lws.single_cell(); - std::cout << "Levelwise " << (lws.failed() ? "FAILED" : "succeeded") << "\n"; std::cout << "Cell intervals:\n"; for (unsigned i = 0; i < cell.size(); ++i) { std::cout << " Level " << i << ": "; @@ -1912,7 +1908,6 @@ static void tst_unsound_lws_et4() { nlsat::levelwise lws(s, polys, max_x, s.sample(), pm, am, cache); auto cell = lws.single_cell(); - std::cout << "Levelwise " << (lws.failed() ? "FAILED" : "succeeded") << "\n"; std::cout << "Cell intervals (count=" << cell.size() << "):\n"; for (auto const& interval : cell) { nlsat::display(std::cout << " ", s, interval) << "\n"; @@ -2074,7 +2069,6 @@ static void tst_unsound_lws_disc_zero() { nlsat::levelwise lws(s, polys, max_x, s.sample(), pm, am, cache); auto cell = lws.single_cell(); - std::cout << "Levelwise " << (lws.failed() ? "FAILED" : "succeeded") << "\n"; std::cout << "Cell intervals:\n"; for (unsigned i = 0; i < cell.size(); ++i) { std::cout << " Level " << i << ": "; @@ -2294,28 +2288,25 @@ static void tst_unsound_lws_ppblockterm() { nlsat::levelwise lws(s, polys, max_x, s.sample(), pm, am, cache); auto cell = lws.single_cell(); - if (lws.failed()) { - std::cout << "Levelwise FAILED\n"; - } else { - std::cout << "Levelwise succeeded\n"; - std::cout << "--- LEMMA from levelwise ---\n"; - for (unsigned i = 0; i < cell.size(); i++) { - auto const& interval = cell[i]; - std::cout << "Level x" << i << ": "; - if (interval.is_section()) { - std::cout << "section at root[" << interval.l_index << "] of " << interval.l << "\n"; - } else { - if (interval.l_inf()) - std::cout << "(-oo, "; - else - std::cout << "(root[" << interval.l_index << "] of " << interval.l << ", "; - if (interval.u_inf()) - std::cout << "+oo)"; - else - std::cout << "root[" << interval.u_index << "] of " << interval.u << ")"; - std::cout << "\n"; - } + std::cout << "Levelwise succeeded\n"; + std::cout << "--- LEMMA from levelwise ---\n"; + for (unsigned i = 0; i < cell.size(); i++) { + auto const& interval = cell[i]; + std::cout << "Level x" << i << ": "; + if (interval.is_section()) { + std::cout << "section at root[" << interval.l_index << "] of " << interval.l << "\n"; + } else { + if (interval.l_inf()) + std::cout << "(-oo, "; + else + std::cout << "(root[" << interval.l_index << "] of " << interval.l << ", "; + if (interval.u_inf()) + std::cout << "+oo)"; + else + std::cout << "root[" << interval.u_index << "] of " << interval.u << ")"; + std::cout << "\n"; } + std::cout << "--- END LEMMA ---\n\n"; // Check polynomial signs at sample and counterexample @@ -2531,7 +2522,6 @@ static void tst_unsound_gh8397() { void tst_nlsat() { tst_unsound_gh8397(); - return; std::cout << "------------------\n"; tst_unsound_lws_ppblockterm(); std::cout << "------------------\n"; From 269dba052591924a4c028cc7c44af7d1177febb4 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 17 Feb 2026 14:20:58 -1000 Subject: [PATCH 03/16] add all coeffs ot a nullified polynomial to the projection Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 66089bdae..a2e527981 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -267,6 +267,17 @@ namespace nlsat { // 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 (w.r.t. 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()) { From af6d461b5e2fb2f901e19efe997bad2af214f52d Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 17 Feb 2026 14:46:21 -1000 Subject: [PATCH 04/16] add tests for levelwise Signed-off-by: Lev Nachmanson --- src/test/nlsat.cpp | 410 ++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 409 insertions(+), 1 deletion(-) diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 33eca3172..9a650e56d 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -2520,8 +2520,416 @@ 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 = false; + + // Counter values for each level + int counter_vals[] = {0, -1, 1, -1, 1, 0, 0, 0, 0, 1, 0, 3, 1, 0, 0, 0}; + + for (unsigned i = 0; i < cell.size(); ++i) { + auto const& interval = cell[i]; + nlsat::var level = i; + std::cout << "Level " << level << " (x" << level << "):\n"; + + // Build assignment up to this level (exclusive) using counterexample values + nlsat::assignment partial_as(am); + scoped_anum pval(am); + for (unsigned j = 0; j < level; ++j) { + am.set(pval, counter_vals[j]); + partial_as.set(j, pval); + } + // Special case: x11 at counter is 3 (integer, handled above) + + scoped_anum counter_val(am); + am.set(counter_val, counter_vals[level]); + + if (interval.is_section()) { + // Section: counterexample must be at the root + polynomial_ref sec_p(interval.l, pm); + scoped_anum_vector roots(am); + am.isolate_roots(sec_p, nlsat::undef_var_assignment(partial_as, level), roots); + if (roots.size() >= interval.l_index) { + bool at_root = am.eq(counter_val, roots[interval.l_index - 1]); + std::cout << " Section root[" << interval.l_index << "]: "; + am.display_decimal(std::cout, roots[interval.l_index - 1], 10); + std::cout << ", counter = "; + am.display_decimal(std::cout, counter_val, 10); + std::cout << " -> " << (at_root ? "AT ROOT" : "NOT AT ROOT") << "\n"; + if (!at_root) counterexample_outside_cell = true; + } + } else { + if (!interval.l_inf()) { + polynomial_ref lower_p(interval.l, pm); + scoped_anum_vector lower_roots(am); + am.isolate_roots(lower_p, nlsat::undef_var_assignment(partial_as, level), lower_roots); + if (lower_roots.size() >= interval.l_index) { + int cmp = am.compare(counter_val, lower_roots[interval.l_index - 1]); + std::cout << " Lower root[" << interval.l_index << "]: "; + am.display_decimal(std::cout, lower_roots[interval.l_index - 1], 10); + std::cout << ", counter = "; + am.display_decimal(std::cout, counter_val, 10); + std::cout << " -> " << (cmp > 0 ? "ABOVE" : (cmp < 0 ? "BELOW" : "EQUAL")) << "\n"; + if (cmp <= 0) counterexample_outside_cell = true; + } + } + if (!interval.u_inf()) { + polynomial_ref upper_p(interval.u, pm); + scoped_anum_vector upper_roots(am); + am.isolate_roots(upper_p, nlsat::undef_var_assignment(partial_as, level), upper_roots); + if (upper_roots.size() >= interval.u_index) { + int cmp = am.compare(counter_val, upper_roots[interval.u_index - 1]); + std::cout << " Upper root[" << interval.u_index << "]: "; + am.display_decimal(std::cout, upper_roots[interval.u_index - 1], 10); + std::cout << ", counter = "; + am.display_decimal(std::cout, counter_val, 10); + std::cout << " -> " << (cmp > 0 ? "ABOVE" : (cmp < 0 ? "BELOW" : "EQUAL")) << "\n"; + if (cmp >= 0) counterexample_outside_cell = true; + } + } + } + std::cout << "\n"; + } + + // 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: +// p[0]: - x6 + x3 x5 + 1 +// p[1]: - x2 +// p[2]: - 2 x2 x6^2 + 2 x3 x5 x6 - 2 x2 x5 x6 + x4 x5^3 + 2 x3 x5^2 +// Sample: x0=4, x1=1, x2=1, x3=5/2, x4=0, x5=1 +// Counterexample: x2=4, x3=-3, x4=0, x5=1, x6=-1 +static void tst_unsound_lws_nullified() { + std::cout << "=== tst_unsound_lws_nullified ===\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); + + 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); + + polynomial_ref _x2(pm), _x3(pm), _x4(pm), _x5(pm), _x6(pm); + _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); + + polynomial_ref p0(pm), p1(pm), p2(pm); + p0 = -_x6 + _x3 * _x5 + 1; + p1 = -_x2; + p2 = -2 * _x2 * (_x6^2) + 2 * _x3 * _x5 * _x6 - 2 * _x2 * _x5 * _x6 + + _x4 * (_x5^3) + 2 * _x3 * (_x5^2); + + std::cout << " p0: " << p0 << "\n p1: " << p1 << "\n p2: " << p2 << "\n"; + + // Sample: x0=4, x1=1, x2=1, x3=5/2, x4=0, x5=1 + scoped_anum val(am); + rational five_half(5, 2); + am.set(val, 4); 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, five_half.to_mpq()); sample_as.set(x3, val); + am.set(val, 0); sample_as.set(x4, val); + am.set(val, 1); sample_as.set(x5, val); + + // Counterexample: x0=4, x1=1, x2=4, x3=-3, x4=0, x5=1, x6=-1 + am.set(val, 4); counter_as.set(x0, val); + am.set(val, 1); counter_as.set(x1, val); + am.set(val, 4); counter_as.set(x2, val); + am.set(val, -3); counter_as.set(x3, val); + am.set(val, 0); counter_as.set(x4, val); + am.set(val, 1); counter_as.set(x5, val); + am.set(val, -1); counter_as.set(x6, val); + + s.set_rvalues(sample_as); + + polynomial_ref_vector polys(pm); + polys.push_back(p0); + polys.push_back(p1); + polys.push_back(p2); + + nlsat::levelwise lws(s, polys, x6, s.sample(), pm, am, cache); + auto cell = lws.single_cell(); + + std::cout << "Cell intervals:\n"; + for (unsigned i = 0; i < cell.size(); ++i) + nlsat::display(std::cout << " Level " << i << ": ", s, cell[i]) << "\n"; + + bool inside = is_point_inside_cell(am, pm, cell, counter_as); + // The counterexample should be OUTSIDE the cell for soundness. + // This ENSURE will fail, demonstrating the bug. + ENSURE(!inside); + std::cout << "=== END tst_unsound_lws_nullified ===\n\n"; +} + +// Test case for unsound lemma - nullified polynomial with x4=3/4 +// Polynomials: +// p[0]: x2 +// p[1]: x5 + x4 +// p[2]: x2^2 x5 x6 + x2^2 x4 x6 + 2 x2^2 x3 x5 + x0 x2^2 x5 - 3 x0 x1 x2 x5 - 2 x0 x1^2 x5 + 2 x2^2 x3 x4 + 2 x0 x2^2 x4 +// p[3]: x5 +// p[4]: x2 x5 x6 - x0 x1 x5 - x0 x5 + x0 x2 x4 +// Sample: x0=1, x1=0, x2=-1, x3=0, x4=3/4, x5=1 +// Counterexample: x0=1, x1=-1, x2=-1, x3=2, x4=1, x5=1, x6=-2 +static void tst_unsound_lws_nullified2() { + std::cout << "=== tst_unsound_lws_nullified2 ===\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); + + 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); + + polynomial_ref _x0(pm), _x1(pm), _x2(pm), _x3(pm), _x4(pm), _x5(pm), _x6(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); + + polynomial_ref p0(pm), p1(pm), p2(pm), p3(pm), p4(pm); + p0 = _x2; + p1 = _x5 + _x4; + p2 = (_x2^2) * _x5 * _x6 + (_x2^2) * _x4 * _x6 + + 2 * (_x2^2) * _x3 * _x5 + _x0 * (_x2^2) * _x5 + - 3 * _x0 * _x1 * _x2 * _x5 - 2 * _x0 * (_x1^2) * _x5 + + 2 * (_x2^2) * _x3 * _x4 + 2 * _x0 * (_x2^2) * _x4; + p3 = _x5; + p4 = _x2 * _x5 * _x6 - _x0 * _x1 * _x5 - _x0 * _x5 + _x0 * _x2 * _x4; + + std::cout << " p0: " << p0 << "\n p1: " << p1 << "\n p2: " << p2 + << "\n p3: " << p3 << "\n p4: " << p4 << "\n"; + + // Sample: x0=1, x1=0, x2=-1, x3=0, x4=3/4, x5=1 + scoped_anum val(am); + rational three_quarter(3, 4); + am.set(val, 1); sample_as.set(x0, val); + am.set(val, 0); sample_as.set(x1, val); + am.set(val, -1); sample_as.set(x2, val); + am.set(val, 0); sample_as.set(x3, val); + am.set(val, three_quarter.to_mpq()); sample_as.set(x4, val); + am.set(val, 1); sample_as.set(x5, val); + + // Counterexample: x0=1, x1=-1, x2=-1, x3=2, x4=1, x5=1, x6=-2 + am.set(val, 1); 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, 2); counter_as.set(x3, val); + am.set(val, 1); counter_as.set(x4, val); + am.set(val, 1); counter_as.set(x5, val); + am.set(val, -2); counter_as.set(x6, val); + + s.set_rvalues(sample_as); + + polynomial_ref_vector polys(pm); + polys.push_back(p0); + polys.push_back(p1); + polys.push_back(p2); + polys.push_back(p3); + polys.push_back(p4); + + nlsat::levelwise lws(s, polys, x6, s.sample(), pm, am, cache); + auto cell = lws.single_cell(); + + std::cout << "Cell intervals:\n"; + for (unsigned i = 0; i < cell.size(); ++i) + nlsat::display(std::cout << " Level " << i << ": ", s, cell[i]) << "\n"; + + bool inside = is_point_inside_cell(am, pm, cell, counter_as); + // The counterexample should be OUTSIDE the cell for soundness. + // This ENSURE will fail, demonstrating the bug. + ENSURE(!inside); + std::cout << "=== END tst_unsound_lws_nullified2 ===\n\n"; +} + void tst_nlsat() { - tst_unsound_gh8397(); + tst_unsound_lws_nullified2(); + std::cout << "------------------\n"; + tst_unsound_lws_nullified(); + std::cout << "------------------\n"; + tst_unsound_lws_p6236(); std::cout << "------------------\n"; tst_unsound_lws_ppblockterm(); std::cout << "------------------\n"; From 7aa1ba1905cfe0bff81937ae907f5545f684afd8 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 17 Feb 2026 20:00:53 -1000 Subject: [PATCH 05/16] a bug fix in levelwise with the section case, where a discriminant was not added, and adding new tests for levelwise Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 4 +- src/test/nlsat.cpp | 540 +++++----------------------------------- 2 files changed, 62 insertions(+), 482 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index a2e527981..d728f40a0 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -1108,8 +1108,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)) - request_factorized(witness); // has roots: witness only + else + add_projection_for_poly(p, m_level, witness, false, true); } } diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 9a650e56d..2380d07a7 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -134,6 +134,34 @@ static bool is_point_inside_cell( return true; } +// Helper: verify that counter_as has a different sign than sample_as on at least +// one polynomial in polys. Only polynomials whose max_var is assigned in BOTH +// assignments are checked. Returns true when at least one sign differs. +static bool has_different_sign( + anum_manager& am, + polynomial::manager& pm, + polynomial_ref_vector const& polys, + nlsat::assignment const& sample_as, + nlsat::assignment const& counter_as) +{ + for (unsigned i = 0; i < polys.size(); ++i) { + polynomial_ref p(polys.get(i), pm); + polynomial::var mv = pm.max_var(p); + if (mv == polynomial::null_var) // constant polynomial + continue; + if (!sample_as.is_assigned(mv) || !counter_as.is_assigned(mv)) + continue; + sign s_sign = am.eval_sign_at(p, sample_as); + sign c_sign = am.eval_sign_at(p, counter_as); + if (s_sign != c_sign) { + std::cout << " p" << i << " has different sign: sample=" << s_sign + << ", counter=" << c_sign << "\n"; + return true; + } + } + return false; +} + nlsat::interval_set_ref tst_interval(nlsat::interval_set_ref const & s1, nlsat::interval_set_ref const & s2, unsigned expected_num_intervals, @@ -167,7 +195,7 @@ nlsat::interval_set_ref tst_interval(nlsat::interval_set_ref const & s1, } static void tst3() { - enable_trace("nlsat_interval"); + // enable_trace("nlsat_interval"); reslimit rl; unsynch_mpq_manager qm; anum_manager am(rl, qm); @@ -353,7 +381,7 @@ static void check_subset_result(nlsat::interval_set_ref const & s1, } static void tst4() { - enable_trace("nlsat_interval"); + // enable_trace("nlsat_interval"); reslimit rl; unsynch_mpq_manager qm; anum_manager am(rl, qm); @@ -1168,7 +1196,7 @@ static void tst_nullified_polynomial() { // Test case for unsound lemma lws2380 - comparing standard projection vs levelwise // The issue: x7 is unconstrained in levelwise output but affects the section polynomial static void tst_unsound_lws2380() { - enable_trace("nlsat_explain"); + // enable_trace("nlsat_explain"); auto run_test = [](bool use_lws) { std::cout << "=== tst_unsound_lws2380: " << (use_lws ? "Levelwise" : "Standard") << " projection (lws=" << use_lws << ") ===\n"; @@ -1337,14 +1365,7 @@ static void tst_unsound_lws_x3() { polynomial_ref p4(pm); p4 = _x3 + _x1 + _x0; - std::cout << "p0: " << p0 << "\n"; - std::cout << "p1: " << p1 << "\n"; - std::cout << "p2: " << p2 << "\n"; - std::cout << "p3: " << p3 << "\n"; - std::cout << "p4: " << p4 << "\n\n"; - - // Set sample: x0=-7, x1=-1, x2=1, x3=? (need to pick a value in the cell) - // For the sample, we need an x3 value. Let's use x3=8 (which is > -x0 = 7, so p0 > 0) + // Set sample: x0=-7, x1=-1, x2=1, x3=8 scoped_anum val(am); am.set(val, -7); sample_as.set(x0, val); am.set(val, -1); sample_as.set(x1, val); @@ -1357,29 +1378,7 @@ static void tst_unsound_lws_x3() { am.set(val, 5); counter_as.set(x2, val); am.set(val, 6); counter_as.set(x3, val); - std::cout << "Sample point: x0=-7, x1=-1, x2=1, x3=8\n"; - std::cout << "Counterexample: x0=-4, x1=-8, x2=5, x3=6\n\n"; - - // Evaluate polynomials at sample - std::cout << "Polynomial signs at SAMPLE:\n"; - std::cout << " p0 sign: " << am.eval_sign_at(p0, sample_as) << "\n"; - std::cout << " p1 sign: " << am.eval_sign_at(p1, sample_as) << "\n"; - std::cout << " p2 sign: " << am.eval_sign_at(p2, sample_as) << "\n"; - std::cout << " p3 sign: " << am.eval_sign_at(p3, sample_as) << "\n"; - std::cout << " p4 sign: " << am.eval_sign_at(p4, sample_as) << "\n\n"; - - // Evaluate polynomials at counterexample - 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"; - std::cout << " p3 sign: " << am.eval_sign_at(p3, counter_as) << "\n"; - std::cout << " p4 sign: " << am.eval_sign_at(p4, counter_as) << "\n\n"; - - // Set solver assignment for levelwise (without x3) - am.set(val, -7); sample_as.set(x0, val); - am.set(val, -1); sample_as.set(x1, val); - am.set(val, 1); sample_as.set(x2, val); + // Set solver assignment for levelwise s.set_rvalues(sample_as); // Build polynomial vector @@ -1391,162 +1390,16 @@ static void tst_unsound_lws_x3() { polys.push_back(p4); unsigned max_x = x3; - - // Print roots of each polynomial at sample - std::cout << "Roots of polynomials at sample (in x3):\n"; - for (unsigned i = 0; i < polys.size(); ++i) { - polynomial_ref p(polys.get(i), pm); - if (pm.max_var(p) != x3) { - std::cout << " p" << i << ": max_var is not x3, skipping\n"; - continue; - } - scoped_anum_vector roots(am); - am.isolate_roots(p, nlsat::undef_var_assignment(sample_as, x3), roots); - std::cout << " p" << i << " roots: "; - if (roots.empty()) { - std::cout << "(none)"; - } else { - for (unsigned j = 0; j < roots.size(); ++j) { - if (j > 0) std::cout << ", "; - am.display_decimal(std::cout, roots[j], 5); - } - } - std::cout << "\n"; - } - std::cout << "\n"; - - // Compute and evaluate resultant of p3 and p4 - std::cout << "Resultant of p3 and p4 (in x3):\n"; - polynomial_ref res_p3_p4(pm); - { - pm.resultant(p3, p4, x3, res_p3_p4); - std::cout << " Res(p3, p4) = "; - pm.display(std::cout, res_p3_p4); - std::cout << "\n"; - std::cout << " Sign at sample (x0=-7, x1=-1, x2=1): " << am.eval_sign_at(res_p3_p4, sample_as) << "\n"; - std::cout << " Sign at counter (x0=-4, x1=-8, x2=5): " << am.eval_sign_at(res_p3_p4, counter_as) << "\n"; - - // Check roots of the resultant at x2 level (parametric in x0, x1) - std::cout << " Roots at sample x0,x1 (in x2): "; - scoped_anum_vector res_roots(am); - nlsat::assignment partial_sample(am); - scoped_anum val(am); - am.set(val, -7); partial_sample.set(x0, val); - am.set(val, -1); partial_sample.set(x1, val); - am.isolate_roots(res_p3_p4, nlsat::undef_var_assignment(partial_sample, x2), res_roots); - for (unsigned j = 0; j < res_roots.size(); ++j) { - if (j > 0) std::cout << ", "; - am.display_decimal(std::cout, res_roots[j], 5); - } - std::cout << "\n"; - - // Check roots at counterexample x0,x1 - std::cout << " Roots at counter x0,x1 (in x2): "; - nlsat::assignment partial_counter(am); - am.set(val, -4); partial_counter.set(x0, val); - am.set(val, -8); partial_counter.set(x1, val); - scoped_anum_vector res_roots_counter(am); - am.isolate_roots(res_p3_p4, nlsat::undef_var_assignment(partial_counter, x2), res_roots_counter); - for (unsigned j = 0; j < res_roots_counter.size(); ++j) { - if (j > 0) std::cout << ", "; - am.display_decimal(std::cout, res_roots_counter[j], 5); - } - std::cout << "\n"; - - // Compute and check discriminant of Res(p3,p4) in x2 - std::cout << "\n Discriminant of Res(p3,p4) in x2:\n"; - polynomial_ref disc_res(pm); - pm.discriminant(res_p3_p4, x2, disc_res); - std::cout << " Disc = "; - pm.display(std::cout, disc_res); - std::cout << "\n"; - std::cout << " Sign at sample (x0=-7, x1=-1): " << am.eval_sign_at(disc_res, sample_as) << "\n"; - std::cout << " Sign at counter (x0=-4, x1=-8): " << am.eval_sign_at(disc_res, counter_as) << "\n"; - } - std::cout << "\n"; - - std::cout << "Running levelwise with max_x = x3\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 (auto const& interval : cell) { - nlsat::display(std::cout << " ", s, interval) << "\n"; - } - // Evaluate cell bounds at counterexample to check if counterexample is in cell - std::cout << "\n--- Checking if counterexample is in cell ---\n"; - std::cout << "For a SECTOR (lower_root, upper_root), variable x satisfies:\n"; - std::cout << " x > lower_root AND x < upper_root\n\n"; - - // For univariate evaluation, we need to substitute lower vars - // Level 0: x0 interval, evaluate at x0=-4 - // Level 1: x1 interval (parametric in x0), evaluate at (x0=-4, x1=-8) - // Level 2: x2 interval (parametric in x0,x1), evaluate at (x0=-4,x1=-8,x2=5) - - bool counterexample_outside_cell = false; - - for (unsigned i = 0; i < cell.size(); ++i) { - auto const& interval = cell[i]; - nlsat::var level = i; - std::cout << "Level " << level << ":\n"; - - // Build assignment up to this level (exclusive) for root isolation - nlsat::assignment partial_as(am); - scoped_anum val(am); - if (level > 0) { am.set(val, -4); partial_as.set(x0, val); } - if (level > 1) { am.set(val, -8); partial_as.set(x1, val); } - if (level > 2) { am.set(val, 5); partial_as.set(x2, val); } - - scoped_anum counter_val(am); - if (level == 0) am.set(counter_val, -4); - else if (level == 1) am.set(counter_val, -8); - else if (level == 2) am.set(counter_val, 5); - - if (interval.is_section()) { - std::cout << " Section case\n"; - } else { - // Isolate roots and check bounds - if (!interval.l_inf()) { - polynomial_ref lower_p(interval.l, pm); - scoped_anum_vector lower_roots(am); - am.isolate_roots(lower_p, nlsat::undef_var_assignment(partial_as, level), lower_roots); - if (lower_roots.size() >= interval.l_index) { - std::cout << " Lower root (root[" << interval.l_index << "]): "; - am.display_decimal(std::cout, lower_roots[interval.l_index - 1], 10); - std::cout << "\n"; - std::cout << " Counter x" << level << " = "; - am.display_decimal(std::cout, counter_val, 10); - int cmp = am.compare(counter_val, lower_roots[interval.l_index - 1]); - std::cout << " -> " << (cmp > 0 ? "ABOVE" : (cmp < 0 ? "BELOW" : "EQUAL")) << " lower bound\n"; - if (cmp <= 0) counterexample_outside_cell = true; - } - } - if (!interval.u_inf()) { - polynomial_ref upper_p(interval.u, pm); - scoped_anum_vector upper_roots(am); - am.isolate_roots(upper_p, nlsat::undef_var_assignment(partial_as, level), upper_roots); - if (upper_roots.size() >= interval.u_index) { - std::cout << " Upper root (root[" << interval.u_index << "]): "; - am.display_decimal(std::cout, upper_roots[interval.u_index - 1], 10); - std::cout << "\n"; - std::cout << " Counter x" << level << " = "; - am.display_decimal(std::cout, counter_val, 10); - int cmp = am.compare(counter_val, upper_roots[interval.u_index - 1]); - std::cout << " -> " << (cmp > 0 ? "ABOVE" : (cmp < 0 ? "BELOW" : "EQUAL")) << " upper bound\n"; - if (cmp >= 0) counterexample_outside_cell = true; - } - } - } - std::cout << "\n"; - } + // Sanity-check: the counterexample must truly be a counterexample + ENSURE(has_different_sign(am, pm, polys, sample_as, counter_as)); - // The counterexample has different polynomial signs than the sample. - // 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"; + // Counterexample must be OUTSIDE the cell + ENSURE(!is_point_inside_cell(am, pm, cell, counter_as)); std::cout << "=== END tst_unsound_lws_x3 ===\n\n"; } @@ -1629,16 +1482,9 @@ static void tst_unsound_lws_n46() { polynomial_ref p4(pm); p4 = _x2 * _x6 * _x7 - 2; - std::cout << "Input polynomials:\n"; - std::cout << " p0: " << p0 << "\n"; - std::cout << " p1: " << p1 << "\n"; - std::cout << " p2: " << p2 << "\n"; - std::cout << " p3: " << p3 << "\n"; - std::cout << " p4: " << p4 << "\n\n"; - // Set sample point: x0=1, x1=2, x2=1, x3=-1, x4=-1, x5=1, x6=7/8 scoped_anum val(am); - rational q(7, 8); // 0.875 = 7/8 + rational q(7, 8); am.set(val, 1); sample_as.set(x0, val); am.set(val, 2); sample_as.set(x1, val); am.set(val, 1); sample_as.set(x2, val); @@ -1647,8 +1493,6 @@ static void tst_unsound_lws_n46() { am.set(val, 1); sample_as.set(x5, val); am.set(val, q.to_mpq()); sample_as.set(x6, val); - std::cout << "Sample point: x0=1, x1=2, x2=1, x3=-1, x4=-1, x5=1, x6=7/8\n"; - // Set counterexample: x0=1, x2=1, x3=0, x4=-9, x5=0, x6=5, x7=0 am.set(val, 1); counter_as.set(x0, val); am.set(val, 0); counter_as.set(x1, val); @@ -1659,8 +1503,6 @@ static void tst_unsound_lws_n46() { am.set(val, 5); counter_as.set(x6, val); am.set(val, 0); counter_as.set(x7, val); - std::cout << "Counterexample: x0=1, x2=1, x3=0, x4=-9, x5=0, x6=5, x7=0\n\n"; - // Set solver assignment for levelwise s.set_rvalues(sample_as); @@ -1675,85 +1517,19 @@ static void tst_unsound_lws_n46() { nlsat::var max_x = x7; // Run levelwise - std::cout << "Running levelwise with max_x = x7...\n"; nlsat::levelwise lws(s, polys, max_x, s.sample(), pm, am, cache); auto cell = lws.single_cell(); - std::cout << "Cell intervals:\n"; - for (unsigned i = 0; i < cell.size(); ++i) { - std::cout << " Level " << i << ": "; - nlsat::display(std::cout, s, cell[i]) << "\n"; - } - - // Print the lemma produced by levelwise - std::cout << "\n--- LEMMA from levelwise ---\n"; - for (unsigned i = 0; i < cell.size(); ++i) { - auto const& interval = cell[i]; - if (interval.section) { - std::cout << "!(x" << i << " = root[" << interval.l_index << "]("; - pm.display(std::cout, interval.l) << "))\n"; - } else { - if (!interval.l_inf()) { - std::cout << "!(x" << i << " > root[" << interval.l_index << "]("; - pm.display(std::cout, interval.l) << "))\n"; - } - if (!interval.u_inf()) { - std::cout << "!(x" << i << " < root[" << interval.u_index << "]("; - pm.display(std::cout, interval.u) << "))\n"; - } - } - } - std::cout << "--- END LEMMA ---\n\n"; - - // Test for the discriminant projection fix: - // - // BUG: When p1 = (x6-1)^2 at the sample (a double root), the discriminant of p1 - // is zero. The function compute_omit_disc_for_same_boundary() incorrectly omitted - // this discriminant because it only checked if p1(sample) != 0, not if disc(p1) = 0. - // - // FIX: Now we also check if disc(p) = 0 at sample, and if so, we keep the discriminant. - // This causes the discriminant's root polynomial (x2*x4 + x0) to be projected, - // creating a section at level 4 that excludes the counterexample. - - std::cout << "=== Verifying discriminant projection fix ===\n"; - - // Check 1: Level 4 should now be a SECTION (not a sector as before the fix) - // The discriminant of p1 w.r.t. x6 has a factor (x2*x4 + x0) that becomes the section + // Verify discriminant projection fix: + // Level 4 should be a SECTION (disc of p1 w.r.t. x6 has factor x2*x4+x0) ENSURE(cell.size() > 4); - ENSURE(cell[4].section); // Level 4 must be a section after the fix - std::cout << "Level 4 is a section: " << (cell[4].section ? "YES (FIX WORKING)" : "NO (BUG!)") << "\n"; + ENSURE(cell[4].section); - // Check 2: The section polynomial at level 4 should be x2*x4 + x0 (or equivalent) - // At sample: x2=1, x0=1, so root is x4 = -x0/x2 = -1 (matches sample x4=-1) - polynomial_ref section_poly(cell[4].l, pm); - std::cout << "Level 4 section polynomial: " << section_poly << "\n"; + // Sanity-check: the counterexample must truly be a counterexample + ENSURE(has_different_sign(am, pm, polys, sample_as, counter_as)); - // Check 3: Verify the counterexample is OUTSIDE the cell - // At counterexample: x2=1, x0=1, so section root is x4 = -1 - // But counterexample has x4 = -9, which is NOT equal to -1 - // Therefore the literal !(x4 = root[1](...)) is TRUE, making the lemma sound - - polynomial_ref x4_section(pm); - x4_section = _x2 * _x4 + _x0; // Expected section polynomial - scoped_anum_vector roots_x4(am); - am.isolate_roots(x4_section, nlsat::undef_var_assignment(counter_as, x4), roots_x4); - - std::cout << "At counterexample:\n"; - std::cout << " Section polynomial: x2*x4 + x0 = x4 + 1\n"; - std::cout << " Section root: x4 = "; - if (!roots_x4.empty()) am.display_decimal(std::cout, roots_x4[0], 6); - std::cout << "\n"; - std::cout << " Counterexample x4 = -9\n"; - - bool x4_at_section = !roots_x4.empty() && am.eq(counter_as.value(x4), roots_x4[0]); - std::cout << " Is x4=-9 equal to section root? " << (x4_at_section ? "YES" : "NO") << "\n"; - - // The fix ensures x4_at_section is FALSE, meaning the counterexample is OUTSIDE the cell - ENSURE(!x4_at_section); // Counterexample must NOT satisfy the section constraint - - std::cout << "\n=== FIX VERIFIED: Counterexample is outside the cell ===\n"; - std::cout << "The lemma literal !(x4 = root[1](x2*x4 + x0)) is TRUE at counterexample.\n"; - std::cout << "Therefore the lemma is SOUND (disjunction has a true literal).\n"; + // Counterexample must be OUTSIDE the cell + ENSURE(!is_point_inside_cell(am, pm, cell, counter_as)); std::cout << "=== END tst_unsound_lws_n46 ===\n\n"; } @@ -1817,11 +1593,6 @@ static void tst_unsound_lws_et4() { polynomial_ref p3(pm); p3 = _x5 - 9; - std::cout << "p0: " << p0 << "\n"; - std::cout << "p1: " << p1 << "\n"; - std::cout << "p2: " << p2 << "\n"; - std::cout << "p3: " << p3 << "\n\n"; - // Sample: x0=4, x1=5, x2=3.5, x3=-8, x4=5 scoped_anum val(am); am.set(val, 4); sample_as.set(x0, val); @@ -1834,18 +1605,13 @@ static void tst_unsound_lws_et4() { // Counterexample: x0=5, x3=3, x4=0, x5=0 am.set(val, 5); counter_as.set(x0, val); - am.set(val, 5); counter_as.set(x1, val); // use same as sample - am.set(val, q.to_mpq()); counter_as.set(x2, val); // use same as sample + am.set(val, 5); counter_as.set(x1, val); + am.set(val, q.to_mpq()); counter_as.set(x2, val); am.set(val, 3); counter_as.set(x3, val); am.set(val, 0); counter_as.set(x4, val); am.set(val, 0); counter_as.set(x5, val); - std::cout << "Sample point: x0=4, x1=5, x2=3.5, x3=-8, x4=5\n"; - std::cout << "Counterexample: x0=5, x3=3, x4=0, x5=0\n\n"; - - // Evaluate polynomials at sample (need to set x5 for evaluation) - scoped_anum sample_x5(am); - am.set(sample_x5, 0); // pick some value in the cell + // sample_full includes x5=0 for sign evaluation nlsat::assignment sample_full(am); am.set(val, 4); sample_full.set(x0, val); am.set(val, 5); sample_full.set(x1, val); @@ -1853,19 +1619,6 @@ static void tst_unsound_lws_et4() { am.set(val, -8); sample_full.set(x3, val); am.set(val, 5); sample_full.set(x4, val); am.set(val, 0); sample_full.set(x5, val); - - std::cout << "Polynomial signs at SAMPLE (with x5=0):\n"; - std::cout << " p0 sign: " << am.eval_sign_at(p0, sample_full) << "\n"; - std::cout << " p1 sign: " << am.eval_sign_at(p1, sample_full) << "\n"; - std::cout << " p2 sign: " << am.eval_sign_at(p2, sample_full) << "\n"; - std::cout << " p3 sign: " << am.eval_sign_at(p3, sample_full) << "\n\n"; - - // Evaluate polynomials at counterexample - 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"; - std::cout << " p3 sign: " << am.eval_sign_at(p3, counter_as) << "\n\n"; // Set solver assignment for levelwise (without x5) s.set_rvalues(sample_as); @@ -1878,110 +1631,16 @@ static void tst_unsound_lws_et4() { polys.push_back(p3); unsigned max_x = x5; - - // Print roots of each polynomial at sample - std::cout << "Roots of polynomials at sample (in x5):\n"; - for (unsigned i = 0; i < polys.size(); ++i) { - polynomial_ref p(polys.get(i), pm); - if (pm.max_var(p) != x5) { - std::cout << " p" << i << ": max_var is not x5, skipping\n"; - continue; - } - scoped_anum_vector roots(am); - am.isolate_roots(p, nlsat::undef_var_assignment(sample_as, x5), roots); - std::cout << " p" << i << " roots: "; - if (roots.empty()) { - std::cout << "(none)"; - } else { - for (unsigned j = 0; j < roots.size(); ++j) { - if (j > 0) std::cout << ", "; - am.display_decimal(std::cout, roots[j], 5); - } - } - std::cout << "\n"; - } - std::cout << "\n"; - - std::cout << "Running levelwise with max_x = x5\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 (auto const& interval : cell) { - nlsat::display(std::cout << " ", s, interval) << "\n"; - } - // Evaluate cell bounds at counterexample to check if counterexample is in cell - std::cout << "\n--- Checking if counterexample is in cell ---\n"; - - bool counterexample_outside_cell = false; - - for (unsigned i = 0; i < cell.size(); ++i) { - auto const& interval = cell[i]; - nlsat::var level = i; - std::cout << "Level " << level << " (x" << level << "):\n"; - - // Build assignment up to this level (exclusive) for root isolation - nlsat::assignment partial_as(am); - scoped_anum val(am); - if (level > 0) { am.set(val, 5); partial_as.set(x0, val); } // counter x0 - if (level > 1) { am.set(val, 5); partial_as.set(x1, val); } - if (level > 2) { am.set(val, q.to_mpq()); partial_as.set(x2, val); } - if (level > 3) { am.set(val, 3); partial_as.set(x3, val); } // counter x3 - if (level > 4) { am.set(val, 0); partial_as.set(x4, val); } // counter x4 - - scoped_anum counter_val(am); - if (level == 0) am.set(counter_val, 5); // x0 - else if (level == 1) am.set(counter_val, 5); - else if (level == 2) am.set(counter_val, q.to_mpq()); - else if (level == 3) am.set(counter_val, 3); // x3 - else if (level == 4) am.set(counter_val, 0); // x4 - else if (level == 5) am.set(counter_val, 0); // x5 - - if (interval.is_section()) { - std::cout << " Section case\n"; - } else { - // Isolate roots and check bounds - if (!interval.l_inf()) { - polynomial_ref lower_p(interval.l, pm); - scoped_anum_vector lower_roots(am); - am.isolate_roots(lower_p, nlsat::undef_var_assignment(partial_as, level), lower_roots); - if (lower_roots.size() >= interval.l_index) { - std::cout << " Lower root (root[" << interval.l_index << "]): "; - am.display_decimal(std::cout, lower_roots[interval.l_index - 1], 10); - std::cout << "\n"; - std::cout << " Counter x" << level << " = "; - am.display_decimal(std::cout, counter_val, 10); - int cmp = am.compare(counter_val, lower_roots[interval.l_index - 1]); - std::cout << " -> " << (cmp > 0 ? "ABOVE" : (cmp < 0 ? "BELOW" : "EQUAL")) << " lower bound\n"; - if (cmp <= 0) counterexample_outside_cell = true; - } - } - if (!interval.u_inf()) { - polynomial_ref upper_p(interval.u, pm); - scoped_anum_vector upper_roots(am); - am.isolate_roots(upper_p, nlsat::undef_var_assignment(partial_as, level), upper_roots); - if (upper_roots.size() >= interval.u_index) { - std::cout << " Upper root (root[" << interval.u_index << "]): "; - am.display_decimal(std::cout, upper_roots[interval.u_index - 1], 10); - std::cout << "\n"; - std::cout << " Counter x" << level << " = "; - am.display_decimal(std::cout, counter_val, 10); - int cmp = am.compare(counter_val, upper_roots[interval.u_index - 1]); - std::cout << " -> " << (cmp > 0 ? "ABOVE" : (cmp < 0 ? "BELOW" : "EQUAL")) << " upper bound\n"; - if (cmp >= 0) counterexample_outside_cell = true; - } - } - } - std::cout << "\n"; - } + // Sanity-check: the counterexample must truly be a counterexample + ENSURE(has_different_sign(am, pm, polys, sample_full, counter_as)); - // The counterexample has different polynomial signs than the sample. - // 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"; + // Counterexample must be OUTSIDE the cell + ENSURE(!is_point_inside_cell(am, pm, cell, counter_as)); std::cout << "=== END tst_unsound_lws_et4 ===\n\n"; } @@ -2154,6 +1813,10 @@ static void tst_unsound_lws_disc_zero() { // For a sound cell, if polynomial signs differ, counter MUST be outside the cell // The fix (projecting p0's discriminant) should create bounds that exclude the counterexample + // Sanity-check: the counterexample must truly be a counterexample, + // i.e. at least one input polynomial has a different sign. + ENSURE(has_different_sign(am, pm, polys, sample_as, counter_as)); + if (p0_sample != p0_counter) { std::cout << "\nPoly signs differ between sample and counter.\n"; std::cout << "For cell to be sound, counter must be OUTSIDE the cell.\n"; @@ -2309,25 +1972,9 @@ static void tst_unsound_lws_ppblockterm() { std::cout << "--- END LEMMA ---\n\n"; - // Check polynomial signs at sample and counterexample - int p0_sample = am.eval_sign_at(p0, sample_as); - int p1_sample = am.eval_sign_at(p1, sample_as); - int p2_sample = am.eval_sign_at(p2, sample_as); - int p3_sample = am.eval_sign_at(p3, sample_as); - - int p0_counter = am.eval_sign_at(p0, counter_as); - int p1_counter = am.eval_sign_at(p1, counter_as); - int p2_counter = am.eval_sign_at(p2, counter_as); - int p3_counter = am.eval_sign_at(p3, counter_as); - - bool signs_differ = (p0_sample != p0_counter) || (p1_sample != p1_counter) || - (p2_sample != p2_counter) || (p3_sample != p3_counter); - - if (signs_differ) { - std::cout << "Polynomial signs DIFFER between sample and counterexample.\n"; - } else { - std::cout << "Polynomial signs match between sample and counterexample.\n"; - } + // Sanity-check: the counterexample must truly be a counterexample, + // i.e. at least one input polynomial has a different sign. + ENSURE(has_different_sign(am, pm, polys, sample_as, counter_as)); // Verify that the counterexample is OUTSIDE the cell (cell is sound) std::cout << "\nChecking if counterexample is inside cell:\n"; @@ -2671,74 +2318,7 @@ static void tst_unsound_lws_p6236() { // Check if counterexample is inside the cell std::cout << "\n--- Checking if counterexample is in cell ---\n"; - bool counterexample_outside_cell = false; - - // Counter values for each level - int counter_vals[] = {0, -1, 1, -1, 1, 0, 0, 0, 0, 1, 0, 3, 1, 0, 0, 0}; - - for (unsigned i = 0; i < cell.size(); ++i) { - auto const& interval = cell[i]; - nlsat::var level = i; - std::cout << "Level " << level << " (x" << level << "):\n"; - - // Build assignment up to this level (exclusive) using counterexample values - nlsat::assignment partial_as(am); - scoped_anum pval(am); - for (unsigned j = 0; j < level; ++j) { - am.set(pval, counter_vals[j]); - partial_as.set(j, pval); - } - // Special case: x11 at counter is 3 (integer, handled above) - - scoped_anum counter_val(am); - am.set(counter_val, counter_vals[level]); - - if (interval.is_section()) { - // Section: counterexample must be at the root - polynomial_ref sec_p(interval.l, pm); - scoped_anum_vector roots(am); - am.isolate_roots(sec_p, nlsat::undef_var_assignment(partial_as, level), roots); - if (roots.size() >= interval.l_index) { - bool at_root = am.eq(counter_val, roots[interval.l_index - 1]); - std::cout << " Section root[" << interval.l_index << "]: "; - am.display_decimal(std::cout, roots[interval.l_index - 1], 10); - std::cout << ", counter = "; - am.display_decimal(std::cout, counter_val, 10); - std::cout << " -> " << (at_root ? "AT ROOT" : "NOT AT ROOT") << "\n"; - if (!at_root) counterexample_outside_cell = true; - } - } else { - if (!interval.l_inf()) { - polynomial_ref lower_p(interval.l, pm); - scoped_anum_vector lower_roots(am); - am.isolate_roots(lower_p, nlsat::undef_var_assignment(partial_as, level), lower_roots); - if (lower_roots.size() >= interval.l_index) { - int cmp = am.compare(counter_val, lower_roots[interval.l_index - 1]); - std::cout << " Lower root[" << interval.l_index << "]: "; - am.display_decimal(std::cout, lower_roots[interval.l_index - 1], 10); - std::cout << ", counter = "; - am.display_decimal(std::cout, counter_val, 10); - std::cout << " -> " << (cmp > 0 ? "ABOVE" : (cmp < 0 ? "BELOW" : "EQUAL")) << "\n"; - if (cmp <= 0) counterexample_outside_cell = true; - } - } - if (!interval.u_inf()) { - polynomial_ref upper_p(interval.u, pm); - scoped_anum_vector upper_roots(am); - am.isolate_roots(upper_p, nlsat::undef_var_assignment(partial_as, level), upper_roots); - if (upper_roots.size() >= interval.u_index) { - int cmp = am.compare(counter_val, upper_roots[interval.u_index - 1]); - std::cout << " Upper root[" << interval.u_index << "]: "; - am.display_decimal(std::cout, upper_roots[interval.u_index - 1], 10); - std::cout << ", counter = "; - am.display_decimal(std::cout, counter_val, 10); - std::cout << " -> " << (cmp > 0 ? "ABOVE" : (cmp < 0 ? "BELOW" : "EQUAL")) << "\n"; - if (cmp >= 0) counterexample_outside_cell = true; - } - } - } - std::cout << "\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); From 05029c6f0321337e84cc0e346bbb9cd27a38c5c3 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Feb 2026 06:33:52 -1000 Subject: [PATCH 06/16] work on nl testing Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_explain.cpp | 6 +----- src/nlsat/nlsat_solver.cpp | 24 ++++++++++++++++++++---- src/test/nlsat.cpp | 6 ++++-- 3 files changed, 25 insertions(+), 11 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 48e23c81d..d5aadf683 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1084,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; @@ -1142,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; diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index ca7e8a2f3..b14c627c8 100644 --- a/src/nlsat/nlsat_solver.cpp +++ 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)); } diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 2380d07a7..0cf3c8912 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -2505,12 +2505,14 @@ static void tst_unsound_lws_nullified2() { } void tst_nlsat() { + tst_unsound_lws_p6236(); + std::cout << "------------------\n"; + tst_unsound_lws_disc_zero(); + std::cout << "------------------\n"; tst_unsound_lws_nullified2(); std::cout << "------------------\n"; tst_unsound_lws_nullified(); std::cout << "------------------\n"; - tst_unsound_lws_p6236(); - std::cout << "------------------\n"; tst_unsound_lws_ppblockterm(); std::cout << "------------------\n"; tst_unsound_lws_n46(); From 138828259a8d6d07360e5d20cee44a2759a7f36a Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Feb 2026 07:08:56 -1000 Subject: [PATCH 07/16] add a test with compute_conflict_explanation call Signed-off-by: Lev Nachmanson --- src/test/nlsat.cpp | 143 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 143 insertions(+) diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 0cf3c8912..6d59a7ff5 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -2504,7 +2504,150 @@ static void tst_unsound_lws_nullified2() { std::cout << "=== END tst_unsound_lws_nullified2 ===\n\n"; } +// Test that compute_conflict_explanation produces a lemma where the counterexample +// falsifies at least one literal. Reproducer from p6236_terminationG_0.smt2. +static void tst_explain_p6236() { + std::cout << "=== tst_explain_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); + + // 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), _x3(pm), _x4(pm), _x5(pm), _x6(pm); + polynomial_ref _x9(pm), _x10(pm), _x11(pm), _x13(pm), _x14(pm), _x15(pm); + _x0 = pm.mk_polynomial(x0); + _x3 = pm.mk_polynomial(x3); + _x4 = pm.mk_polynomial(x4); + _x5 = pm.mk_polynomial(x5); + _x6 = pm.mk_polynomial(x6); + _x9 = pm.mk_polynomial(x9); + _x10 = pm.mk_polynomial(x10); + _x11 = pm.mk_polynomial(x11); + _x13 = pm.mk_polynomial(x13); + _x14 = pm.mk_polynomial(x14); + _x15 = pm.mk_polynomial(x15); + + // p1: -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; + + // p2: x15 + x6*x13 + x0*x4 + polynomial_ref p2(pm); + p2 = _x15 + _x6 * _x13 + _x0 * _x4; + + // Build justification literals: + // jst lit[0]: !(x15 < root[1](p1)) => literal(root_lt_bvar, true) + // jst lit[1]: !(p2 > 0) => literal(gt_bvar, true) + nlsat::bool_var root_lt_bvar = s.mk_root_atom(nlsat::atom::ROOT_LT, x15, 1, p1.get()); + nlsat::literal jst_lit0(root_lt_bvar, true); // negated: !(x15 < root[1](p1)) + + nlsat::literal gt_lit = mk_gt(s, p2.get()); + nlsat::literal jst_lit1 = ~gt_lit; // negated: !(p2 > 0) + + nlsat::literal jst_lits[2] = { jst_lit0, jst_lit1 }; + + // 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); + set_assignment_value(sample_as, am, x0, rational(1)); + set_assignment_value(sample_as, am, x1, rational(-1)); + set_assignment_value(sample_as, am, x2, rational(1)); + set_assignment_value(sample_as, am, x3, rational(-1)); + set_assignment_value(sample_as, am, x4, rational(2)); + set_assignment_value(sample_as, am, x5, rational(0)); + set_assignment_value(sample_as, am, x6, rational(0)); + set_assignment_value(sample_as, am, x7, rational(0)); + set_assignment_value(sample_as, am, x8, rational(0)); + set_assignment_value(sample_as, am, x9, rational(1)); + set_assignment_value(sample_as, am, x10, rational(0)); + set_assignment_value(sample_as, am, x11, half); + set_assignment_value(sample_as, am, x12, rational(1)); + set_assignment_value(sample_as, am, x13, rational(-4)); + set_assignment_value(sample_as, am, x14, rational(2)); + + s.set_rvalues(sample_as); + + // Compute conflict explanation + nlsat::explain& ex = s.get_explain(); + nlsat::scoped_literal_vector result(s); + ex.compute_conflict_explanation(2, jst_lits, result); + + // Build the full lemma: result literals + ~jst_lits + nlsat::literal_vector lemma; + for (unsigned i = 0; i < result.size(); ++i) + lemma.push_back(result[i]); + lemma.push_back(~jst_lits[0]); // x15 < root[1](p1) + lemma.push_back(~jst_lits[1]); // p2 > 0 + + std::cout << "Lemma (" << lemma.size() << " literals):\n"; + s.display(std::cout << " ", lemma.size(), lemma.data()) << "\n"; + + // Counterexample: x0=0,x3=-1,x4=1,x5=0,x6=0,x9=1,x10=0,x11=3,x13=0,x14=0,x15=0 + set_assignment_value(counter_as, am, x0, rational(0)); + set_assignment_value(counter_as, am, x1, rational(-1)); + set_assignment_value(counter_as, am, x2, rational(1)); + set_assignment_value(counter_as, am, x3, rational(-1)); + set_assignment_value(counter_as, am, x4, rational(1)); + set_assignment_value(counter_as, am, x5, rational(0)); + set_assignment_value(counter_as, am, x6, rational(0)); + set_assignment_value(counter_as, am, x7, rational(0)); + set_assignment_value(counter_as, am, x8, rational(0)); + set_assignment_value(counter_as, am, x9, rational(1)); + set_assignment_value(counter_as, am, x10, rational(0)); + set_assignment_value(counter_as, am, x11, rational(3)); + set_assignment_value(counter_as, am, x12, rational(1)); + set_assignment_value(counter_as, am, x13, rational(0)); + set_assignment_value(counter_as, am, x14, rational(0)); + set_assignment_value(counter_as, am, x15, rational(0)); + + // Set counterexample as the solver's assignment for evaluation + s.set_rvalues(counter_as); + nlsat::evaluator& ev = s.get_evaluator(); + + // Check unsat + bool unsat = true; + for (unsigned i = 0; i < lemma.size(); ++i) { + nlsat::literal lit = lemma[i]; + nlsat::atom* a = s.bool_var2atom(lit.var()); + if (a == nullptr) + continue; + bool sat = ev.eval(a, lit.sign()); + std::cout << " lit[" << i << "]: "; + s.display(std::cout, lit) << " = " << (sat ? "true" : "false") << "\n"; + if (sat) + unsat = false; + } + + ENSURE(unsat); + std::cout << "=== END tst_explain_p6236 ===\n\n"; +} + void tst_nlsat() { + tst_explain_p6236(); + std::cout << "------------------\n"; tst_unsound_lws_p6236(); std::cout << "------------------\n"; tst_unsound_lws_disc_zero(); From b60e0e0dd33fdd3ce5a655146d8d2e75409ae8a7 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Feb 2026 07:23:22 -1000 Subject: [PATCH 08/16] keep literals alive Signed-off-by: Lev Nachmanson --- src/test/nlsat.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 6d59a7ff5..1920d569a 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -2562,9 +2562,11 @@ static void tst_explain_p6236() { // jst lit[0]: !(x15 < root[1](p1)) => literal(root_lt_bvar, true) // jst lit[1]: !(p2 > 0) => literal(gt_bvar, true) nlsat::bool_var root_lt_bvar = s.mk_root_atom(nlsat::atom::ROOT_LT, x15, 1, p1.get()); + s.inc_ref(root_lt_bvar); nlsat::literal jst_lit0(root_lt_bvar, true); // negated: !(x15 < root[1](p1)) nlsat::literal gt_lit = mk_gt(s, p2.get()); + s.inc_ref(gt_lit); nlsat::literal jst_lit1 = ~gt_lit; // negated: !(p2 > 0) nlsat::literal jst_lits[2] = { jst_lit0, jst_lit1 }; @@ -2642,6 +2644,9 @@ static void tst_explain_p6236() { } ENSURE(unsat); + + s.dec_ref(root_lt_bvar); + s.dec_ref(gt_lit); std::cout << "=== END tst_explain_p6236 ===\n\n"; } From df419c137dfdaa6e89831531242ea036df72af8f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Feb 2026 07:47:16 -1000 Subject: [PATCH 09/16] fix the test Signed-off-by: Lev Nachmanson --- src/test/nlsat.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 1920d569a..8e6261e70 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -2629,21 +2629,21 @@ static void tst_explain_p6236() { s.set_rvalues(counter_as); nlsat::evaluator& ev = s.get_evaluator(); - // Check unsat - bool unsat = true; + // At least one lemma literal must be true at the counterexample for soundness + bool some_true = false; for (unsigned i = 0; i < lemma.size(); ++i) { nlsat::literal lit = lemma[i]; nlsat::atom* a = s.bool_var2atom(lit.var()); if (a == nullptr) continue; - bool sat = ev.eval(a, lit.sign()); + bool v = ev.eval(a, lit.sign()); std::cout << " lit[" << i << "]: "; - s.display(std::cout, lit) << " = " << (sat ? "true" : "false") << "\n"; - if (sat) - unsat = false; + s.display(std::cout, lit) << " = " << (v ? "true" : "false") << "\n"; + if (v) + some_true = true; } - ENSURE(unsat); + ENSURE(some_true); s.dec_ref(root_lt_bvar); s.dec_ref(gt_lit); From d8f2b5ca0139d7f98fe7ed8d82e390f32a546ce1 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Feb 2026 10:54:39 -1000 Subject: [PATCH 10/16] 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(); From 799fc9e8c4d7b3e5e91bdb14b2810bb2a787f21f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Feb 2026 10:59:41 -1000 Subject: [PATCH 11/16] hook up a test Signed-off-by: Lev Nachmanson --- src/test/nlsat.cpp | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 4a6d65beb..81d0cab9e 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -466,16 +466,6 @@ static void project_fa(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsig std::cout << ")\n"; } -static bool literal_holds(nlsat::solver& s, nlsat::evaluator& eval, nlsat::literal l) { - if (l == nlsat::true_literal) - return true; - if (l == nlsat::false_literal) - return false; - nlsat::atom* a = s.bool_var2atom(l.var()); - ENSURE(a != nullptr); - return eval.eval(a, l.sign()); -} - static nlsat::literal mk_gt(nlsat::solver& s, nlsat::poly* p) { nlsat::poly * _p[1] = { p }; bool is_even[1] = { false }; @@ -2492,6 +2482,8 @@ static void tst_explain_p6236() { } void tst_nlsat() { + tst_unsound_gh8397(); + std::cout << "------------------\n"; tst_explain_p6236(); std::cout << "------------------\n"; tst_unsound_lws_disc_zero(); From d1461de8a76c0247bf4f2ca2708f2419205163b7 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Feb 2026 12:02:56 -1000 Subject: [PATCH 12/16] fix nlsat.cpp and enable control over what added in handle_nullified_poly Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 68 +++++++++++++++++++++----------------- src/nlsat/nlsat_params.pyg | 2 ++ src/nlsat/nlsat_solver.cpp | 8 +++++ src/nlsat/nlsat_solver.h | 2 ++ 4 files changed, 50 insertions(+), 30 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index e01aa15bc..22297d4e6 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -55,6 +55,8 @@ namespace nlsat { unsigned m_level = 0; // current level being processed unsigned m_spanning_tree_threshold = 3; // minimum both-side count for spanning tree + bool m_null_coeffs = true; + bool m_null_derivs = true; unsigned m_l_rf = UINT_MAX; // position of lower bound in m_rel.m_rfunc unsigned m_u_rf = UINT_MAX; // position of upper bound in m_rel.m_rfunc, UINT_MAX in section case @@ -260,6 +262,8 @@ namespace nlsat { m_I.emplace_back(m_pm); m_spanning_tree_threshold = m_solver.lws_spt_threshold(); + m_null_coeffs = m_solver.lws_null_coeffs(); + m_null_derivs = m_solver.lws_null_derivs(); } // Handle a polynomial whose every coefficient evaluates to zero at the sample. @@ -268,43 +272,47 @@ namespace nlsat { // 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 (w.r.t. 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); + if (m_null_coeffs) { + 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) + if (m_null_derivs) { + 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; - 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; + 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); } - 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); } - 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); } } @@ -1225,7 +1233,7 @@ namespace nlsat { polynomial_ref w = choose_nonzero_coeff(p, m_level); if (!w) 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); diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg index 1ab305984..c29bd648c 100644 --- a/src/nlsat/nlsat_params.pyg +++ b/src/nlsat/nlsat_params.pyg @@ -24,5 +24,7 @@ def_module_params('nlsat', ('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only"), ('lws', BOOL, True, "apply levelwise."), ('lws_spt_threshold', UINT, 2, "minimum both-side polynomial count to apply spanning tree optimization; < 2 disables spanning tree"), + ('lws_null_coeffs', BOOL, True, "add coefficients of nullified polynomials during projection."), + ('lws_null_derivs', BOOL, True, "add derivatives of nullified polynomials during projection."), ('canonicalize', BOOL, True, "canonicalize polynomials.") )) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index b14c627c8..ee875440f 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -251,6 +251,8 @@ namespace nlsat { bool m_apply_lws; bool m_last_conflict_used_lws = false; // Track if last conflict explanation used levelwise unsigned m_lws_spt_threshold = 3; + bool m_lws_null_coeffs = true; + bool m_lws_null_derivs = true; imp(solver& s, ctx& c): m_ctx(c), m_solver(s), @@ -312,6 +314,8 @@ namespace nlsat { m_debug_known_solution_file_name = p.known_sat_assignment_file_name(); m_apply_lws = p.lws(); m_lws_spt_threshold = p.lws_spt_threshold(); // 0 disables spanning tree + m_lws_null_coeffs = p.lws_null_coeffs(); + m_lws_null_derivs = p.lws_null_derivs(); m_check_lemmas |= !(m_debug_known_solution_file_name.empty()); m_ism.set_seed(m_random_seed); @@ -4721,4 +4725,8 @@ namespace nlsat { unsigned solver::lws_spt_threshold() const { return m_imp->m_lws_spt_threshold; } + bool solver::lws_null_coeffs() const { return m_imp->m_lws_null_coeffs; } + + bool solver::lws_null_derivs() const { return m_imp->m_lws_null_derivs; } + }; diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index 566a7c09e..44cc56cb9 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -249,6 +249,8 @@ namespace nlsat { assignment& sample(); bool apply_levelwise() const; unsigned lws_spt_threshold() const; + bool lws_null_coeffs() const; + bool lws_null_derivs() const; void reset(); void collect_statistics(statistics & st); void reset_statistics(); From aff0a82914a20008194387980c63c1e65c2e2e5b Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Feb 2026 12:47:42 -1000 Subject: [PATCH 13/16] disable control over what added in handle_nullified_poly Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 68 +++++++++++++++++--------------------- src/nlsat/nlsat_params.pyg | 2 -- src/nlsat/nlsat_solver.cpp | 13 ++------ src/nlsat/nlsat_solver.h | 2 -- 4 files changed, 33 insertions(+), 52 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 22297d4e6..80409754c 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -55,8 +55,6 @@ namespace nlsat { unsigned m_level = 0; // current level being processed unsigned m_spanning_tree_threshold = 3; // minimum both-side count for spanning tree - bool m_null_coeffs = true; - bool m_null_derivs = true; unsigned m_l_rf = UINT_MAX; // position of lower bound in m_rel.m_rfunc unsigned m_u_rf = UINT_MAX; // position of upper bound in m_rel.m_rfunc, UINT_MAX in section case @@ -262,8 +260,6 @@ namespace nlsat { m_I.emplace_back(m_pm); m_spanning_tree_threshold = m_solver.lws_spt_threshold(); - m_null_coeffs = m_solver.lws_null_coeffs(); - m_null_derivs = m_solver.lws_null_derivs(); } // Handle a polynomial whose every coefficient evaluates to zero at the sample. @@ -272,48 +268,46 @@ namespace nlsat { // 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 (w.r.t. m_level) to m_todo. - if (m_null_coeffs) { - 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); - } + 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. - if (m_null_derivs) { - 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) + 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; - 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); + 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); } + 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) { diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg index c29bd648c..1ab305984 100644 --- a/src/nlsat/nlsat_params.pyg +++ b/src/nlsat/nlsat_params.pyg @@ -24,7 +24,5 @@ def_module_params('nlsat', ('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only"), ('lws', BOOL, True, "apply levelwise."), ('lws_spt_threshold', UINT, 2, "minimum both-side polynomial count to apply spanning tree optimization; < 2 disables spanning tree"), - ('lws_null_coeffs', BOOL, True, "add coefficients of nullified polynomials during projection."), - ('lws_null_derivs', BOOL, True, "add derivatives of nullified polynomials during projection."), ('canonicalize', BOOL, True, "canonicalize polynomials.") )) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index ee875440f..1c83b5e10 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -251,8 +251,6 @@ namespace nlsat { bool m_apply_lws; bool m_last_conflict_used_lws = false; // Track if last conflict explanation used levelwise unsigned m_lws_spt_threshold = 3; - bool m_lws_null_coeffs = true; - bool m_lws_null_derivs = true; imp(solver& s, ctx& c): m_ctx(c), m_solver(s), @@ -314,8 +312,6 @@ namespace nlsat { m_debug_known_solution_file_name = p.known_sat_assignment_file_name(); m_apply_lws = p.lws(); m_lws_spt_threshold = p.lws_spt_threshold(); // 0 disables spanning tree - m_lws_null_coeffs = p.lws_null_coeffs(); - m_lws_null_derivs = p.lws_null_derivs(); m_check_lemmas |= !(m_debug_known_solution_file_name.empty()); m_ism.set_seed(m_random_seed); @@ -4720,13 +4716,8 @@ namespace nlsat { assumption solver::join(assumption a, assumption b) { return (m_imp->m_asm.mk_join(static_cast(a), static_cast(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; } - - bool solver::lws_null_coeffs() const { return m_imp->m_lws_null_coeffs; } - - bool solver::lws_null_derivs() const { return m_imp->m_lws_null_derivs; } - + }; diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index 44cc56cb9..566a7c09e 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -249,8 +249,6 @@ namespace nlsat { assignment& sample(); bool apply_levelwise() const; unsigned lws_spt_threshold() const; - bool lws_null_coeffs() const; - bool lws_null_derivs() const; void reset(); void collect_statistics(statistics & st); void reset_statistics(); From 1e985ea96e4d489b3fba01a16a23f034a0224a2f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Feb 2026 13:14:59 -1000 Subject: [PATCH 14/16] enable optional failure in levelwise Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 20 +++++++++++++++++++- src/nlsat/levelwise.h | 1 + src/nlsat/nlsat_explain.cpp | 2 ++ src/nlsat/nlsat_params.pyg | 1 + src/nlsat/nlsat_solver.cpp | 6 +++++- src/nlsat/nlsat_solver.h | 1 + 6 files changed, 29 insertions(+), 2 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 80409754c..5c6981004 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -32,6 +32,8 @@ static void vec_setx(std_vector& v, unsigned idx, T val, T def) { namespace nlsat { + struct nullified_poly_exception {}; + // The three projection modes for a level: // 1. section_biggest_cell: Sample is on a root. All disc/lc added. // 2. sector_biggest_cell: Sample between roots. noLdcf optimization only. @@ -55,6 +57,8 @@ namespace nlsat { unsigned m_level = 0; // current level being processed unsigned m_spanning_tree_threshold = 3; // minimum both-side count for spanning tree + bool m_null_fail = false; + bool m_fail = false; unsigned m_l_rf = UINT_MAX; // position of lower bound in m_rel.m_rfunc unsigned m_u_rf = UINT_MAX; // position of upper bound in m_rel.m_rfunc, UINT_MAX in section case @@ -260,6 +264,7 @@ namespace nlsat { m_I.emplace_back(m_pm); m_spanning_tree_threshold = m_solver.lws_spt_threshold(); + m_null_fail = m_solver.lws_null_fail(); } // Handle a polynomial whose every coefficient evaluates to zero at the sample. @@ -267,6 +272,8 @@ namespace nlsat { // 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) { + if (m_null_fail) + throw nullified_poly_exception(); // Add all coefficients of p (w.r.t. m_level) to m_todo. unsigned deg = m_pm.degree(p, m_level); for (unsigned j = 0; j <= deg; ++j) { @@ -1295,7 +1302,7 @@ namespace nlsat { } } - std_vector single_cell() { + std_vector single_cell_work() { TRACE(lws, tout << "Input polynomials (" << m_P.size() << "):\n"; for (unsigned i = 0; i < m_P.size(); ++i) @@ -1342,6 +1349,16 @@ namespace nlsat { return m_I; } + + std_vector single_cell() { + try { + return single_cell_work(); + } + catch (nullified_poly_exception&) { + m_fail = true; + return m_I; + } + } }; levelwise::levelwise( @@ -1360,6 +1377,7 @@ namespace nlsat { return m_impl->single_cell(); } + bool levelwise::failed() const { return m_impl->m_fail; } } // namespace nlsat diff --git a/src/nlsat/levelwise.h b/src/nlsat/levelwise.h index 950bee641..27e379374 100644 --- a/src/nlsat/levelwise.h +++ b/src/nlsat/levelwise.h @@ -46,6 +46,7 @@ namespace nlsat { levelwise(levelwise const&) = delete; levelwise& operator=(levelwise const&) = delete; std_vector single_cell(); + bool failed() const; }; // diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index d5aadf683..3240cae2a 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1048,6 +1048,8 @@ 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. diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg index 1ab305984..9d1ed45fc 100644 --- a/src/nlsat/nlsat_params.pyg +++ b/src/nlsat/nlsat_params.pyg @@ -24,5 +24,6 @@ def_module_params('nlsat', ('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only"), ('lws', BOOL, True, "apply levelwise."), ('lws_spt_threshold', UINT, 2, "minimum both-side polynomial count to apply spanning tree optimization; < 2 disables spanning tree"), + ('lws_null_fail', BOOL, False, "fail levelwise projection on nullified polynomials and fall back to standard projection."), ('canonicalize', BOOL, True, "canonicalize polynomials.") )) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 1c83b5e10..eba014358 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -251,6 +251,7 @@ namespace nlsat { bool m_apply_lws; bool m_last_conflict_used_lws = false; // Track if last conflict explanation used levelwise unsigned m_lws_spt_threshold = 3; + bool m_lws_null_fail = false; imp(solver& s, ctx& c): m_ctx(c), m_solver(s), @@ -312,6 +313,7 @@ namespace nlsat { m_debug_known_solution_file_name = p.known_sat_assignment_file_name(); m_apply_lws = p.lws(); m_lws_spt_threshold = p.lws_spt_threshold(); // 0 disables spanning tree + m_lws_null_fail = p.lws_null_fail(); m_check_lemmas |= !(m_debug_known_solution_file_name.empty()); m_ism.set_seed(m_random_seed); @@ -4719,5 +4721,7 @@ namespace nlsat { bool solver::apply_levelwise() const { return m_imp->m_apply_lws; } unsigned solver::lws_spt_threshold() const { return m_imp->m_lws_spt_threshold; } - + + bool solver::lws_null_fail() const { return m_imp->m_lws_null_fail; } + }; diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index 566a7c09e..a5f3ea065 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -249,6 +249,7 @@ namespace nlsat { assignment& sample(); bool apply_levelwise() const; unsigned lws_spt_threshold() const; + bool lws_null_fail() const; void reset(); void collect_statistics(statistics & st); void reset_statistics(); From 91a3068f799ad8664bc3345fb349978298c8ec86 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 19 Feb 2026 07:18:10 -1000 Subject: [PATCH 15/16] disable a failure on a nullified poly in levelwise Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 21 ++------------------- src/nlsat/levelwise.h | 1 - src/nlsat/nlsat_explain.cpp | 2 -- src/nlsat/nlsat_params.pyg | 1 - src/nlsat/nlsat_solver.cpp | 1 - 5 files changed, 2 insertions(+), 24 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 5c6981004..1edd0f41a 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -57,8 +57,6 @@ namespace nlsat { unsigned m_level = 0; // current level being processed unsigned m_spanning_tree_threshold = 3; // minimum both-side count for spanning tree - bool m_null_fail = false; - bool m_fail = false; unsigned m_l_rf = UINT_MAX; // position of lower bound in m_rel.m_rfunc unsigned m_u_rf = UINT_MAX; // position of upper bound in m_rel.m_rfunc, UINT_MAX in section case @@ -264,7 +262,6 @@ namespace nlsat { m_I.emplace_back(m_pm); m_spanning_tree_threshold = m_solver.lws_spt_threshold(); - m_null_fail = m_solver.lws_null_fail(); } // Handle a polynomial whose every coefficient evaluates to zero at the sample. @@ -272,9 +269,7 @@ namespace nlsat { // 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) { - if (m_null_fail) - throw nullified_poly_exception(); - // Add all coefficients of p (w.r.t. m_level) to m_todo. + // 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); @@ -1302,7 +1297,7 @@ namespace nlsat { } } - std_vector single_cell_work() { + std_vector single_cell() { TRACE(lws, tout << "Input polynomials (" << m_P.size() << "):\n"; for (unsigned i = 0; i < m_P.size(); ++i) @@ -1350,15 +1345,6 @@ namespace nlsat { return m_I; } - std_vector single_cell() { - try { - return single_cell_work(); - } - catch (nullified_poly_exception&) { - m_fail = true; - return m_I; - } - } }; levelwise::levelwise( @@ -1376,9 +1362,6 @@ namespace nlsat { std_vector 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 diff --git a/src/nlsat/levelwise.h b/src/nlsat/levelwise.h index 27e379374..950bee641 100644 --- a/src/nlsat/levelwise.h +++ b/src/nlsat/levelwise.h @@ -46,7 +46,6 @@ namespace nlsat { levelwise(levelwise const&) = delete; levelwise& operator=(levelwise const&) = delete; std_vector single_cell(); - bool failed() const; }; // diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 3240cae2a..d5aadf683 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1048,8 +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. diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg index 9d1ed45fc..1ab305984 100644 --- a/src/nlsat/nlsat_params.pyg +++ b/src/nlsat/nlsat_params.pyg @@ -24,6 +24,5 @@ def_module_params('nlsat', ('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only"), ('lws', BOOL, True, "apply levelwise."), ('lws_spt_threshold', UINT, 2, "minimum both-side polynomial count to apply spanning tree optimization; < 2 disables spanning tree"), - ('lws_null_fail', BOOL, False, "fail levelwise projection on nullified polynomials and fall back to standard projection."), ('canonicalize', BOOL, True, "canonicalize polynomials.") )) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index eba014358..3d595b919 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -313,7 +313,6 @@ namespace nlsat { m_debug_known_solution_file_name = p.known_sat_assignment_file_name(); m_apply_lws = p.lws(); m_lws_spt_threshold = p.lws_spt_threshold(); // 0 disables spanning tree - m_lws_null_fail = p.lws_null_fail(); m_check_lemmas |= !(m_debug_known_solution_file_name.empty()); m_ism.set_seed(m_random_seed); From 23560ba8a5e217f1ac575b2f01644d345a106410 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 19 Feb 2026 09:31:30 -1000 Subject: [PATCH 16/16] cleanup regarding levelwise Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 2 - src/nlsat/nlsat_solver.cpp | 5 -- src/nlsat/nlsat_solver.h | 1 - src/test/main.cpp | 2 +- src/test/nlsat.cpp | 94 +++++++++++++++++++------------------- 5 files changed, 47 insertions(+), 57 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 1edd0f41a..7e1e97496 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -32,8 +32,6 @@ static void vec_setx(std_vector& v, unsigned idx, T val, T def) { namespace nlsat { - struct nullified_poly_exception {}; - // The three projection modes for a level: // 1. section_biggest_cell: Sample is on a root. All disc/lc added. // 2. sector_biggest_cell: Sample between roots. noLdcf optimization only. diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 3d595b919..fef3bcccf 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -251,7 +251,6 @@ namespace nlsat { bool m_apply_lws; bool m_last_conflict_used_lws = false; // Track if last conflict explanation used levelwise unsigned m_lws_spt_threshold = 3; - bool m_lws_null_fail = false; imp(solver& s, ctx& c): m_ctx(c), m_solver(s), @@ -4718,9 +4717,5 @@ namespace nlsat { return (m_imp->m_asm.mk_join(static_cast(a), static_cast(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; } - - bool solver::lws_null_fail() const { return m_imp->m_lws_null_fail; } - }; diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index a5f3ea065..566a7c09e 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -249,7 +249,6 @@ namespace nlsat { assignment& sample(); bool apply_levelwise() const; unsigned lws_spt_threshold() const; - bool lws_null_fail() const; void reset(); void collect_statistics(statistics & st); void reset_statistics(); diff --git a/src/test/main.cpp b/src/test/main.cpp index 063ef31d3..a4dabd79d 100644 --- a/src/test/main.cpp +++ b/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); diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 81d0cab9e..9709a36bf 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -496,7 +496,7 @@ static void set_assignment_value(nlsat::assignment& as, anum_manager& am, nlsat: as.set(v, tmp); } -static void tst_vandermond() { +static void tst_12() { params_ref ps; reslimit rlim; nlsat::solver s(rlim, ps, false); @@ -914,7 +914,7 @@ static void tst10() { std::cout << "\n"; } -void tst_nlsat_mv() { +void tst_13() { params_ref ps; reslimit rlim; nlsat::solver s(rlim, ps, false); @@ -923,7 +923,7 @@ void tst_nlsat_mv() { nlsat::assignment assignment(am); nlsat::explain& ex = s.get_explain(); - tst_vandermond(); + tst_12(); return; // Regression: reproduce lemma 114 where main_operator adds spurious bounds. @@ -1088,7 +1088,7 @@ x7 := 1 } -static void tst_polynomial_cache_mk_unique() { +static void tst_14() { params_ref ps; reslimit rlim; nlsat::solver s(rlim, ps, false); @@ -1134,7 +1134,7 @@ static void tst_polynomial_cache_mk_unique() { } -static void tst_nullified_polynomial() { +static void tst_15() { params_ref ps; reslimit rlim; nlsat::solver s(rlim, ps, false); @@ -1185,11 +1185,11 @@ static void tst_nullified_polynomial() { // Test case for unsound lemma lws2380 - comparing standard projection vs levelwise // The issue: x7 is unconstrained in levelwise output but affects the section polynomial -static void tst_unsound_lws2380() { +static void tst_16() { // enable_trace("nlsat_explain"); auto run_test = [](bool use_lws) { - std::cout << "=== tst_unsound_lws2380: " << (use_lws ? "Levelwise" : "Standard") << " projection (lws=" << use_lws << ") ===\n"; + std::cout << "=== tst_16: " << (use_lws ? "Levelwise" : "Standard") << " projection (lws=" << use_lws << ") ===\n"; params_ref ps; ps.set_bool("lws", use_lws); reslimit rlim; @@ -1294,8 +1294,8 @@ static void tst_unsound_lws2380() { // Test case for unsound lemma - levelwise produces cell that's too large // Input: 5 polynomials with max_var=x3, sample x0=-7, x1=-1, x2=1 // Counterexample: x0=-4, x1=-8, x2=5, x3=6 -static void tst_unsound_lws_x3() { - std::cout << "=== tst_unsound_lws_x3 ===\n"; +static void tst_17() { + std::cout << "=== tst_17 ===\n"; params_ref ps; ps.set_bool("lws", true); reslimit rlim; @@ -1391,7 +1391,7 @@ static void tst_unsound_lws_x3() { // Counterexample must be OUTSIDE the cell ENSURE(!is_point_inside_cell(am, pm, cell, counter_as)); - std::cout << "=== END tst_unsound_lws_x3 ===\n\n"; + std::cout << "=== END tst_17 ===\n\n"; } // Test case for unsound lemma from From_T2__n-46.t2__p4432_terminationG_0.smt2 @@ -1415,8 +1415,8 @@ static void tst_unsound_lws_x3() { // !(2 x2 x6^2 + x0 x5 x6 + 2 x2 x4 x6 + x2 x3 x6 - x0 x6 - x0 x4 < 0) or // x7 < root[1](x2 x6^2 x7 + ... + 2 x6 + 2 x4) or // !(x7 < root[1](x2 x6 x7 - 2)) -static void tst_unsound_lws_n46() { - std::cout << "=== tst_unsound_lws_n46 ===\n"; +static void tst_18() { + std::cout << "=== tst_18 ===\n"; params_ref ps; ps.set_bool("lws", true); @@ -1521,7 +1521,7 @@ static void tst_unsound_lws_n46() { // Counterexample must be OUTSIDE the cell ENSURE(!is_point_inside_cell(am, pm, cell, counter_as)); - std::cout << "=== END tst_unsound_lws_n46 ===\n\n"; + std::cout << "=== END tst_18 ===\n\n"; } // Test case for unsound lemma from From_AProVE_2014__Et4-rec.jar-obl-8__p28996_terminationG_0.smt2 @@ -1532,8 +1532,8 @@ static void tst_unsound_lws_n46() { // p[1]: 2 x0 x4^2 + 2 x3 x4 - x0 x4 - 2 x3 // p[2]: 2 x0 x4^2 x5 + 2 x3 x4 x5 - x0 x4 x5 - 2 x3 x5 + 4 x3 x4^2 + 9 x0 x3 x4 - 26 x3 x4 - 3 x0 x4 // p[3]: x5 - 9 -static void tst_unsound_lws_et4() { - std::cout << "=== tst_unsound_lws_et4 ===\n"; +static void tst_19() { + std::cout << "=== tst_19 ===\n"; params_ref ps; ps.set_bool("lws", true); reslimit rlim; @@ -1632,7 +1632,7 @@ static void tst_unsound_lws_et4() { // Counterexample must be OUTSIDE the cell ENSURE(!is_point_inside_cell(am, pm, cell, counter_as)); - std::cout << "=== END tst_unsound_lws_et4 ===\n\n"; + std::cout << "=== END tst_19 ===\n\n"; } // Test case for unsound lemma with disc=0 at sample for same_boundary_poly sector case @@ -1642,8 +1642,8 @@ static void tst_unsound_lws_et4() { // p[2]: x3 // Sample: x0=1, x1=1, x2=1 // Counterexample: x1=12, x2=16, x3=0 -static void tst_unsound_lws_disc_zero() { - std::cout << "=== tst_unsound_lws_disc_zero ===\n"; +static void tst_20() { + std::cout << "=== tst_20 ===\n"; params_ref ps; ps.set_bool("lws", true); @@ -1816,13 +1816,13 @@ static void tst_unsound_lws_disc_zero() { std::cout << "\nPoly signs match - cell is trivially sound.\n"; } - std::cout << "\n=== END tst_unsound_lws_disc_zero ===\n\n"; + std::cout << "\n=== END tst_20 ===\n\n"; } // Test case for unsound lemma from ppblockterm.t2__p7867_terminationG_0.smt2 // Issue z3-76w: levelwise produces unsound cell -static void tst_unsound_lws_ppblockterm() { - std::cout << "=== tst_unsound_lws_ppblockterm ===\n"; +static void tst_21() { + std::cout << "=== tst_21 ===\n"; params_ref ps; ps.set_bool("lws", true); reslimit rlim; @@ -1975,7 +1975,7 @@ static void tst_unsound_lws_ppblockterm() { std::cout << "SUCCESS: Counterexample is OUTSIDE the cell (cell is sound)\n"; } - std::cout << "=== END tst_unsound_lws_ppblockterm ===\n\n"; + std::cout << "=== END tst_21 ===\n\n"; } // Test case for gh-8397: unsound lemma with lws=false @@ -1986,7 +1986,7 @@ static void tst_unsound_lws_ppblockterm() { // 4 x6^3 + 4 x5 x6^2 - 4 x1 x6^2 + 4 x6^2 - 4 x1 x5 x6 - 4 x1 x6 < 0 or // x6 - x1 = 0 or x6 > 0 // Counterexample: x1 = 0, x5 = 0, x6 = -0.5 -static void tst_unsound_gh8397() { +static void tst_22() { // Reproduce exact unsound lemma from gh-8397 // Unsound lemma: !(1024 x1 = 0) or !(x1 + 1 > 0) or !(2048 x1^2 + 4096 x1 = 0) or // !(x1 = root[3](1024 x1^3 + 6144 x1^2 + 6144 x1)) or @@ -1994,7 +1994,7 @@ static void tst_unsound_gh8397() { // 4 x6^3 + 4 x5 x6^2 - 4 x1 x6^2 + 4 x6^2 - 4 x1 x5 x6 - 4 x1 x6 < 0 or x6 - x1 = 0 or x6 > 0 // Counterexample: x1=0, x5=0, x6=-0.5 makes ALL literals FALSE // Sample point: x0=-1, x1=0, x2=0, x3=-1, x4=0, x5=-1 (x6 is conflict var) - std::cout << "=== tst_unsound_gh8397 ===\n"; + std::cout << "=== tst_22 ===\n"; auto run_test = [](bool use_lws) { std::cout << "\n--- Running with lws=" << (use_lws ? "true" : "false") << " ---\n"; @@ -2154,7 +2154,7 @@ static void tst_unsound_gh8397() { run_test(false); // lws=false (buggy) run_test(true); // lws=true (should be correct) - std::cout << "\n=== END tst_unsound_gh8397 ===\n\n"; + std::cout << "\n=== END tst_22 ===\n\n"; } @@ -2165,8 +2165,8 @@ static void tst_unsound_gh8397() { // p[2]: - 2 x2 x6^2 + 2 x3 x5 x6 - 2 x2 x5 x6 + x4 x5^3 + 2 x3 x5^2 // Sample: x0=4, x1=1, x2=1, x3=5/2, x4=0, x5=1 // Counterexample: x2=4, x3=-3, x4=0, x5=1, x6=-1 -static void tst_unsound_lws_nullified() { - std::cout << "=== tst_unsound_lws_nullified ===\n"; +static void tst_23() { + std::cout << "=== tst_23 ===\n"; params_ref ps; ps.set_bool("lws", true); @@ -2236,9 +2236,8 @@ static void tst_unsound_lws_nullified() { bool inside = is_point_inside_cell(am, pm, cell, counter_as); // The counterexample should be OUTSIDE the cell for soundness. - // This ENSURE will fail, demonstrating the bug. ENSURE(!inside); - std::cout << "=== END tst_unsound_lws_nullified ===\n\n"; + std::cout << "=== END tst_23 ===\n\n"; } // Test case for unsound lemma - nullified polynomial with x4=3/4 @@ -2250,8 +2249,8 @@ static void tst_unsound_lws_nullified() { // p[4]: x2 x5 x6 - x0 x1 x5 - x0 x5 + x0 x2 x4 // Sample: x0=1, x1=0, x2=-1, x3=0, x4=3/4, x5=1 // Counterexample: x0=1, x1=-1, x2=-1, x3=2, x4=1, x5=1, x6=-2 -static void tst_unsound_lws_nullified2() { - std::cout << "=== tst_unsound_lws_nullified2 ===\n"; +static void tst_24() { + std::cout << "=== tst_24 ===\n"; params_ref ps; ps.set_bool("lws", true); @@ -2330,15 +2329,14 @@ static void tst_unsound_lws_nullified2() { bool inside = is_point_inside_cell(am, pm, cell, counter_as); // The counterexample should be OUTSIDE the cell for soundness. - // This ENSURE will fail, demonstrating the bug. ENSURE(!inside); - std::cout << "=== END tst_unsound_lws_nullified2 ===\n\n"; + std::cout << "=== END tst_24 ===\n\n"; } // Test that compute_conflict_explanation produces a lemma where the counterexample // falsifies at least one literal. Reproducer from p6236_terminationG_0.smt2. -static void tst_explain_p6236() { - std::cout << "=== tst_explain_p6236 ===\n"; +static void tst_25() { + std::cout << "=== tst_25 ===\n"; params_ref ps; ps.set_bool("lws", true); @@ -2478,33 +2476,33 @@ static void tst_explain_p6236() { s.dec_ref(root_lt_bvar); s.dec_ref(gt_lit); - std::cout << "=== END tst_explain_p6236 ===\n\n"; + std::cout << "=== END tst_25 ===\n\n"; } void tst_nlsat() { - tst_unsound_gh8397(); + tst_22(); std::cout << "------------------\n"; - tst_explain_p6236(); + tst_25(); std::cout << "------------------\n"; - tst_unsound_lws_disc_zero(); + tst_20(); std::cout << "------------------\n"; - tst_unsound_lws_nullified2(); + tst_24(); std::cout << "------------------\n"; - tst_unsound_lws_nullified(); + tst_23(); std::cout << "------------------\n"; - tst_unsound_lws_ppblockterm(); + tst_21(); std::cout << "------------------\n"; - tst_unsound_lws_n46(); + tst_18(); std::cout << "------------------\n"; - tst_unsound_lws_et4(); + tst_19(); std::cout << "------------------\n"; - tst_unsound_lws_x3(); + tst_17(); std::cout << "------------------\n"; - tst_unsound_lws2380(); + tst_16(); std::cout << "------------------\n"; - tst_polynomial_cache_mk_unique(); + tst_14(); std::cout << "------------------\n"; - tst_nullified_polynomial(); + tst_15(); std::cout << "------------------\n"; tst11(); std::cout << "------------------\n";