mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-25 11:34:01 +00:00
Code Activity

Restrict noDisc optimization to section_lowest_degree only

Browse source 
Match SMT-RAT behavior: noDisc (discriminant omission for leaves
connected only to section polynomial) is only applied for
sectionHeuristic == 3 (lowest_degree), not for biggest_cell or chain.

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
This commit is contained in:
Lev Nachmanson 2026-01-16 10:50:26 -10:00
parent e0be8a8f8d
commit 9d22786649
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/nlsat/levelwise.cpp
View file

@ -1120,7 +1120,9 @@ namespace nlsat {
std_vector<bool> omit_lc;
compute_omit_lc_section(level, level_ps, omit_lc);
std_vector<bool> omit_disc;
compute_omit_disc_from_section_relation(level, level_ps, omit_disc);
// SMT-RAT only applies noDisc optimization for section_lowest_degree (heuristic 3)
if (m_section_relation_mode == section_lowest_degree)
compute_omit_disc_from_section_relation(level, level_ps, omit_disc);
for (unsigned i = 0; i < level_ps.size(); ++i) {
polynomial_ref p(level_ps.get(i), m_pm);