mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-08 06:52:26 +00:00
Code Activity

move optimize_nl_bounds to monomial_bounds

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-08-06 22:19:59 -07:00
parent 2c508b3753
commit af10b18f4d
5 changed files with 96 additions and 98 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -109,7 +109,7 @@ bool horner::horner_lemmas() {
// exclude zero and expose conflicts. Done here (instead of core::propagate)
// so the LP maximization only runs when horner is actually scheduled.
// optimize_nl_bounds() checks arith.nl.optimize_bounds internally.
c().optimize_nl_bounds();
c().m_monomial_bounds.optimize_nl_bounds();
// optimize_nl_bounds re-calibrated m_to_refine against the model it produced.
// If nothing remains to refine, every monomial is consistent under a feasible
// LP model: the nonlinear goal is satisfied. Declare it and stop.
@ -145,4 +145,3 @@ bool horner::horner_lemmas() {
return conflict;
}
}

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

@ -1123,4 +1123,97 @@ namespace nla {
return dep;
}
/**
\brief Tighten the bounds of variables occurring in nonlinear monomials by
maximizing/minimizing them over the LP tableau (analogous to theory_arith's
max_min_nl_vars). The tighter implied bounds, each carrying an LP explanation,
let the subsequent horner/cross-nested interval evaluation exclude zero and
detect a conflict that would otherwise be missed with only the propagated
bounds.
*/
bool monomial_bounds::optimize_nl_bounds() {
if (!c().params().arith_nl_optimize_bounds() || !m_bounds_optimization_enabled)
return false;
c().trail().push(value_trail(m_bounds_optimization_enabled));
m_bounds_optimization_enabled = false;
auto& lra = c().lra;
if (!lra.is_feasible())
return false;
if (lra.find_feasible_solution() == lp::lp_status::INFEASIBLE) {
// find_feasible_solution moved the model; keep m_to_refine in sync.
c().init_to_refine();
return false;
}
// Gather the candidate columns: every non-fixed leaf variable that
// participates in a monomial (mirrors solver=2's max_min_nl_vars).
svector<lpvar> cands;
auto add = [&](lpvar j) {
if (c().active_var_set_contains(j))
return;
c().insert_to_active_var_set(j);
if (lra.column_is_fixed(j))
return;
cands.push_back(j);
};
c().clear_active_var_set();
for (auto const& m : c().emons()) {
add(m.var());
for (lpvar k : m.vars())
add(k);
}
// Throttle: the LP maximize/minimize cost scales with the number of
// candidate variables (two LP optimizations each). On large nonlinear
// problems this pass is expensive and rarely productive, so skip it when the
// candidate set exceeds the threshold (0 = unlimited).
unsigned const max_vars = c().params().arith_nl_optimize_bounds_lp_max_vars();
if (max_vars != 0 && cands.size() > max_vars) {
// find_feasible_solution() above already moved the model, so m_to_refine
// is stale on this path too and has to be re-calibrated before returning.
c().init_to_refine();
return false;
}
// Collect improved bounds first (each improve_bound maximizes a term
// over the *unchanged* constraint set, so all improvements are valid implied
// bounds), then apply them together and re-establish feasibility once.
// Interleaving update_column_type_and_bound between the maximize calls
// corrupts the core solver's x/inf_heap (maximize_term_on_tableau issues a
// raw solve() that does not reconcile pending bound changes).
struct improved_bound { lpvar j; lp::lconstraint_kind kind; rational bound; u_dependency* dep; };
vector<improved_bound> improvements;
for (lpvar j : cands) {
if (!lra.is_feasible())
break;
for (bool is_lower : { true, false }) {
rational bound;
u_dependency* dep = improve_bound(j, is_lower, bound);
if (!dep)
continue;
auto kind = is_lower ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LE;
improvements.push_back({ j, kind, bound, dep });
}
}
if (improvements.empty()) {
// The exploratory simplex walk in improve_bound/mm_optimize mutated the
// LP model even though no bound was tightened. Restore a clean feasible
// model and re-calibrate m_to_refine so downstream lemma passes (grobner,
// basic_lemma) never see a stale monomial that is now consistent.
lra.find_feasible_solution();
c().init_to_refine();
return false;
}
for (auto const& ib : improvements)
lra.update_column_type_and_bound(ib.j, ib.kind, ib.bound, ib.dep);
lra.find_feasible_solution();
// The model changed: re-calibrate m_to_refine against the new assignment.
c().init_to_refine();
return true;
}
}

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

@ -16,6 +16,7 @@ namespace nla {
class core;
class monomial_bounds : common {
dep_intervals& dep;
bool m_bounds_optimization_enabled = true;
bool tighten_lp_bound(dep_interval const &range, lpvar v, unsigned p);
bool tighten_lp_upper_bound(dep_interval const& range, lpvar v, unsigned p);
@ -91,6 +92,7 @@ namespace nla {
bool propagate_linear_bounds();
bool propagate_changed_bounds();
bool propagate_fixed_rows();
bool optimize_nl_bounds();
// Maximize (is_lower == false) or minimize (is_lower == true) column j
// over the LP tableau and, if the resulting bound improves j's current

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

@ -1564,99 +1564,6 @@ bool core::incremental_propagate() {
return propagated;
}
/**
\brief Tighten the bounds of variables occurring in nonlinear monomials by
maximizing/minimizing them over the LP tableau (analogous to theory_arith's
max_min_nl_vars). The tighter implied bounds, each carrying an LP explanation,
let the subsequent horner/cross-nested interval evaluation exclude zero and
detect a conflict that would otherwise be missed with only the propagated
bounds.
*/
bool core::optimize_nl_bounds() {
if (!params().arith_nl_optimize_bounds() || !m_bounds_optimization_enabled)
return false;
trail().push(value_trail(m_bounds_optimization_enabled));
m_bounds_optimization_enabled = false;
if (!lra.is_feasible())
return false;
if (lra.find_feasible_solution() == lp::lp_status::INFEASIBLE) {
// find_feasible_solution moved the model; keep m_to_refine in sync.
init_to_refine();
return false;
}
// Gather the candidate columns: every non-fixed leaf variable that
// participates in a monomial (mirrors solver=2's max_min_nl_vars).
svector<lpvar> cands;
auto add = [&](lpvar j) {
if (active_var_set_contains(j))
return;
insert_to_active_var_set(j);
if (lra.column_is_fixed(j))
return;
cands.push_back(j);
};
clear_active_var_set();
for (auto const& m : m_emons) {
add(m.var());
for (lpvar k : m.vars())
add(k);
}
// Throttle: the LP maximize/minimize cost scales with the number of
// candidate variables (two LP optimizations each). On large nonlinear
// problems this pass is expensive and rarely productive, so skip it when the
// candidate set exceeds the threshold (0 = unlimited).
unsigned const max_vars = params().arith_nl_optimize_bounds_lp_max_vars();
if (max_vars != 0 && cands.size() > max_vars) {
// find_feasible_solution() above already moved the model, so m_to_refine
// is stale on this path too and has to be re-calibrated before returning.
init_to_refine();
return false;
}
// Collect improved bounds first (each find_improved_bound maximizes a term
// over the *unchanged* constraint set, so all improvements are valid implied
// bounds), then apply them together and re-establish feasibility once.
// Interleaving update_column_type_and_bound between the maximize calls
// corrupts the core solver's x/inf_heap (maximize_term_on_tableau issues a
// raw solve() that does not reconcile pending bound changes).
struct improved_bound { lpvar j; lp::lconstraint_kind kind; rational bound; u_dependency* dep; };
vector<improved_bound> improvements;
for (lpvar j : cands) {
if (!lra.is_feasible())
break;
for (bool is_lower : { true, false }) {
rational bound;
u_dependency* dep = m_monomial_bounds.improve_bound(j, is_lower, bound);
if (!dep)
continue;
auto kind = is_lower ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LE;
improvements.push_back({ j, kind, bound, dep });
}
}
if (improvements.empty()) {
// The exploratory simplex walk in improve_bound/mm_optimize mutated the
// LP model even though no bound was tightened. Restore a clean feasible
// model and re-calibrate m_to_refine so downstream lemma passes (grobner,
// basic_lemma) never see a stale monomial that is now consistent.
lra.find_feasible_solution();
init_to_refine();
return false;
}
for (auto const& ib : improvements)
lra.update_column_type_and_bound(ib.j, ib.kind, ib.bound, ib.dep);
lra.find_feasible_solution();
// The model changed: re-calibrate m_to_refine against the new assignment.
init_to_refine();
return true;
}
void core::simplify() {
// in-processing simplifiation can go here, such as bounds improvements.
}

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

@ -111,7 +111,6 @@ class core {
nla_throttle m_throttle;
bool m_throttle_enabled = true;
bool m_bounds_optimization_enabled = true;
@ -122,8 +121,6 @@ class core {
bool is_pseudo_linear(monic const& m) const;
void refine_pseudo_linear(monic const& m);
bool optimize_nl_bounds();
std::ostream& display_constraint_smt(std::ostream& out, unsigned id, lp::lar_base_constraint const& c) const;
std::ostream& display_declarations_smt(std::ostream& out) const;