mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-27 09:22:41 +00:00
Code Activity

opt: preserve strict-inequality (infinitesimal) optima in maximize_objective

Browse source 
Box/lex optimization over an open interval (e.g. minimize/maximize a Real
x under `x > 16/5 && x < 127/10`) regressed to reporting arbitrary feasible
interior points (37/10, 117/10) instead of the true infimum/supremum with
infinitesimals (16/5 + epsilon, 127/10 - epsilon).

Root cause: commit fdc32d0e6 (#10028/#10040) stopped committing the
arithmetic optimization hint `val` unless it is re-validated by
check_bound(). That fix is correct for objectives that share symbols with
other theories, where the LP hint can over-estimate an unachievable
optimum. But check_bound() cannot validate a strict/open optimum: such a
value carries a non-zero infinitesimal, and mk_ge() drops the infinitesimal
when building the bound literal (it is not expressible as an arithmetic
atom). So `x >= c - epsilon` becomes the strictly stronger `x >= c`, which
is unsatisfiable together with the original `x < c`; the check fails and the
correct optimum is discarded in favour of an interior model point.

Fix: in check_bound(), trust `val` when it has a non-zero infinitesimal --
it is the exact optimum of the arithmetic relaxation and cannot be
re-validated by re-asserting a (necessarily weaker) rational bound. The
zero-infinitesimal path (integer/rational objectives, including the #10028
shared-symbol case) is unchanged.

Validated by rebuilding z3 and re-running the benchmark: output now matches
the recorded oracle. Closed-interval, integer-strict, unbounded, and lex
cases were also checked and the #10028 distinct-minimize case remains
consistent.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-07-05 00:41:18 -07:00 • committed by GitHub
parent 557a0cadab
commit 28e9610a1f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 15 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/opt/opt_solver.cpp
View file

@ -361,6 +361,21 @@ namespace opt {
//
auto check_bound = [&]() {
SASSERT(has_shared);
//
// A strict (open) optimum is represented with a non-zero
// infinitesimal, e.g. the supremum of 'x' subject to 'x < c' is
// 'c - epsilon'. Such a bound cannot be re-validated here:
// mk_ge() drops the infinitesimal when constructing the bound
// literal (an infinitesimal is not expressible as an arithmetic
// atom), so 'x >= c - epsilon' is turned into the strictly
// stronger 'x >= c', which is unsatisfiable together with the
// original 'x < c' and makes this check spuriously fail. The
// infinitesimal value is the exact optimum of the arithmetic
// relaxation, so trust it rather than discarding it in favour of
// an arbitrary interior model point.
//
if (!val.get_infinitesimal().is_zero())
return true;
return bound_value(i, val) && l_true == m_context.check(0, nullptr);
};