z3 - 通过 C/C++ API 在 Z3 中消除 LIA 的量词

Question

我想使用 Z3 通过 C/C++ API 消除线性整数算术公式中的量词。考虑一个简单的例子:Exists (x) ( x <= y & y <= 2*x)。无量词 同模型的公式是y >= 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);

我得到的是

(exists ((x Int) (and (<= x y) (<= y (* 2 x))))

而我想获得类似的东西

(<= 0 y)

有没有可能用Z3得到它？提前谢谢了。

Answer 1

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

因此，当我们调用返回 Z3_ast 的 C API 时，我们应该使用函数 to_expr、to_sort 或 to_func_decl 包装结果. to_expr 的签名是:

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

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

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);
}