From acd2e9475d4c5d3e7f18434b23887f971a6403e2 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 19 Mar 2026 10:09:34 -1000 Subject: [PATCH] fix #9030: box mode objectives are now optimized independently In box mode (opt.priority=box), each objective should be optimized independently. Previously, box() called geometric_opt() which optimizes all objectives together using a shared disjunction of bounds. This caused adding/removing an objective to change the optimal values of other objectives. Fix: Rewrite box() to optimize each objective in its own push/pop scope using geometric_lex, ensuring complete isolation between objectives. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/opt/optsmt.cpp | 40 ++++++++++++++++--------- src/opt/optsmt.h | 2 +- src/test/api.cpp | 73 ++++++++++++++++++++++++++++++++++++++++++++++ src/test/main.cpp | 1 + 4 files changed, 101 insertions(+), 15 deletions(-) diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 8a321d28a..29fc2961b 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -202,15 +202,19 @@ namespace opt { } } - lbool optsmt::geometric_lex(unsigned obj_index, bool is_maximize) { + lbool optsmt::geometric_lex(unsigned obj_index, bool is_maximize, bool is_box) { TRACE(opt, tout << "index: " << obj_index << " is-max: " << is_maximize << "\n";); arith_util arith(m); bool is_int = arith.is_int(m_objs.get(obj_index)); lbool is_sat = l_true; expr_ref bound(m), last_bound(m); - for (unsigned i = 0; i < obj_index; ++i) - commit_assignment(i); + // In lex mode, commit previous objectives so that earlier objectives + // constrain later ones. In box mode, skip this so each objective + // is optimized independently. + if (!is_box) + for (unsigned i = 0; i < obj_index; ++i) + commit_assignment(i); unsigned steps = 0; unsigned step_incs = 0; @@ -291,9 +295,9 @@ namespace opt { // set the solution tight. m_upper[obj_index] = m_lower[obj_index]; - for (unsigned i = obj_index+1; i < m_lower.size(); ++i) { - m_lower[i] = inf_eps(rational(-1), inf_rational(0)); - } + if (!is_box) + for (unsigned i = obj_index+1; i < m_lower.size(); ++i) + m_lower[i] = inf_eps(rational(-1), inf_rational(0)); return l_true; } @@ -534,15 +538,23 @@ namespace opt { if (m_vars.empty()) { return is_sat; } - // assertions added during search are temporary. - solver::scoped_push _push(*m_s); - if (m_optsmt_engine == symbol("symba")) { - is_sat = symba_opt(); + // In box mode, optimize each objective independently. + // Each objective gets its own push/pop scope so that bounds + // from one objective do not constrain another. + // Note: geometric_lex is used unconditionally here, even when + // m_optsmt_engine is "symba", because symba_opt and geometric_opt + // optimize all objectives jointly, violating box mode semantics. + m_context.get_base_model(m_best_model); + for (unsigned i = 0; i < m_vars.size() && m.inc(); ++i) { + solver::scoped_push _push(*m_s); + is_sat = geometric_lex(i, true, true); + if (is_sat == l_undef) + return l_undef; + if (is_sat == l_false) + return l_false; + m_models.set(i, m_best_model.get()); } - else { - is_sat = geometric_opt(); - } - return is_sat; + return l_true; } diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h index 80dd4e5f7..b1198a7f9 100644 --- a/src/opt/optsmt.h +++ b/src/opt/optsmt.h @@ -81,7 +81,7 @@ namespace opt { lbool symba_opt(); - lbool geometric_lex(unsigned idx, bool is_maximize); + lbool geometric_lex(unsigned idx, bool is_maximize, bool is_box = false); void set_max(vector& dst, vector const& src, expr_ref_vector& fmls); diff --git a/src/test/api.cpp b/src/test/api.cpp index ac4fe9818..e9a3cd6f7 100644 --- a/src/test/api.cpp +++ b/src/test/api.cpp @@ -519,3 +519,76 @@ void tst_box_mod_opt() { Z3_del_context(ctx); std::cout << "box mod optimization test passed" << std::endl; } + +// Regression test for #9030: adding an objective in box mode must not +// change the optimal values of other objectives. +void tst_box_independent() { + Z3_config cfg = Z3_mk_config(); + Z3_context ctx = Z3_mk_context(cfg); + Z3_del_config(cfg); + + Z3_sort int_sort = Z3_mk_int_sort(ctx); + Z3_ast a = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "a"), int_sort); + Z3_ast b = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "b"), int_sort); + + auto mk_int = [&](int v) { return Z3_mk_int(ctx, v, int_sort); }; + + // Helper: create a fresh optimizer with box priority and constraints + // equivalent to: b >= -166, a <= -166, 5a >= 9b + 178 + auto mk_opt = [&]() { + Z3_optimize opt = Z3_mk_optimize(ctx); + Z3_optimize_inc_ref(ctx, opt); + Z3_params p = Z3_mk_params(ctx); + Z3_params_inc_ref(ctx, p); + Z3_params_set_symbol(ctx, p, Z3_mk_string_symbol(ctx, "priority"), + Z3_mk_string_symbol(ctx, "box")); + Z3_optimize_set_params(ctx, opt, p); + Z3_params_dec_ref(ctx, p); + Z3_optimize_assert(ctx, opt, Z3_mk_ge(ctx, b, mk_int(-166))); + Z3_optimize_assert(ctx, opt, Z3_mk_le(ctx, a, mk_int(-166))); + // 5a - 9b >= 178 + Z3_ast lhs_args[] = { mk_int(5), a }; + Z3_ast five_a = Z3_mk_mul(ctx, 2, lhs_args); + Z3_ast rhs_args[] = { mk_int(9), b }; + Z3_ast nine_b = Z3_mk_mul(ctx, 2, rhs_args); + Z3_ast diff_args[] = { five_a, nine_b }; + Z3_ast diff = Z3_mk_sub(ctx, 2, diff_args); + Z3_optimize_assert(ctx, opt, Z3_mk_ge(ctx, diff, mk_int(178))); + return opt; + }; + + // objective: maximize -(b + a) + auto mk_neg_sum = [&]() { + Z3_ast args[] = { b, a }; + return Z3_mk_unary_minus(ctx, Z3_mk_add(ctx, 2, args)); + }; + + // Run 1: three objectives + Z3_optimize opt3 = mk_opt(); + unsigned idx_max_expr_3 = Z3_optimize_maximize(ctx, opt3, mk_neg_sum()); + Z3_optimize_maximize(ctx, opt3, b); + unsigned idx_min_a_3 = Z3_optimize_minimize(ctx, opt3, a); + ENSURE(Z3_optimize_check(ctx, opt3, 0, nullptr) == Z3_L_TRUE); + + // Run 2: two objectives, without (maximize b) + Z3_optimize opt2 = mk_opt(); + unsigned idx_max_expr_2 = Z3_optimize_maximize(ctx, opt2, mk_neg_sum()); + unsigned idx_min_a_2 = Z3_optimize_minimize(ctx, opt2, a); + ENSURE(Z3_optimize_check(ctx, opt2, 0, nullptr) == Z3_L_TRUE); + + // The shared objectives must have the same optimal values + Z3_string val_max3 = Z3_ast_to_string(ctx, Z3_optimize_get_lower(ctx, opt3, idx_max_expr_3)); + Z3_string val_max2 = Z3_ast_to_string(ctx, Z3_optimize_get_lower(ctx, opt2, idx_max_expr_2)); + std::cout << "maximize expr with 3 obj: " << val_max3 << ", with 2 obj: " << val_max2 << std::endl; + ENSURE(std::string(val_max3) == std::string(val_max2)); + + Z3_string val_min3 = Z3_ast_to_string(ctx, Z3_optimize_get_upper(ctx, opt3, idx_min_a_3)); + Z3_string val_min2 = Z3_ast_to_string(ctx, Z3_optimize_get_upper(ctx, opt2, idx_min_a_2)); + std::cout << "minimize a with 3 obj: " << val_min3 << ", with 2 obj: " << val_min2 << std::endl; + ENSURE(std::string(val_min3) == std::string(val_min2)); + + Z3_optimize_dec_ref(ctx, opt3); + Z3_optimize_dec_ref(ctx, opt2); + Z3_del_context(ctx); + std::cout << "box independent objectives test passed" << std::endl; +} diff --git a/src/test/main.cpp b/src/test/main.cpp index 8e5bd70fb..2d52a64c5 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -78,6 +78,7 @@ X(max_rev) \ X(scaled_min) \ X(box_mod_opt) \ + X(box_independent) \ X(deep_api_bugs) \ X(api_algebraic) \ X(api_polynomial) \