mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 16:27:37 +00:00
Code Activity

remove an obsolete m_fail and related from levelwise

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-02-17 14:11:16 -10:00
parent 2d8e866e19
commit a781f9c0a0
4 changed files with 18 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/nlsat/levelwise.cpp
View file

@ -65,7 +65,6 @@ namespace nlsat {
std_vector<bool> m_poly_has_roots;
polynomial_ref_vector m_psc_tmp; // scratch for PSC chains
bool m_fail = false;
// Vectors indexed by position in m_level_ps (more cache-friendly than maps)
mutable std_vector<uint8_t> m_side_mask; // bit0 = lower, bit1 = upper, 3 = both
@ -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

1
src/nlsat/levelwise.h
View file

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

3
src/nlsat/nlsat_explain.cpp
View file

@ -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.

46
src/test/nlsat.cpp
View file

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