通过C/C ++ API在Z3中消除LIA的量化器 [英] Quantifier Elimination for LIA in Z3 via C/C++ API

问题描述

我想使用Z3通过C/C ++ API消除线性整数算术公式中的量词.考虑一个简单的例子:存在(x)(x< = y& y< = 2 * x).无量词 相同模型的公式为y> = 0.

I would like to use Z3 for eliminating quantifiers in linear integer arithmetic formulas via C/C++ API. Consider a simple example: Exists (x) ( x <= y & y <= 2*x). A quantifier-free formula with the same models is 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);

我得到的是

(存在((x Int)(和(< = x y)(< = y(* 2 x))))

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

而我想获得类似

(< = 0 y)

(<= 0 y)

Z3是否有可能得到它? 提前谢谢了.

Is there a possibility to get it with Z3? Many thanks in advance.

推荐答案

尼古拉(Nikolaj)已经指出，战术可用于执行量词消除.在本文中，我想强调一下如何安全地混合使用C ++和C API. Z3 C ++ API使用引用计数来管理内存. expr本质上是一个智能指针"，可为我们自动管理参考计数器.我在以下文章中讨论了此问题:使用C ++进行数组选择和存储API .

Nikolaj already pointed out that tactics can be used to perform quantifier elimination. In this post, I'd like to emphasize how to safely mix the C++ and C APIs. The Z3 C++ API uses reference counting to manage the memory. expr is essentially a "smart-pointer" that manages the reference counters automatically for us. I discussed this issue in the following post: Array select and store using the C++ API.

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

So, when we invoke a C API that returns a Z3_ast, we should wrap the result using the functions to_expr, to_sort or to_func_decl. The signature of to_expr is:

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

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

By using this function, we avoid memory leaks, and crashes (when accessing objects that have been garbage collected by Z3). Here is the complete example using to_expr(). You can test it by copying this function in the example.cpp file in the c++ folder in the Z3 distribution.

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

这篇关于通过C/C ++ API在Z3中消除LIA的量化器的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！