mirror of
https://github.com/Z3Prover/z3
synced 2026-07-18 21:15:47 +00:00
opt: validate strict optimization optima faithfully with delta-rational bounds (#10059)
## Problem Maximizing/minimizing under a **strict** inequality has a delta-rational optimum. For ```smt2 (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 #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> --------- Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Lev Nachmanson
GitHub
parent
5a55ed7cfb
commit
ed6e2a241d
7 changed files with 212 additions and 84 deletions
|
|
@ -1338,10 +1338,14 @@ namespace lp {
|
|||
if (m_imp->m_settings.get_cancel_flag())
|
||||
return true;
|
||||
std::unordered_map<lpvar, mpq> var_map;
|
||||
get_model_do_not_care_about_diff_vars(var_map);
|
||||
// Compute the strict-bounds delta once per model: it flattens both the
|
||||
// model (var_map) and the eps component of any delta-rational bound in
|
||||
// constraint_holds, so the two must use the very same value.
|
||||
mpq delta = get_core_solver().find_delta_for_strict_bounds(m_imp->m_settings.m_epsilon);
|
||||
get_model_do_not_care_about_diff_vars(var_map, delta);
|
||||
|
||||
for (auto const& c : m_imp->m_constraints.active()) {
|
||||
if (!constraint_holds(c, var_map)) {
|
||||
if (!constraint_holds(c, var_map, delta)) {
|
||||
TRACE(lar_solver,
|
||||
m_imp->m_constraints.display(tout, c) << "\n";
|
||||
for (auto p : c.coeffs()) {
|
||||
|
|
@ -1353,14 +1357,21 @@ namespace lp {
|
|||
return true;
|
||||
}
|
||||
|
||||
bool lar_solver::constraint_holds(const lar_base_constraint& constr, std::unordered_map<lpvar, mpq>& var_map) const {
|
||||
bool lar_solver::constraint_holds(const lar_base_constraint& constr, std::unordered_map<lpvar, mpq>& var_map, const mpq& delta) const {
|
||||
mpq left_side_val = get_left_side_val(constr, var_map);
|
||||
// Account for a delta-rational bound rhs + eps*delta (eps != 0 only for
|
||||
// the bounds that validate strict optimization optima). 'delta' is the
|
||||
// same strict-bounds delta that flattened var_map, so the comparison is
|
||||
// exact over the reals.
|
||||
mpq rhs = constr.rhs();
|
||||
if (!constr.bound_eps().is_zero())
|
||||
rhs += constr.bound_eps() * delta;
|
||||
switch (constr.kind()) {
|
||||
case LE: return left_side_val <= constr.rhs();
|
||||
case LT: return left_side_val < constr.rhs();
|
||||
case GE: return left_side_val >= constr.rhs();
|
||||
case GT: return left_side_val > constr.rhs();
|
||||
case EQ: return left_side_val == constr.rhs();
|
||||
case LE: return left_side_val <= rhs;
|
||||
case LT: return left_side_val < rhs;
|
||||
case GE: return left_side_val >= rhs;
|
||||
case GT: return left_side_val > rhs;
|
||||
case EQ: return left_side_val == rhs;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
|
@ -1583,6 +1594,10 @@ namespace lp {
|
|||
|
||||
void lar_solver::get_model_do_not_care_about_diff_vars(std::unordered_map<lpvar, mpq>& variable_values) const {
|
||||
mpq delta = get_core_solver().find_delta_for_strict_bounds(m_imp->m_settings.m_epsilon);
|
||||
get_model_do_not_care_about_diff_vars(variable_values, delta);
|
||||
}
|
||||
|
||||
void lar_solver::get_model_do_not_care_about_diff_vars(std::unordered_map<lpvar, mpq>& variable_values, const mpq& delta) const {
|
||||
for (unsigned i = 0; i < get_core_solver().r_x().size(); ++i) {
|
||||
const impq& rp = get_core_solver().r_x(i);
|
||||
variable_values[i] = rp.x + delta * rp.y;
|
||||
|
|
@ -2142,12 +2157,12 @@ namespace lp {
|
|||
|
||||
void lar_solver::activate_check_on_equal(constraint_index ci, unsigned& equal_column) {
|
||||
auto const& c = m_imp->m_constraints[ci];
|
||||
update_column_type_and_bound_check_on_equal(c.column(), c.rhs(), ci, equal_column);
|
||||
update_column_type_and_bound_check_on_equal(c.column(), c.rhs_impq(), ci, equal_column);
|
||||
}
|
||||
|
||||
void lar_solver::activate(constraint_index ci) {
|
||||
auto const& c = m_imp->m_constraints[ci];
|
||||
update_column_type_and_bound(c.column(), c.rhs(), ci);
|
||||
update_column_type_and_bound(c.column(), c.rhs_impq(), ci);
|
||||
}
|
||||
|
||||
mpq lar_solver::adjust_bound_for_int(lpvar j, lconstraint_kind& k, const mpq& bound) {
|
||||
|
|
@ -2191,6 +2206,24 @@ namespace lp {
|
|||
return ci;
|
||||
}
|
||||
|
||||
// Variant that attaches an infinitesimal coefficient 'eps' to the bound, so
|
||||
// that activating the resulting constraint asserts the delta-rational bound
|
||||
// (right_side, eps). Used to faithfully validate strict optimization optima
|
||||
// (e.g. a maximize supremum r - delta is validated as a lower bound
|
||||
// (r, -1)). Only supported for plain column bounds (no term column).
|
||||
constraint_index lar_solver::mk_var_bound(lpvar j, lconstraint_kind kind, const mpq& right_side, const mpq& eps) {
|
||||
TRACE(lar_solver, tout << "j = " << get_variable_name(j) << " " << lconstraint_kind_string(kind) << " " << right_side << " + " << eps << "*eps" << std::endl;);
|
||||
mpq rs = adjust_bound_for_int(j, kind, right_side);
|
||||
SASSERT(bound_is_integer_for_integer_column(j, rs));
|
||||
constraint_index ci;
|
||||
if (!column_has_term(j))
|
||||
ci = m_imp->m_constraints.add_var_constraint(j, kind, rs, eps);
|
||||
else
|
||||
ci = m_imp->m_constraints.add_term_constraint(j, m_imp->m_columns[j].term(), kind, rs, eps);
|
||||
SASSERT(sizes_are_correct());
|
||||
return ci;
|
||||
}
|
||||
|
||||
bool lar_solver::compare_values(lpvar j, lconstraint_kind k, const mpq& rhs) {
|
||||
return compare_values(get_column_value(j), k, rhs);
|
||||
}
|
||||
|
|
@ -2209,7 +2242,7 @@ namespace lp {
|
|||
}
|
||||
|
||||
void lar_solver::update_column_type_and_bound(unsigned j,
|
||||
const mpq& right_side,
|
||||
const impq& right_side,
|
||||
constraint_index constr_index) {
|
||||
TRACE(lar_solver_feas, tout << "j = " << j << " was " << (this->column_is_feasible(j)?"feas":"non-feas") << std::endl;);
|
||||
m_imp->m_constraints.activate(constr_index);
|
||||
|
|
@ -2273,7 +2306,10 @@ namespace lp {
|
|||
ls.add_var_bound(tv, c.kind(), c.rhs());
|
||||
}
|
||||
void lar_solver::update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
|
||||
// SASSERT(validate_bound(j, kind, right_side, dep));
|
||||
update_column_type_and_bound(j, kind, impq(right_side), dep);
|
||||
}
|
||||
void lar_solver::update_column_type_and_bound(unsigned j, lconstraint_kind kind, const impq& right_side, u_dependency* dep) {
|
||||
// SASSERT(validate_bound(j, kind, right_side.x, dep));
|
||||
TRACE(
|
||||
lar_solver_feas,
|
||||
tout << "j" << j << " " << lconstraint_kind_string(kind) << " " << right_side << std::endl;
|
||||
|
|
@ -2287,11 +2323,16 @@ namespace lp {
|
|||
}
|
||||
});
|
||||
bool was_fixed = column_is_fixed(j);
|
||||
mpq rs = adjust_bound_for_int(j, kind, right_side);
|
||||
// adjust_bound_for_int operates on the rational part (and may sharpen
|
||||
// the kind for integer columns); the infinitesimal part y is carried
|
||||
// through unchanged. y is non-zero only for the delta-rational bounds
|
||||
// that validate strict optimization optima, which target real columns.
|
||||
mpq rs = adjust_bound_for_int(j, kind, right_side.x);
|
||||
impq bound(rs, right_side.y);
|
||||
if (column_has_upper_bound(j))
|
||||
update_column_type_and_bound_with_ub(j, kind, rs, dep);
|
||||
update_column_type_and_bound_with_ub(j, kind, bound, dep);
|
||||
else
|
||||
update_column_type_and_bound_with_no_ub(j, kind, rs, dep);
|
||||
update_column_type_and_bound_with_no_ub(j, kind, bound, dep);
|
||||
|
||||
if (!was_fixed && column_is_fixed(j) && m_fixed_var_eh)
|
||||
m_fixed_var_eh(j);
|
||||
|
|
@ -2320,7 +2361,7 @@ namespace lp {
|
|||
}
|
||||
|
||||
void lar_solver::update_column_type_and_bound_check_on_equal(unsigned j,
|
||||
const mpq& right_side,
|
||||
const impq& right_side,
|
||||
constraint_index constr_index,
|
||||
unsigned& equal_to_j) {
|
||||
update_column_type_and_bound(j, right_side, constr_index);
|
||||
|
|
@ -2336,7 +2377,7 @@ namespace lp {
|
|||
return m_imp->m_constraints.add_term_constraint(j, m_imp->m_columns[j].term(), kind, rs);
|
||||
}
|
||||
|
||||
void lar_solver::update_column_type_and_bound_with_ub(unsigned j, lp::lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
|
||||
void lar_solver::update_column_type_and_bound_with_ub(unsigned j, lp::lconstraint_kind kind, const impq& right_side, u_dependency* dep) {
|
||||
SASSERT(column_has_upper_bound(j));
|
||||
if (column_has_lower_bound(j)) {
|
||||
update_bound_with_ub_lb(j, kind, right_side, dep);
|
||||
|
|
@ -2346,7 +2387,7 @@ namespace lp {
|
|||
}
|
||||
}
|
||||
|
||||
void lar_solver::update_column_type_and_bound_with_no_ub(unsigned j, lp::lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
|
||||
void lar_solver::update_column_type_and_bound_with_no_ub(unsigned j, lp::lconstraint_kind kind, const impq& right_side, u_dependency* dep) {
|
||||
SASSERT(!column_has_upper_bound(j));
|
||||
if (column_has_lower_bound(j)) {
|
||||
update_bound_with_no_ub_lb(j, kind, right_side, dep);
|
||||
|
|
@ -2356,18 +2397,18 @@ namespace lp {
|
|||
}
|
||||
}
|
||||
|
||||
void lar_solver::update_bound_with_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
|
||||
void lar_solver::update_bound_with_ub_lb(lpvar j, lconstraint_kind kind, const impq& right_side, u_dependency* dep) {
|
||||
SASSERT(column_has_lower_bound(j) && column_has_upper_bound(j));
|
||||
SASSERT(get_core_solver().m_column_types[j] == column_type::boxed ||
|
||||
get_core_solver().m_column_types[j] == column_type::fixed);
|
||||
|
||||
mpq y_of_bound(0);
|
||||
mpq y_of_bound(right_side.y);
|
||||
switch (kind) {
|
||||
case LT:
|
||||
y_of_bound = -1;
|
||||
y_of_bound += -1;
|
||||
Z3_fallthrough;
|
||||
case LE: {
|
||||
auto up = numeric_pair<mpq>(right_side, y_of_bound);
|
||||
auto up = numeric_pair<mpq>(right_side.x, y_of_bound);
|
||||
if (up < get_lower_bound(j)) {
|
||||
set_crossed_bounds_column_and_deps(j, true, dep);
|
||||
}
|
||||
|
|
@ -2379,10 +2420,10 @@ namespace lp {
|
|||
break;
|
||||
}
|
||||
case GT:
|
||||
y_of_bound = 1;
|
||||
y_of_bound += 1;
|
||||
Z3_fallthrough;
|
||||
case GE: {
|
||||
auto low = numeric_pair<mpq>(right_side, y_of_bound);
|
||||
auto low = numeric_pair<mpq>(right_side.x, y_of_bound);
|
||||
if (low > get_upper_bound(j)) {
|
||||
set_crossed_bounds_column_and_deps(j, false, dep);
|
||||
}
|
||||
|
|
@ -2395,7 +2436,7 @@ namespace lp {
|
|||
break;
|
||||
}
|
||||
case EQ: {
|
||||
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
|
||||
auto v = numeric_pair<mpq>(right_side.x, zero_of_type<mpq>());
|
||||
if (v > get_upper_bound(j))
|
||||
set_crossed_bounds_column_and_deps(j, false, dep);
|
||||
else if (v < get_lower_bound(j))
|
||||
|
|
@ -2416,17 +2457,17 @@ namespace lp {
|
|||
get_core_solver().m_column_types[j] = column_type::fixed;
|
||||
}
|
||||
|
||||
void lar_solver::update_bound_with_no_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
|
||||
void lar_solver::update_bound_with_no_ub_lb(lpvar j, lconstraint_kind kind, const impq& right_side, u_dependency* dep) {
|
||||
SASSERT(column_has_lower_bound(j) && !column_has_upper_bound(j));
|
||||
SASSERT(get_core_solver().m_column_types[j] == column_type::lower_bound);
|
||||
|
||||
mpq y_of_bound(0);
|
||||
mpq y_of_bound(right_side.y);
|
||||
switch (kind) {
|
||||
case LT:
|
||||
y_of_bound = -1;
|
||||
y_of_bound += -1;
|
||||
Z3_fallthrough;
|
||||
case LE: {
|
||||
auto up = numeric_pair<mpq>(right_side, y_of_bound);
|
||||
auto up = numeric_pair<mpq>(right_side.x, y_of_bound);
|
||||
if (up < get_lower_bound(j)) {
|
||||
set_crossed_bounds_column_and_deps(j, true, dep);
|
||||
}
|
||||
|
|
@ -2437,9 +2478,9 @@ namespace lp {
|
|||
break;
|
||||
}
|
||||
case GT:
|
||||
y_of_bound = 1;
|
||||
y_of_bound += 1;
|
||||
case GE: {
|
||||
auto low = numeric_pair<mpq>(right_side, y_of_bound);
|
||||
auto low = numeric_pair<mpq>(right_side.x, y_of_bound);
|
||||
if (low < get_lower_bound(j)) {
|
||||
return;
|
||||
}
|
||||
|
|
@ -2447,7 +2488,7 @@ namespace lp {
|
|||
break;
|
||||
}
|
||||
case EQ: {
|
||||
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
|
||||
auto v = numeric_pair<mpq>(right_side.x, zero_of_type<mpq>());
|
||||
if (v < get_lower_bound(j)) {
|
||||
set_crossed_bounds_column_and_deps(j, true, dep);
|
||||
}
|
||||
|
|
@ -2464,28 +2505,28 @@ namespace lp {
|
|||
}
|
||||
}
|
||||
|
||||
void lar_solver::update_bound_with_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
|
||||
void lar_solver::update_bound_with_ub_no_lb(lpvar j, lconstraint_kind kind, const impq& right_side, u_dependency* dep) {
|
||||
SASSERT(!column_has_lower_bound(j) && column_has_upper_bound(j));
|
||||
SASSERT(get_core_solver().m_column_types[j] == column_type::upper_bound);
|
||||
mpq y_of_bound(0);
|
||||
mpq y_of_bound(right_side.y);
|
||||
switch (kind) {
|
||||
case LT:
|
||||
y_of_bound = -1;
|
||||
y_of_bound += -1;
|
||||
Z3_fallthrough;
|
||||
case LE:
|
||||
{
|
||||
auto up = numeric_pair<mpq>(right_side, y_of_bound);
|
||||
auto up = numeric_pair<mpq>(right_side.x, y_of_bound);
|
||||
if (up >= get_upper_bound(j))
|
||||
return;
|
||||
set_upper_bound_witness(j, dep, up);
|
||||
}
|
||||
break;
|
||||
case GT:
|
||||
y_of_bound = 1;
|
||||
y_of_bound += 1;
|
||||
Z3_fallthrough;
|
||||
case GE:
|
||||
{
|
||||
auto low = numeric_pair<mpq>(right_side, y_of_bound);
|
||||
auto low = numeric_pair<mpq>(right_side.x, y_of_bound);
|
||||
if (low > get_upper_bound(j)) {
|
||||
set_crossed_bounds_column_and_deps(j, false, dep);
|
||||
}
|
||||
|
|
@ -2497,7 +2538,7 @@ namespace lp {
|
|||
break;
|
||||
case EQ:
|
||||
{
|
||||
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
|
||||
auto v = numeric_pair<mpq>(right_side.x, zero_of_type<mpq>());
|
||||
if (v > get_upper_bound(j)) {
|
||||
set_crossed_bounds_column_and_deps(j, false, dep);
|
||||
}
|
||||
|
|
@ -2514,30 +2555,30 @@ namespace lp {
|
|||
}
|
||||
}
|
||||
|
||||
void lar_solver::update_bound_with_no_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
|
||||
void lar_solver::update_bound_with_no_ub_no_lb(lpvar j, lconstraint_kind kind, const impq& right_side, u_dependency* dep) {
|
||||
SASSERT(!column_has_lower_bound(j) && !column_has_upper_bound(j));
|
||||
|
||||
mpq y_of_bound(0);
|
||||
mpq y_of_bound(right_side.y);
|
||||
switch (kind) {
|
||||
case LT:
|
||||
y_of_bound = -1;
|
||||
y_of_bound += -1;
|
||||
Z3_fallthrough;
|
||||
case LE: {
|
||||
auto up = numeric_pair<mpq>(right_side, y_of_bound);
|
||||
auto up = numeric_pair<mpq>(right_side.x, y_of_bound);
|
||||
set_upper_bound_witness(j, dep, up);
|
||||
get_core_solver().m_column_types[j] = column_type::upper_bound;
|
||||
} break;
|
||||
case GT:
|
||||
y_of_bound = 1;
|
||||
y_of_bound += 1;
|
||||
Z3_fallthrough;
|
||||
case GE: {
|
||||
auto low = numeric_pair<mpq>(right_side, y_of_bound);
|
||||
auto low = numeric_pair<mpq>(right_side.x, y_of_bound);
|
||||
set_lower_bound_witness(j, dep, low);
|
||||
get_core_solver().m_column_types[j] = column_type::lower_bound;
|
||||
|
||||
} break;
|
||||
case EQ: {
|
||||
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
|
||||
auto v = numeric_pair<mpq>(right_side.x, zero_of_type<mpq>());
|
||||
set_upper_bound_witness(j, dep, v);
|
||||
set_lower_bound_witness(j, dep, v);
|
||||
get_core_solver().m_column_types[j] = column_type::fixed;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue