Z3get-valueinCAPI

Z3 C API中的get-value函数用于获取求解器中所有变量的具体解值。其具体用法如下：

void Z3_API Z3_solver_get_model(__in Z3_context c, __in Z3_solver s, __out Z3_model * m);

其中，c是上下文环境，s是求解器，m是用于输出得到的模型。

示例代码如下：

// 创建上下文环境
Z3_context ctx = mk_context();

// 创建求解器
Z3_solver solver = Z3_mk_solver(ctx);

// 往求解器中添加约束
Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), Z3_mk_int_sort(ctx));
Z3_ast y = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "y"), Z3_mk_int_sort(ctx));
Z3_ast c1 = Z3_mk_gt(ctx, x, Z3_mk_int(ctx, 10, Z3_mk_int_sort(ctx)));
Z3_ast c2 = Z3_mk_lt(ctx, y, Z3_mk_int(ctx, 20, Z3_mk_int_sort(ctx)));
Z3_solver_assert(ctx, solver, c1);
Z3_solver_assert(ctx, solver, c2);

// 检查约束是否可满足
Z3_lbool result = Z3_solver_check(ctx, solver);

if (result == Z3_L_TRUE)
{
    // 获取求解器中所有变量的具体解值
    Z3_model model = NULL;
    Z3_solver_get_model(ctx, solver, &model);

    // 获取变量x的具体值
    Z3_ast x_value = NULL;
    Z3_model_eval(ctx, model, x, true, &x_value);
    printf("x = %s\n", Z3_get_numeral_string(ctx, x_value));

    // 获取变量y的具体值
    Z3_ast y_value = NULL;
    Z3_model_eval(ctx, model, y, true, &y_value);
    printf("y = %s\n", Z3_get_numeral_string(ctx, y_value));
}
else if (