mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-15 17:49:59 +00:00
Code Activity

rename bhn_opt to max_reg

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-03-11 19:18:45 -10:00
parent b8d6952e9e
commit 3176151cc2
2 changed files with 13 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/test/api.cpp
View file

@ -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);

2
src/test/main.cpp
View file

@ -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);