From cd9346d2cdcede167429cb046d5b11c4b36a1c15 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Tue, 7 Jul 2026 01:10:06 -0700 Subject: [PATCH] opt: adopt exact strict supremum/infimum optima (fixes strict-optimum regression) For a strict real optimum such as `maximize a` subject to `a < 0`, the arithmetic solver returns the exact supremum `-epsilon` (a finite value with a non-zero infinitesimal). Since #10028, opt_solver::maximize_objective defers committing this hint to check_bound(), but check_bound() can never validate a strict supremum: mk_ge() must drop the negative infinitesimal (the strict real bound `a >= q - epsilon` is not expressible), so the assert+check is UNSAT and the exact optimum is discarded in favor of the strictly smaller current model value (e.g. -1/4 instead of -epsilon). An earlier fix (#10052) re-committed the infinitesimal hint unconditionally and was reverted (#10057) as unsound: for a shared-symbol objective (e.g. one whose value depends on the auxiliary UF that encodes a `distinct` with > 32 integer arguments) the LP relaxation only yields a hint that can strictly over-estimate the true optimum. This change follows the revert's prescription and gates the eager commit on a proved-exact optimum. theory_lra now reports has_shared == false only when the LP proved an exact OPTIMAL (integrality- and NLA-relaxed FEASIBLE hints report has_shared == true), and opt_solver only adopts a finite strict-infinitesimal value eagerly when that exact flag holds. This restores the strict single objective supremum/infimum (issues #5720, discussion Z3Prover/bench#3059) while keeping the shared-symbol hint deferred to validation, so the soundness fix of #10028 is preserved. The eager commit is strictly narrower than the pre-#10028 behavior (it fires only for finite strict optima with a proved-exact status). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/opt/opt_solver.cpp | 32 ++++++++++++++++++++++++++++++++ src/smt/theory_lra.cpp | 11 ++++++++++- 2 files changed, 42 insertions(+), 1 deletion(-) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index eb8b4dd6cb..c41c563ee7 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -312,6 +312,16 @@ namespace opt { inf_eps val = get_optimizer().maximize(v, blocker, has_shared); m_context.get_model(m_model); inf_eps val2; + // + // 'has_shared' as returned by maximize() is false only when the + // arithmetic solver proved an *exact* optimum: a pure-LP optimum with + // no shared-symbol or integrality relaxation (theory_lra returns an + // exact optimum only for lp_status::OPTIMAL; theory_arith only when no + // shared symbols or nonlinear monomials are involved). Capture it + // before it is overwritten below; it tells us whether a strict + // supremum hint is trustworthy enough to adopt without validation. + // + bool exact_optimum = !has_shared; has_shared = true; TRACE(opt, tout << (has_shared?"has shared":"non-shared") << " " << val << " " << blocker << "\n"; if (m_model) tout << *m_model << "\n";); @@ -342,6 +352,28 @@ namespace opt { return true; } + // + // The arithmetic solver proved an exact optimum (exact_optimum) whose + // value is a strict supremum: a finite value carrying a non-zero + // infinitesimal, e.g. 'maximize a' subject to 'a < 0' yields -epsilon. + // Such a bound is genuinely achievable in the limit but cannot be + // re-validated by check_bound() below: mk_ge() has to drop the negative + // infinitesimal (the strict real bound 'a >= q - epsilon' is not + // expressible), so the subsequent assert+check is UNSAT and the hint + // would otherwise be discarded, leaving m_objective_values holding the + // strictly smaller current model value (regression from #10028; + // discussion Z3Prover/bench#3059). Adopt it here. This is restricted + // to proved-exact optima: for shared-symbol or relaxed hints + // (has_shared) the value may over-estimate the true optimum and is + // still deferred to validation below, so the soundness fix of #10028 + // (and the revert of #10052) is preserved. update_objective() only + // ever raises the stored value, so a genuine larger model value still + // wins. + // + if (exact_optimum && val.is_finite() && !val.get_infinitesimal().is_zero() && + val > m_objective_values[i]) + m_objective_values[i] = val; + // // retrieve value of objective from current model and update // current optimal. diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index d3ac4840ad..b092cd4850 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -4089,6 +4089,11 @@ public: return value(v); case lp::lp_status::FEASIBLE: TRACE(arith, display(tout << st << " v" << v << " vi: " << vi << "\n");); + // FEASIBLE (as opposed to OPTIMAL) means the returned value is only + // a hint: the exact optimum could not be proved, e.g. integrality + // forced a fallback to a feasible assignment. Flag it as shared so + // the optimizer validates the bound instead of adopting it eagerly. + has_shared = true; blocker = mk_gt(v); return value(v); default: @@ -4118,8 +4123,12 @@ public: else { st = max_with_lp(v, vi, term_max); inf_eps nl_result; - if (max_with_nl(v, st, level, blocker, nl_result)) + if (max_with_nl(v, st, level, blocker, nl_result)) { + // NLA returned a feasible hint rather than a proved optimum; + // mark it as shared so the optimizer validates it. + has_shared = true; return nl_result; + } } return max_result(v, vi, st, blocker, has_shared); }