通过 C/C++ API 对 Z3 中的 LIA 进行量词消除

我想使用 Z3 通过 C/C++ API 消除线性整数算术公式中的量词。考虑一个简单的例子：Exists (x) ( x = 0。

我尝试这样做：

   context ctx;
   ctx.set("ELIM_QUANTIFIERS", "true");
   expr x = ctx.int_const("x"); 
   expr y = ctx.int_const("y"); 
   expr sub_expr = (x <= y)  && (y <= 2*x);

   Z3_ast qf = Z3_mk_exists_const(ctx, 0, 1, (Z3_app[]) {x}, 
                                  0, {}, // patterns don't seem to make sense here.
                                  sub_expr); //No C++ API for quantifiers :(
   qf = Z3_simplify(ctx, qf);
   cout << Z3_ast_to_string(ctx, qf);

我得到的是

（存在（（x Int）（并且（

而我想获得类似的东西

(

Z3有可能获得吗？ 提前谢谢了。

Nikolaj 已经指出可以使用策略来执行量词消除。在这篇文章中，我想强调如何安全地混合 C++ 和 C API。 Z3 C++ API 使用引用计数来管理内存。expr本质上是一个“智能指针”，它自动为我们管理引用计数器。我在以下帖子中讨论了这个问题：使用 C++ API 进行数组选择和存储 https://stackoverflow.com/questions/12995317/array-select-and-store-using-the-c-api.

因此，当我们调用返回 Z3_ast 的 C API 时，我们应该使用函数包装结果to_expr, to_sort or to_func_decl。的签名to_expr is:

inline expr to_expr(context & c, Z3_ast a);

通过使用此函数，我们可以避免内存泄漏和崩溃（当访问已被 Z3 垃圾收集的对象时）。这是使用的完整示例to_expr()。您可以通过复制此函​​数来测试它example.cpp文件在c++Z3 发行版中的文件夹。

void tst_quantifier() {
    context ctx;
    expr x = ctx.int_const("x"); 
    expr y = ctx.int_const("y"); 
    expr sub_expr = (x <= y) && (y <= 2*x);
    Z3_app vars[] = {(Z3_app) x};

    expr qf = to_expr(ctx, Z3_mk_exists_const(ctx, 0, 1, vars,
                                              0, 0, // patterns don't seem to make sense here.
                                              sub_expr)); //No C++ API for quantifiers :(
    tactic qe(ctx, "qe");
    goal g(ctx);
    g.add(qf);
    std::cout << qe.apply(g);
}