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";