From ce7c7f458e98cd9db7e1f4ce396f3e1f9e484942 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 11 Mar 2026 18:15:57 -1000 Subject: [PATCH] Add max_rev test: BNH with reversed argument order in f1/f2 Same as test_bnh_optimize but constructs f1 and f2 with reversed parameter order in mk_add, mk_mul, mk_sub calls. Exposes optimizer sensitivity to expression structure. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/test/api.cpp | 109 ++++++++++++++++++++++++++++++++++++++++++++++ src/test/main.cpp | 1 + 2 files changed, 110 insertions(+) diff --git a/src/test/api.cpp b/src/test/api.cpp index 76303ca9b..671913591 100644 --- a/src/test/api.cpp +++ b/src/test/api.cpp @@ -288,3 +288,112 @@ void tst_api() { void tst_bnh_opt() { test_bnh_optimize(); } + +void test_max_rev() { + // Same as test_bnh_optimize but with reversed argument order in f1/f2 construction. + Z3_config cfg = Z3_mk_config(); + Z3_context ctx = Z3_mk_context(cfg); + Z3_del_config(cfg); + + Z3_sort real_sort = Z3_mk_real_sort(ctx); + Z3_ast x1 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x1"), real_sort); + Z3_ast x2 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x2"), real_sort); + + auto mk_real = [&](int num, int den = 1) { return Z3_mk_real(ctx, num, den); }; + auto mk_mul = [&](Z3_ast a, Z3_ast b) { Z3_ast args[] = {a, b}; return Z3_mk_mul(ctx, 2, args); }; + auto mk_add = [&](Z3_ast a, Z3_ast b) { Z3_ast args[] = {a, b}; return Z3_mk_add(ctx, 2, args); }; + auto mk_sub = [&](Z3_ast a, Z3_ast b) { Z3_ast args[] = {a, b}; return Z3_mk_sub(ctx, 2, args); }; + auto mk_sq = [&](Z3_ast a) { return mk_mul(a, a); }; + + // f1 = 4*x2^2 + 4*x1^2 (reversed from: 4*x1^2 + 4*x2^2) + Z3_ast f1 = mk_add(mk_mul(mk_sq(x2), mk_real(4)), mk_mul(mk_sq(x1), mk_real(4))); + // f2 = (x2-5)^2 + (x1-5)^2 (reversed from: (x1-5)^2 + (x2-5)^2) + Z3_ast f2 = mk_add(mk_sq(mk_sub(mk_real(5), x2)), mk_sq(mk_sub(mk_real(5), x1))); + + auto mk_bnh_opt = [&]() -> Z3_optimize { + 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_uint(ctx, p, Z3_mk_string_symbol(ctx, "timeout"), 5000); + Z3_optimize_set_params(ctx, opt, p); + Z3_params_dec_ref(ctx, p); + Z3_optimize_assert(ctx, opt, Z3_mk_ge(ctx, x1, mk_real(0))); + Z3_optimize_assert(ctx, opt, Z3_mk_le(ctx, x1, mk_real(5))); + Z3_optimize_assert(ctx, opt, Z3_mk_ge(ctx, x2, mk_real(0))); + Z3_optimize_assert(ctx, opt, Z3_mk_le(ctx, x2, mk_real(3))); + Z3_optimize_assert(ctx, opt, Z3_mk_le(ctx, mk_add(mk_sq(mk_sub(mk_real(5), x1)), mk_sq(x2)), mk_real(25))); + Z3_optimize_assert(ctx, opt, Z3_mk_ge(ctx, mk_add(mk_sq(mk_sub(mk_real(8), x1)), mk_sq(mk_add(mk_real(3), x2))), mk_real(77, 10))); + return opt; + }; + + auto result_str = [](Z3_lbool r) { return r == Z3_L_TRUE ? "sat" : r == Z3_L_FALSE ? "unsat" : "unknown"; }; + + unsigned num_sat = 0; + + { + Z3_optimize opt = mk_bnh_opt(); + Z3_optimize_minimize(ctx, opt, f1); + Z3_lbool result = Z3_optimize_check(ctx, opt, 0, nullptr); + std::cout << "max_rev min f1: " << result_str(result) << std::endl; + ENSURE(result == Z3_L_TRUE); + if (result == Z3_L_TRUE) { + Z3_model m = Z3_optimize_get_model(ctx, opt); + Z3_model_inc_ref(ctx, m); + Z3_ast val; Z3_model_eval(ctx, m, f1, true, &val); + std::cout << " f1=" << Z3_ast_to_string(ctx, val) << std::endl; + Z3_model_dec_ref(ctx, m); + num_sat++; + } + Z3_optimize_dec_ref(ctx, opt); + } + + { + Z3_optimize opt = mk_bnh_opt(); + Z3_optimize_minimize(ctx, opt, f2); + Z3_lbool result = Z3_optimize_check(ctx, opt, 0, nullptr); + std::cout << "max_rev min f2: " << result_str(result) << std::endl; + ENSURE(result == Z3_L_TRUE); + if (result == Z3_L_TRUE) { + Z3_model m = Z3_optimize_get_model(ctx, opt); + Z3_model_inc_ref(ctx, m); + Z3_ast val; Z3_model_eval(ctx, m, f2, true, &val); + std::cout << " f2=" << Z3_ast_to_string(ctx, val) << std::endl; + Z3_model_dec_ref(ctx, m); + num_sat++; + } + Z3_optimize_dec_ref(ctx, opt); + } + + int weights[][2] = {{1, 4}, {2, 3}, {1, 1}, {3, 2}, {4, 1}}; + for (auto& w : weights) { + Z3_optimize opt = mk_bnh_opt(); + Z3_ast weighted = mk_add(mk_mul(mk_real(w[1], 100), f2), mk_mul(mk_real(w[0], 100), f1)); + Z3_optimize_minimize(ctx, opt, weighted); + Z3_lbool result = Z3_optimize_check(ctx, opt, 0, nullptr); + std::cout << "max_rev weighted (w1=" << w[0] << "/5, w2=" << w[1] << "/5): " + << result_str(result) << std::endl; + ENSURE(result == Z3_L_TRUE); + if (result == Z3_L_TRUE) { + Z3_model m = Z3_optimize_get_model(ctx, opt); + Z3_model_inc_ref(ctx, m); + Z3_ast v1, v2; + Z3_model_eval(ctx, m, f1, true, &v1); + Z3_model_eval(ctx, m, f2, true, &v2); + std::cout << " f1=" << Z3_ast_to_string(ctx, v1) + << " f2=" << Z3_ast_to_string(ctx, v2) << std::endl; + Z3_model_dec_ref(ctx, m); + num_sat++; + } + Z3_optimize_dec_ref(ctx, opt); + } + + std::cout << "max_rev: " << num_sat << "/7 optimizations returned sat" << std::endl; + ENSURE(num_sat == 7); + Z3_del_context(ctx); + std::cout << "max_rev optimization test done" << std::endl; +} + +void tst_max_rev() { + test_max_rev(); +} diff --git a/src/test/main.cpp b/src/test/main.cpp index f3b41f629..9f3367378 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -176,6 +176,7 @@ int main(int argc, char ** argv) { TST(simple_parser); TST(api); TST(bnh_opt); + TST(max_rev); TST(api_algebraic); TST(api_polynomial); TST(api_pb);