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

Merge branch 'Z3Prover:master' into master

Browse source
This commit is contained in:
davedets 2026-08-08 16:14:54 -07:00 • committed by GitHub
commit f805b557d2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 76 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -244,15 +244,19 @@ namespace nla {
return false;
lpvar w, fixed_to_zero;
if (!is_linear(m, w, fixed_to_zero))
if (!is_linear(m, w, fixed_to_zero))
return false;
c().emons().set_propagated(m);
return linearize(m, w, fixed_to_zero);
}
bool monomial_bounds::linearize(monic const& m, lpvar w, lpvar fixed_to_zero) {
bool propagated = false;
if (fixed_to_zero != null_lpvar) {
propagated = propagate_fixed_to_zero(m, fixed_to_zero);
}
}
else {
rational k = fixed_var_product(m, w);
if (w == null_lpvar)
@ -265,6 +269,69 @@ namespace nla {
return propagated;
}
/**
\brief Linearize the violated monomials that have at most one non-fixed
factor, ignoring the is_propagated latch.
propagate_linear_bound sees a linear monomial once: it records the
defining relation and retires the monomial via set_propagated. When that
relation happens to be satisfied by the model of the moment,
propagate_nonfixed skips adding the defining row, so the relation is
recorded nowhere; as soon as the model moves, the monomial is violated
again and the only handles left are a case split (refine_pseudo_linear)
or a horner/grobner round per final check.
This pass runs from core::propagate(), which theory_lra invokes on entry
to every final check, so the repaired LP is re-solved and the surviving
violations still get their regular horner/grobner round. Only monomials
the current model violates are linearized: the guards of propagate_fixed
/ propagate_nonfixed cannot dismiss such a row as redundant, and every
row added repairs an actual violation. Recording the row unconditionally
instead (even when the model satisfies it) was measured to lose over 500
QF_NIA instances: there factors are fixed by branching, and the rows,
re-added on every branch, grow the tableau for no benefit. Restricting
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;
for (auto const& m : c().emons()) {
if (c().check_monic(m))
continue;
lpvar w, fixed_to_zero;
if (!is_linear(m, w, fixed_to_zero))
continue;
// The pass pays off when the factors are fixed for good (bound
// propagation from structural facts, e.g. pow2 constants in F*
// queries): the same defining row then repairs the violation for
// the rest of the search. When the factors are fixed by branching
// instead, each branch re-fixes them to another small value, and
// the rows, popped by the next backjump, only perturb the search
// (installing m = 3*w rows at deep decision levels was measured to
// turn a 0.1s F* query into a timeout). A small fixed-factor
// product is the signature of enumeration, so the row-installing
// path is reserved for products too wide to be branch-enumerated.
// The row-free paths (m fixed to a constant) are plain bound
// updates and stay ungated.
if (fixed_to_zero == null_lpvar && w != null_lpvar) {
rational k = fixed_var_product(m, w);
if (k.is_int() && k.bitsize() <= 16)
continue;
}
if (linearize(m, w, fixed_to_zero)) {
propagated = true;
TRACE(nla_solver, tout << "linearized violated monomial " << m
<< ", scope " << c().lra.get_scope_level() << "\n";);
}
if (c().lra.get_status() == lp::lp_status::INFEASIBLE)
break;
}
return propagated;
}
lp::explanation monomial_bounds::get_explanation(u_dependency* dep) {
lp::explanation exp;
svector<lp::constraint_index> cs;

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

@ -50,9 +50,11 @@ namespace nla {
// when all but one variable of a monomial are fixed, the monomial is
// linear and its value/equality can be propagated into the LP solver.
bool propagate_linear_bound(monic & m);
bool linearize(monic const& m, lpvar w, lpvar fixed_to_zero);
bool is_linear(monic const& m, lpvar& w, lpvar & fixed_to_zero);
rational fixed_var_product(monic const& m, lpvar w);
// ----------------------------------------------------------------
// max_min: incremental LP bound optimization.
//
@ -91,6 +93,7 @@ namespace nla {
bool tighten_lp_bounds();
bool propagate_linear_bounds();
bool propagate_changed_bounds();
bool propagate_violated_linear_monomials();
bool propagate_fixed_rows();
bool optimize_nl_bounds();

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

@ -1538,7 +1538,9 @@ bool core::propagate() {
propagated = true;
if (m_monomial_bounds.tighten_lp_bounds())
propagated = true;
if (m_monomial_bounds.propagate_changed_bounds())
if (m_monomial_bounds.propagate_changed_bounds())
propagated = true;
if (m_monomial_bounds.propagate_violated_linear_monomials())
propagated = true;
m_monics_with_changed_bounds.reset();
if (propagated)

1
src/params/smt_params_helper.pyg
View file

@ -100,6 +100,7 @@ def_module_params(module_name='smt',
('arith.nl.reduce_pseudo_linear', BOOL, True, 'create incremental linearization axioms for pseudo-linear monomials'),
('arith.nl.delay', UINT, 10, 'number of calls to final check before invoking bounded nlsat check'),
('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'),
('arith.nl.linearize_violated_monomials', BOOL, True, 'in final check, install the defining row m = k*w for violated monomials with at most one non-fixed factor before resorting to case splits and horner/grobner'),
('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'),
('arith.nl.propagate_fixed_rows', BOOL, False, 'scan LP rows for fixed variables'),
('arith.nl.optimize_bounds_lp_max_vars', UINT, 120, 'skip LP-based nonlinear bounds optimization when the number of candidate monomial variables exceeds this threshold (0 = unlimited)'),