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

disable a failure on a nullified poly in levelwise

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-02-19 07:18:10 -10:00
parent 1e985ea96e
commit 91a3068f79
5 changed files with 2 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/nlsat/levelwise.cpp
View file

@ -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<root_function_interval> single_cell_work() {
std_vector<root_function_interval> 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<root_function_interval> 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::root_function_interval> 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

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;
};
//

2
src/nlsat/nlsat_explain.cpp
View file

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

1
src/nlsat/nlsat_params.pyg
View file

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

1
src/nlsat/nlsat_solver.cpp
View file

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