mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-24 02:49:38 +00:00
Code Activity

fix bug with skipping too many discriminants

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-01-26 12:10:24 -10:00
parent f429a57384
commit 7cfafc133f
1 changed files with 2 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/nlsat/levelwise.cpp
View file

@ -1168,8 +1168,7 @@ namespace nlsat {
poly* section_p = m_I[m_level].l.get(); poly* section_p = m_I[m_level].l.get();
compute_omit_lc_section(); compute_omit_lc_section();
// No noDisc optimization - always compute discriminants // m_omit_disc is computed by compute_omit_disc_for_spanning_tree() in process_level_section()
m_omit_disc.clear();
for (unsigned i = 0; i < m_level_ps.size(); ++i) { for (unsigned i = 0; i < m_level_ps.size(); ++i) {
polynomial_ref p(m_level_ps.get(i), m_pm); polynomial_ref p(m_level_ps.get(i), m_pm);
@ -1190,12 +1189,8 @@ namespace nlsat {
add_lc = false; add_lc = false;
} }
// Compute add_disc: biggest_cell only adds disc for section_poly and ORD polys // Compute add_disc: spanning_tree can omit disc for leaves
bool add_disc = true; bool add_disc = true;
if (!is_section_poly && m_rel_mode == biggest_cell) {
if (get_req(i) != inv_req::ord)
add_disc = false;
}
// Only omit discriminants for polynomials that were not required to be order-invariant // Only omit discriminants for polynomials that were not required to be order-invariant
// by upstream projection steps. // by upstream projection steps.
if (add_disc && get_req(i) != inv_req::ord) { if (add_disc && get_req(i) != inv_req::ord) {