时间戳

首页 > 解决方案 > C API 中的 Z3 获取值

c - C API 中的 Z3 获取值

问题描述

smtlib 提供了get-value获取特定值的功能，例如在优化一个术语之后：

(declare-const A Int)
(declare-const B Int)
(assert (> A B))
(assert (> B 10))
(assert (< A 100))
(maximize (- A B))
(check-sat)
(get-value (A B))

产量

sat
((A 99)
 (B 11))

我尝试使用 C API 执行此操作，但是我找不到任何等效的操作get-value。有没有类似的操作？如果不是，它是如何在 Z3 shell 中实现的？

编辑：我尝试了 christoph-wintersteiger 的答案，但我只得到一个null结果，即使我希望它为 A 返回 99：

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

int main()
{
    Z3_context context = Z3_mk_context(Z3_mk_config());
    Z3_optimize opt = Z3_mk_optimize(context);
    Z3_optimize_inc_ref(context, opt);
    Z3_ast a = Z3_mk_const(context, Z3_mk_string_symbol(context, "A"), Z3_mk_int_sort(context));
    Z3_ast b = Z3_mk_const(context, Z3_mk_string_symbol(context, "B"), Z3_mk_int_sort(context));
    Z3_ast args[] = {a, b};
    Z3_ast objective = Z3_mk_sub(context, 2, args);
    Z3_optimize_assert(context, opt, Z3_mk_gt(context, a, b));
    Z3_optimize_assert(context, opt, Z3_mk_gt(context, b, Z3_mk_unsigned_int64(context, 10, Z3_mk_int_sort(context))));
    Z3_optimize_assert(context, opt, Z3_mk_lt(context, a, Z3_mk_unsigned_int64(context, 100, Z3_mk_int_sort(context))));
    unsigned index = Z3_optimize_maximize(context, opt, objective);
    Z3_lbool result = Z3_optimize_check(context, opt, 0, 0);
    Z3_model model = Z3_optimize_get_model(context, opt);
    Z3_func_decl func_a = Z3_to_func_decl(context, a);
    Z3_ast a_result = Z3_model_get_const_interp (context, model, func_a);
    fprintf(stderr, "a: %s\n", Z3_ast_to_string(context, a_result));
    return 0;
}

// a: null

EDIT2：别名评论中的链接结合 christoph-wintersteigers 答案为我解决了这个问题。

标签： cz3

解决方案

在 C API 中，值是从模型对象中提取的，例如通过Z3_solver_get_model后跟Z3_model_get_const_interp来获取值（常量的解释）。

推荐阅读