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: drop LP-relaxation infinitesimal on NLA maximize path

Browse source 
The nonlinear optimization path (max_with_nl) returned the linear-relaxation
optimum lp_val including its infinitesimal.  That infinitesimal is an artifact
of the strict bounds introduced by the linearization, not a genuine strict
optimum of the nonlinear problem.  Threading it into opt_solver::mk_ge made
theory_lra assert a delta-rational lower bound (r, -1) that coincides with the
column's existing strict upper bound (r, -1), fixing the objective column at a
delta value the LP core never snapped, tripping the
non_basic_columns_are_set_correctly assertion in a debug build (unit tests
max_reg / max_rev).

Project the infinitesimal away in both NLA branches (FC_DONE and FC_CONTINUE);
the rational part remains a sound bound for check_bound to validate.  The
genuinely-strict, NLA-free path (e.g. pure LP suprema and shared-symbol/EUF
objectives) is unaffected, so faithful validation of strict optima is preserved.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-07-07 08:45:15 -07:00
parent 4065e4688c
commit 475af3e5c5
1 changed files with 13 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/smt/theory_lra.cpp
View file

@ -4068,11 +4068,22 @@ public:
tout << " x[" << j << "] = " << lp().get_column_value(j) << "\n";
}
});
// Discard the infinitesimal of the value returned from the NLA path.
// When NLA is involved the objective is nonlinear, so lp_val is the
// optimum of the LINEAR relaxation: its infinitesimal comes from the
// strict bounds introduced by the linearization, not from a genuine
// strict optimum of the nonlinear problem. If it were kept,
// opt_solver::mk_ge would assert a delta-rational bound (r, -1) that the
// real problem cannot honor, fixing the objective column at a delta
// value the LP core cannot snap on the next solve (assertion
// non_basic_columns_are_set_correctly). The rational part remains a
// sound bound for the optimizer to validate via check_bound.
inf_eps lp_val_no_eps(lp_val.get_infinity(), inf_rational(lp_val.get_rational()));
switch (nla_st) {
case FC_DONE:
// NLA satisfied: keep the optimal assignment, return LP value
blocker = mk_gt(v);
result = lp_val;
result = lp_val_no_eps;
st = lp::lp_status::FEASIBLE;
return true;
case FC_CONTINUE:
@ -4081,7 +4092,7 @@ public:
// as a bound for the optimizer to validate via check_bound().
lp().restore_x();
blocker = mk_gt(v, lp_ival);
result = lp_val;
result = lp_val_no_eps;
st = lp::lp_status::FEASIBLE;
return true;
case FC_GIVEUP: