如何通过Z3 C-API获取优化目标的实际求解值？

使用Z3 4.8.9的C-API做优化求解时，调用Z3_optimize_get_objectives仅返回目标表达式（如(- x)），无法直接拿到变量的最优赋值。这是因为该API返回的是优化目标的定义项，而非求解后的数值结果，需要从求解得到的模型中提取变量的实际值。

解决步骤 #

1. 调用Z3_optimize_check确认求解状态为可满足（返回Z3_L_TRUE）
2. 通过Z3_optimize_get_model获取最优解对应的模型
3. 从模型中查询目标变量的赋值，而非直接解析Z3_optimize_get_objectives的返回结果

对应场景的完整C代码示例 #

#include <z3.h>
#include <stdio.h>

int main() {
    // 初始化Z3上下文和优化器
    Z3_config cfg = Z3_mk_config();
    Z3_context ctx = Z3_mk_context(cfg);
    Z3_optimize opt = Z3_mk_optimize(ctx);
    Z3_del_config(cfg);

    // 创建整数变量x、y
    Z3_sort int_sort = Z3_mk_int_sort(ctx);
    Z3_symbol x_sym = Z3_mk_string_symbol(ctx, "x");
    Z3_symbol y_sym = Z3_mk_string_symbol(ctx, "y");
    Z3_ast x = Z3_mk_const(ctx, x_sym, int_sort);
    Z3_ast y = Z3_mk_const(ctx, y_sym, int_sort);

    // 添加变量域约束：-1000 < x < 1000，-1000 < y < 1000
    Z3_ast x_low = Z3_mk_int(ctx, -1000, int_sort);
    Z3_ast x_high = Z3_mk_int(ctx, 1000, int_sort);
    Z3_ast y_low = Z3_mk_int(ctx, -1000, int_sort);
    Z3_ast y_high = Z3_mk_int(ctx, 1000, int_sort);
    Z3_ast x_bound = Z3_mk_and(ctx, 2, (Z3_ast[]){Z3_mk_lt(ctx, x_low, x), Z3_mk_lt(ctx, x, x_high)});
    Z3_ast y_bound = Z3_mk_and(ctx, 2, (Z3_ast[]){Z3_mk_lt(ctx, y_low, y), Z3_mk_lt(ctx, y, y_high)});
    Z3_optimize_assert(opt, x_bound);
    Z3_optimize_assert(opt, y_bound);

    // 添加核心公式约束：x == 3 || (x > y) && (y == 10)
    Z3_ast eq_x3 = Z3_mk_eq(ctx, x, Z3_mk_int(ctx, 3, int_sort));
    Z3_ast gt_xy = Z3_mk_gt(ctx, x, y);
    Z3_ast eq_y10 = Z3_mk_eq(ctx, y, Z3_mk_int(ctx, 10, int_sort));
    Z3_ast conj = Z3_mk_and(ctx, 2, (Z3_ast[]){gt_xy, eq_y10});
    Z3_ast core_formula = Z3_mk_or(ctx, 2, (Z3_ast[]){eq_x3, conj});
    Z3_optimize_assert(opt, core_formula);

    // 添加字典序优化目标：先最小化x，再最小化y
    Z3_optimize_minimize(opt, x);
    Z3_optimize_minimize(opt, y);

    // 求解优化问题
    Z3_lbool result = Z3_optimize_check(opt);
    if (result != Z3_L_TRUE) {
        printf("问题不可满足\n");
        Z3_del_context(ctx);
        return 1;
    }

    // 获取最优解模型
    Z3_model model = Z3_optimize_get_model(ctx, opt);
    if (!model) {
        printf("无法获取模型\n");
        Z3_del_context(ctx);
        return 1;
    }

    // 从模型中提取x和y的实际值
    int x_val, y_val;
    Z3_ast x_interp = Z3_model_get_const_interp(ctx, model, x);
    Z3_ast y_interp = Z3_model_get_const_interp(ctx, model, y);
    if (Z3_get_numeral_int(ctx, x_interp, &x_val) && Z3_get_numeral_int(ctx, y_interp, &y_val)) {
        printf("最优解：x = %d, y = %d\n", x_val, y_val);
    } else {
        printf("无法解析变量数值\n");
    }

    // 释放资源
    Z3_del_model(ctx, model);
    Z3_del_optimize(ctx, opt);
    Z3_del_context(ctx);
    return 0;
}

补充说明 #

• Z3_optimize_get_objectives的作用是返回你添加的优化目标定义（比如最小化x对应内部表达式(-x)），并非求解后的数值。要拿到实际值必须从模型中提取。
• 如果目标是复杂表达式（而非单一变量），可以用Z3_model_eval在模型上计算该表达式的数值结果。
• 编译时需要链接Z3库，例如：gcc -o z3_opt z3_opt.c -lz3

内容的提问来源于stack exchange，提问作者Jouke Stoel