diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 340d397d7..85421195c 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -554,52 +554,6 @@ namespace nlsat { } } - // Compute noDisc for same_boundary_poly case (sector with same lower/upper poly). - // When lower and upper bounds come from the same polynomial t, non-bound polynomials - // can omit their discriminant IF they don't vanish at sample AND their discriminant - // is non-zero at sample. - // - // Theory: If poly p doesn't vanish at sample, all its roots are on one side of the sample. - // Sign(p at sample) = sign(LC) * (-1)^(#roots below). If roots coincide (disc=0), - // two roots merge/disappear, parity changes by 2, sign unchanged. So disc not needed. - // - // However, if disc(p) = 0 at sample, p has a multiple root that can SPLIT when parameters - // change. When a double root splits, it creates two distinct roots, potentially one on - // each side of the sample, causing a sign change. So we must keep disc when disc=0. - // - // Example: p = (x-1)^2 at sample has disc=0. If it splits to (x-1)(x-9), the sample - // at x=5 has different sign than before. - void compute_omit_disc_for_same_boundary() { - m_omit_disc.clear(); - m_omit_disc.resize(m_level_ps.size(), false); - if (!same_boundary_poly()) - return; - - unsigned bound_idx = lower_bound_idx(); - - for (unsigned i = 0; i < m_level_ps.size(); ++i) { - // Skip boundary polynomial - if (i == bound_idx) - continue; - // Only skip if poly is not ORD-required - if (get_req(i) == inv_req::ord) - continue; - // Only skip if poly has roots (rootless needs disc to stay rootless) - if (!poly_has_roots(i)) - continue; - poly* p = m_level_ps.get(i); - polynomial_ref p_ref(p, m_pm); - // Keep disc if poly vanishes at sample (root coincides with boundary) - if (m_am.eval_sign_at(p_ref, sample()) == 0) - continue; - // Keep disc if discriminant is zero at sample (multiple root can split) - polynomial_ref disc = psc_discriminant(p_ref, m_level); - if (disc && !is_const(disc) && m_am.eval_sign_at(disc, sample()) == 0) - continue; - m_omit_disc[i] = true; - } - } - // ---------------------------------------------------------------------------- // noLdcf heuristic helpers // ---------------------------------------------------------------------------- @@ -1263,16 +1217,8 @@ namespace nlsat { fill_relation_sector_spanning_tree(); compute_omit_disc_for_spanning_tree(); m_rel_mode = spanning_tree; - } else { - fill_relation_sector_biggest_cell(); - // For same_boundary_poly, compute disc omission - if (same_boundary_poly()) - compute_omit_disc_for_same_boundary(); - // TODO: Could also drop discriminants for single-side leaves in biggest_cell mode. - // A leaf p with all roots on one side (e.g., below lb) has sign at sample determined - // solely by being above/below all roots - internal root ordering doesn't matter. - // SMT-RAT doesn't implement this, but it should be theoretically sound. - } + } else + fill_relation_sector_biggest_cell(); compute_omit_lc_both_sides(m_rel_mode == spanning_tree); SASSERT(relation_invariant()); diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 1660c9cfb..b27781687 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -1880,7 +1880,190 @@ static void tst_unsound_lws_et4() { std::cout << "=== END tst_unsound_lws_et4 ===\n\n"; } +// Test case for unsound lemma with disc=0 at sample for same_boundary_poly sector case +// Polynomials: +// p[0]: - x2^3 + x1^3 x2 - x1^4 +// p[1]: - x2^3 x3 + x1^3 x2 x3 - x1^4 x3 - x2^3 + x1^3 x2^2 + 4 x1^4 x2 - x1^3 x2 - x1^5 - x1^4 +// 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"; + + 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 4 variables x0-x3 + 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); + + polynomial_ref _x0(pm), _x1(pm), _x2(pm), _x3(pm); + _x0 = pm.mk_polynomial(x0); + _x1 = pm.mk_polynomial(x1); + _x2 = pm.mk_polynomial(x2); + _x3 = pm.mk_polynomial(x3); + (void)_x0; // unused + + // p[0]: - x2^3 + x1^3 x2 - x1^4 + polynomial_ref p0(pm); + p0 = -(_x2^3) + (_x1^3) * _x2 - (_x1^4); + + // p[1]: - x2^3 x3 + x1^3 x2 x3 - x1^4 x3 - x2^3 + x1^3 x2^2 + 4 x1^4 x2 - x1^3 x2 - x1^5 - x1^4 + polynomial_ref p1(pm); + p1 = -(_x2^3) * _x3 + (_x1^3) * _x2 * _x3 - (_x1^4) * _x3 + - (_x2^3) + (_x1^3) * (_x2^2) + 4 * (_x1^4) * _x2 - (_x1^3) * _x2 - (_x1^5) - (_x1^4); + + // p[2]: x3 + polynomial_ref p2(pm); + p2 = _x3; + + std::cout << "Input polynomials:\n"; + std::cout << " p0: " << p0 << "\n"; + std::cout << " p1: " << p1 << "\n"; + std::cout << " p2: " << p2 << "\n\n"; + + // Set sample point: x0=1, x1=1, x2=1 + scoped_anum val(am); + 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); + + std::cout << "Sample point: x0=1, x1=1, x2=1\n"; + + // Set counterexample: x1=12, x2=16, x3=0 + am.set(val, 1); counter_as.set(x0, val); + am.set(val, 12); counter_as.set(x1, val); + am.set(val, 16); counter_as.set(x2, val); + am.set(val, 0); counter_as.set(x3, val); + + std::cout << "Counterexample: x1=12, x2=16, x3=0\n\n"; + + // Set solver assignment for levelwise + 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 = x3; + + // Run levelwise + std::cout << "Running levelwise with max_x = x3...\n"; + 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 << ": "; + 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"; + + // Check sign of p0 at sample vs counterexample + std::cout << "=== Checking sign of p0 (projection poly) ===\n"; + sign p0_sample = am.eval_sign_at(p0, sample_as); + sign p0_counter = am.eval_sign_at(p0, counter_as); + std::cout << " p0 at sample (x1=1, x2=1): " << p0_sample << "\n"; + std::cout << " p0 at counter (x1=12, x2=16): " << p0_counter << "\n"; + std::cout << " Signs " << (p0_sample == p0_counter ? "match" : "DIFFER") << "\n"; + + // Check if counterexample is inside the cell at each level + // For soundness: if counter has different poly sign, it MUST be outside the cell + std::cout << "\n=== Checking if counterexample is in the cell ===\n"; + bool counter_outside = false; + + // Level 0: (-oo, +oo) - always inside + std::cout << "Level 0: (-oo, +oo) -> counter inside\n"; + + // Level 1: check if x1=12 is in the cell + { + auto const& interval = cell[1]; + if (!interval.l_inf()) { + polynomial_ref lower_p(interval.l, pm); + scoped_anum_vector lower_roots(am); + // Partial assignment for level 1 (just x0) + nlsat::assignment partial_as(am); + scoped_anum val0(am); + am.set(val0, 1); // counter x0 = 1 + partial_as.set(x0, val0); + am.isolate_roots(lower_p, nlsat::undef_var_assignment(partial_as, 1), lower_roots); + if (lower_roots.size() >= interval.l_index) { + scoped_anum counter_x1(am); + am.set(counter_x1, 12); + int cmp = am.compare(counter_x1, lower_roots[interval.l_index - 1]); + std::cout << "Level 1 lower bound: root[" << interval.l_index << "] of poly, counter x1=12 is " + << (cmp > 0 ? "ABOVE" : (cmp < 0 ? "BELOW" : "AT")) << " lower bound\n"; + if (cmp <= 0) counter_outside = true; + } + } + if (!interval.u_inf()) { + polynomial_ref upper_p(interval.u, pm); + scoped_anum_vector upper_roots(am); + // Partial assignment for level 1 (just x0) + nlsat::assignment partial_as(am); + scoped_anum val0(am); + am.set(val0, 1); // counter x0 = 1 + partial_as.set(x0, val0); + am.isolate_roots(upper_p, nlsat::undef_var_assignment(partial_as, 1), upper_roots); + if (upper_roots.size() >= interval.u_index) { + scoped_anum counter_x1(am); + am.set(counter_x1, 12); + int cmp = am.compare(counter_x1, upper_roots[interval.u_index - 1]); + std::cout << "Level 1 upper bound: root[" << interval.u_index << "] of poly, counter x1=12 is " + << (cmp > 0 ? "ABOVE" : (cmp < 0 ? "BELOW" : "AT")) << " upper bound\n"; + if (cmp >= 0) counter_outside = true; + } + } + } + + // 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 + 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"; + std::cout << "Counter is " << (counter_outside ? "OUTSIDE" : "INSIDE") << " the cell.\n"; + ENSURE(counter_outside); // Cell is sound if counter is outside + } else { + std::cout << "\nPoly signs match - cell is trivially sound.\n"; + } + + std::cout << "\n=== END tst_unsound_lws_disc_zero ===\n\n"; +} + void tst_nlsat() { + tst_unsound_lws_disc_zero(); + std::cout << "------------------\n"; tst_unsound_lws_n46(); std::cout << "------------------\n"; tst_unsound_lws_et4();