Z3 在 C 中获取值 API

Question

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:

的结果为 return 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

编辑2：别名评论中的 link 结合 christoph-wintersteigers 的回答为我解决了这个问题。

Answer 1

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

Answer 2

z3 C API 非常低级，很难导航。最好的办法是研究 https://github.com/Z3Prover/z3/blob/master/examples/c/test_capi.c#L630-L654，以及它为完整解决方案调用的所有函数。

但是，如果您只想显示整数值的简单元素，则可以使用一些最少的代码。这是您使用简单整数值打印机的示例：

注意。正如@Christoph 评论的那样，下面的代码只是对 OP 代码的修改，以添加整数值的模型提取。它可能需要更好地管理引用计数，所以要小心！

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

void disp_int(Z3_context c, Z3_model m, const char *n, Z3_ast a)
{
   Z3_ast v = a;
   Z3_model_eval(c, m, a, 1, &v);
   printf("%s = %s\n", n, Z3_get_numeral_string(c, v));
}

int main()
{
    <YOUR CODE ABOVE; elided for clarity>

    disp_int(context, model, "a", a);
    disp_int(context, model, "b", b);

    return 0;
}

把它放在一个名为a.c的文件中，然后像这样编译它：

gcc a.c -o a -lz3

现在您可以：

$ ./a
a = 99
b = 11

这就是我相信您正在寻找的东西。但同样，要使这项工作适用于任意排序的值，您必须研究原始代码并进行更深入的分析。（这也是为什么大多数人使用更高级别的 API 的原因，例如来自 Python/Haskell/Scala 等的那些，这避免了大多数这些复杂性。）

Z3 在 C 中获取值 API

Z3 get-value in C API

c

z3