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

Add max_rev test: BNH with reversed argument order in f1/f2

Browse source 
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>
This commit is contained in:
Lev Nachmanson 2026-03-11 18:15:57 -10:00
parent 274d64299e
commit ce7c7f458e
2 changed files with 110 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

109
src/test/api.cpp
View file

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

1
src/test/main.cpp
View file

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