mirror of
https://github.com/Z3Prover/z3
synced 2026-07-30 02:33:51 +00:00
4065e4688c
Maximizing/minimizing under a strict inequality (e.g. maximize r subject to r < 1) has the delta-rational optimum 1 - epsilon. Reporting it soundly requires check_bound to validate the bound r >= 1 - epsilon, i.e. to assert a LOWER bound whose value carries a NEGATIVE infinitesimal (r, -1). No lconstraint_kind can express that: the kind->epsilon map only produces the matching-sign infinitesimals (GT -> lower (r, +1), LT -> upper (r, -1)) or zero (GE/LE). opt_solver::mk_ge therefore projected the negative infinitesimal away, turning r >= 1 - epsilon into the over-strong, unsatisfiable r >= 1, so validation spuriously failed and the strictly smaller current model value was reported instead (e.g. r = 0). For shared-symbol objectives this also produced values matching neither the model nor the true optimum (issue #10028 follow-up). Fix: carry the infinitesimal faithfully through the bound pipeline. - lp_api::bound gains an eps component so get_value reports the true delta value (no spurious rational fixed-variable equality is propagated to EUF). - lar_base_constraint stores its right-hand side as a delta-rational impq pair; rhs() returns the rational component, bound_eps() the infinitesimal one. - lar_solver bound activation/update threads the whole impq bound, so a lower bound (r, -1) can be asserted; constraint_holds accounts for it using the same strict-bounds delta that flattens the model (computed once per model). - theory_lra::mk_ge builds a fresh predicate for the (r, -1) lower bound to avoid colliding with an already-internalized v >= r literal, and attaches eps = -1; opt_solver::mk_ge passes the unprojected value to theory_lra / theory_mi_arith / theory_inf_arith (whose bounds are inf_rational). Results: maximize r, r<1 -> 1-eps; minimize r, r>1 -> 1+eps; bounded and lex/box strict optima correct; integer optima and the #10028 shared-symbol cases unchanged. Unit tests 92/92; the opt regression corpus (model_validate=true) is byte-identical to baseline. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> |
||
|---|---|---|
| .. | ||
| ackermannization | ||
| api | ||
| ast | ||
| cmd_context | ||
| math | ||
| model | ||
| muz | ||
| nlsat | ||
| opt | ||
| params | ||
| parsers | ||
| qe | ||
| sat | ||
| shell | ||
| smt | ||
| solver | ||
| tactic | ||
| test | ||
| util | ||
| CMakeLists.txt | ||