mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-01 06:37:49 +00:00
Code Activity

bug fixes

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-01-25 19:21:06 -10:00
parent e84844a873
commit 6595c72f30
1 changed files with 17 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/nlsat/levelwise.cpp
View file

@ -1501,6 +1501,7 @@ namespace nlsat {
if (add_lc && witness && !is_const(witness)) if (add_lc && witness && !is_const(witness))
if (lc && !is_zero(lc) && m_am.eval_sign_at(lc, sample()) != 0) if (lc && !is_zero(lc) && m_am.eval_sign_at(lc, sample()) != 0)
witness = polynomial_ref(m_pm); witness = polynomial_ref(m_pm);
add_projections_for(p, m_level, witness, add_lc, true); //true for adding the discriminant: always add it in sector, required by Lemma 3.2. add_projections_for(p, m_level, witness, add_lc, true); //true for adding the discriminant: always add it in sector, required by Lemma 3.2.
} }
} }
@ -1532,10 +1533,9 @@ namespace nlsat {
// add_lc stays true // add_lc stays true
} }
else if (m_section_relation_mode == section_biggest_cell) { else if (m_section_relation_mode == section_biggest_cell) {
// SMT-RAT section heuristic 1 projects leading coefficients primarily for the // SMT-RAT section heuristic 1 does NOT use noLdcf optimization.
// defining section polynomial; keep LCs only for upstream ORD polynomials. // All polynomials with roots get their LC projected.
if (get_req(i) != inv_req::ord) // add_lc stays true
add_lc = false;
} }
else { else {
if (add_lc && i < m_omit_lc.size() && m_omit_lc[i]) if (add_lc && i < m_omit_lc.size() && m_omit_lc[i])
@ -1595,13 +1595,24 @@ namespace nlsat {
return false; return false;
} }
// Clear all per-level state that could be stale from previous levels.
// This ensures no leftover heuristic decisions affect the current level.
void clear_level_state() {
m_omit_lc.clear();
m_omit_disc.clear();
m_rel.m_pairs.clear();
m_side_mask.clear();
m_deg_in_order_graph.clear();
m_unique_neighbor.clear();
}
void process_level_section(bool have_interval) { void process_level_section(bool have_interval) {
SASSERT(m_I[m_level].section); SASSERT(m_I[m_level].section);
m_solver.record_levelwise_section(); m_solver.record_levelwise_section();
clear_level_state(); // Clear stale state from previous level
if (have_interval) { if (have_interval) {
// Check spanning tree threshold first, independent of dynamic heuristic // Check spanning tree threshold first, independent of dynamic heuristic
if (should_use_spanning_tree()) { if (should_use_spanning_tree()) {
m_rel.m_pairs.clear();
fill_relation_pairs_for_section_spanning_tree(); fill_relation_pairs_for_section_spanning_tree();
compute_omit_lc_both_sides(true); compute_omit_lc_both_sides(true);
m_section_relation_mode = section_spanning_tree; m_section_relation_mode = section_spanning_tree;
@ -1621,10 +1632,10 @@ namespace nlsat {
void process_level_sector(bool have_interval) { void process_level_sector(bool have_interval) {
SASSERT(!m_I[m_level].section); SASSERT(!m_I[m_level].section);
m_solver.record_levelwise_sector(); m_solver.record_levelwise_sector();
clear_level_state(); // Clear stale state from previous level
if (have_interval) { if (have_interval) {
// Check spanning tree threshold first, independent of dynamic heuristic // Check spanning tree threshold first, independent of dynamic heuristic
if (should_use_spanning_tree()) { if (should_use_spanning_tree()) {
m_rel.m_pairs.clear();
fill_relation_with_spanning_tree_heuristic(); fill_relation_with_spanning_tree_heuristic();
compute_omit_lc_both_sides(true); compute_omit_lc_both_sides(true);
m_sector_relation_mode = spanning_tree; m_sector_relation_mode = spanning_tree;