mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-14 09:45:36 +00:00
Code Activity

Move nonlinear parameter check into monomial bounds

Browse source 
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-08-04 13:35:04 -07:00 • committed by Lev Nachmanson
parent 953f85e1ab
commit e7b7d85d23
2 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/monomial_bounds.cpp
View file

@ -293,6 +293,8 @@ namespace nla {
the pass to violated monomials keeps the wins without that regression.
*/
bool monomial_bounds::propagate_violated_linear_monomials() {
if (!c().params().arith_nl_linearize_violated_monomials())
return false;
if (!c().lra.is_feasible())
return false;
bool propagated = false;

3
src/math/lp/nla_core.cpp
View file

@ -1547,8 +1547,7 @@ bool core::propagate() {
propagated = true;
if (m_monomial_bounds.propagate_changed_bounds())
propagated = true;
if (params().arith_nl_linearize_violated_monomials() &&
m_monomial_bounds.propagate_violated_linear_monomials())
if (m_monomial_bounds.propagate_violated_linear_monomials())
propagated = true;
m_monics_with_changed_bounds.reset();
if (propagated)