opt: validate strict optimization optima faithfully with delta-rational bounds

[levnach]

Problem

Maximizing/minimizing under a strict inequality has a delta-rational optimum. For

(declare-const r Real)
(assert (< r 1))
(maximize r)
(check-sat)
(get-objectives)

the optimum is the supremum 1 - epsilon, but z3 reported r = 0.

The same defect makes shared-symbol objectives report a value matching neither the model nor the true optimum (issue #10028 follow-up). Minimal reproducer — a 6-mark Golomb ruler (a >32-arg distinct, so the objective is coupled to EUF) with a strict real objective obj > x5, whose true optimum is 17 + epsilon:

case	before	after
maximize r, r < 1	0 ❌	1 - epsilon ✅
minimize r, r > 1	0 ❌	1 + epsilon ✅
Golomb minimize obj, obj > x5	35/2 / 7+eps ❌	17 + epsilon ✅

Root cause

check_bound validates the LP hint by asserting objective >= optimum. For a supremum 1 - epsilon this is a lower bound whose value carries a negative infinitesimal (1, -1).

No lconstraint_kind can express that. The kind->infinitesimal map only yields the matching-sign cases — GT -> lower (r, +1), LT -> upper (r, -1) — or zero (GE/LE). The opposite-sign lower bound (r, -1) (i.e. r >= r0 - delta) is a relaxation that no strict inequality produces. opt_solver::mk_ge therefore projected the -epsilon away, turning r >= 1 - epsilon into the over-strong, unsatisfiable r >= 1; validation failed and the strictly smaller current model value was reported instead.

Fix — carry the infinitesimal faithfully through the bound pipeline

• lp_api::bound gains an eps component so get_value returns 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 already inf_rational).

The pair machinery is what makes the supremum both representable (optimum 1 - epsilon) and validatable; the reported witness model remains the flattened rational (find_delta_for_strict_bounds), consistent with the existing epsilon semantics.

Validation

• Strict optima correct: 1-eps, 1+eps, bounded 2<r<5 -> 5-eps, and lex/box variants.
• Integer optima and the Z3 incorrect objective with inconsistent bounds #10028 shared-symbol cases unchanged (Golomb n=6/7/8 -> 17/25/34, consistent with the model).
• Unit tests 92/92 (release); no new debug-suite failures.
• Opt regression corpus (73 files, model_validate=true) byte-identical to baseline.

Co-authored-by: Copilot 223556219+Copilot@users.noreply.github.com

[levnach]

@NikolajBjorner , I think one of the main changes is here:

z3/src/math/lp/lar_constraints.h

Line 52 in 4065e46

impq m_right_side;

. This allows to theory_lra to express something like (max x, x >= 3 - eps) in lar_solver.

[NikolajBjorner]

simplify away if-then-else to just else branch