From 3176151cc2a3aa3bed452212eea9c25e96469c25 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 11 Mar 2026 19:18:45 -1000 Subject: [PATCH] rename bhn_opt to max_reg Signed-off-by: Lev Nachmanson --- src/test/api.cpp | 24 ++++++++++++------------ src/test/main.cpp | 2 +- 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/test/api.cpp b/src/test/api.cpp index 671913591..27e881fe9 100644 --- a/src/test/api.cpp +++ b/src/test/api.cpp @@ -160,7 +160,7 @@ void test_optimize_translate() { Z3_del_context(ctx1); } -void test_bnh_optimize() { +void test_max_reg() { // BNH multi-objective optimization problem using Z3 Optimize C API. // Mimics /tmp/bnh_z3.py: two objectives over a constrained 2D domain. // f1 = 4*x1^2 + 4*x2^2 @@ -189,7 +189,7 @@ void test_bnh_optimize() { Z3_ast f2 = mk_add(mk_sq(mk_sub(x1, mk_real(5))), mk_sq(mk_sub(x2, mk_real(5)))); // Helper: create optimize with BNH constraints and timeout - auto mk_bnh_opt = [&]() -> Z3_optimize { + auto mk_max_reg = [&]() -> Z3_optimize { Z3_optimize opt = Z3_mk_optimize(ctx); Z3_optimize_inc_ref(ctx, opt); // Set timeout to 5 seconds @@ -214,7 +214,7 @@ void test_bnh_optimize() { // Approach 1: Minimize f1 (Python: opt.minimize(f1)) { - Z3_optimize opt = mk_bnh_opt(); + Z3_optimize opt = mk_max_reg(); Z3_optimize_minimize(ctx, opt, f1); Z3_lbool result = Z3_optimize_check(ctx, opt, 0, nullptr); std::cout << "BNH min f1: " << result_str(result) << std::endl; @@ -232,7 +232,7 @@ void test_bnh_optimize() { // Approach 2: Minimize f2 (Python: opt2.minimize(f2)) { - Z3_optimize opt = mk_bnh_opt(); + Z3_optimize opt = mk_max_reg(); Z3_optimize_minimize(ctx, opt, f2); Z3_lbool result = Z3_optimize_check(ctx, opt, 0, nullptr); std::cout << "BNH min f2: " << result_str(result) << std::endl; @@ -251,7 +251,7 @@ void test_bnh_optimize() { // Approach 3: Weighted sum method (Python loop over weights) int weights[][2] = {{1, 4}, {2, 3}, {1, 1}, {3, 2}, {4, 1}}; for (auto& w : weights) { - Z3_optimize opt = mk_bnh_opt(); + Z3_optimize opt = mk_max_reg(); Z3_ast weighted = mk_add(mk_mul(mk_real(w[0], 100), f1), mk_mul(mk_real(w[1], 100), f2)); Z3_optimize_minimize(ctx, opt, weighted); Z3_lbool result = Z3_optimize_check(ctx, opt, 0, nullptr); @@ -285,12 +285,12 @@ void tst_api() { test_optimize_translate(); } -void tst_bnh_opt() { - test_bnh_optimize(); +void tst_max_reg() { + test_max_reg(); } void test_max_rev() { - // Same as test_bnh_optimize but with reversed argument order in f1/f2 construction. + // Same as test_max_regimize 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); @@ -310,7 +310,7 @@ void test_max_rev() { // 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 { + auto mk_max_reg = [&]() -> Z3_optimize { Z3_optimize opt = Z3_mk_optimize(ctx); Z3_optimize_inc_ref(ctx, opt); Z3_params p = Z3_mk_params(ctx); @@ -332,7 +332,7 @@ void test_max_rev() { unsigned num_sat = 0; { - Z3_optimize opt = mk_bnh_opt(); + Z3_optimize opt = mk_max_reg(); 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; @@ -349,7 +349,7 @@ void test_max_rev() { } { - Z3_optimize opt = mk_bnh_opt(); + Z3_optimize opt = mk_max_reg(); 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; @@ -367,7 +367,7 @@ void test_max_rev() { int weights[][2] = {{1, 4}, {2, 3}, {1, 1}, {3, 2}, {4, 1}}; for (auto& w : weights) { - Z3_optimize opt = mk_bnh_opt(); + Z3_optimize opt = mk_max_reg(); 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); diff --git a/src/test/main.cpp b/src/test/main.cpp index 9f3367378..a8444dc14 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -175,7 +175,7 @@ int main(int argc, char ** argv) { TST(var_subst); TST(simple_parser); TST(api); - TST(bnh_opt); + TST(max_reg); TST(max_rev); TST(api_algebraic); TST(api_polynomial);