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

Question

我想使用 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) (and (

而我想获得类似的东西

（

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

Answer 2

简化器不再调用量词消除过程。量词消除和许多其他特殊目的的简化重写可通过策略获得。

C++ 包装器 z3++.h 公开了创建策略对象的方法。 您必须为“qe”策略创建一个策略对象。 Z3 发行版附带了几个示例，用于使用 z3++.h API 中的策略。 例如：

void tactic_example1() {
/*
  Z3 implements a methodology for orchestrating reasoning engines where "big" symbolic
  reasoning steps are represented as functions known as tactics, and tactics are composed
  using combinators known as tacticals. Tactics process sets of formulas called Goals.

  When a tactic is applied to some goal G, four different outcomes are possible. The tactic succeeds
  in showing G to be satisfiable (i.e., feasible); succeeds in showing G to be unsatisfiable (i.e., infeasible); 
  produces a sequence of subgoals; or fails. When reducing a goal G to a sequence of subgoals G1, ..., Gn, 
  we face the problem of model conversion. A model converter construct a model for G using a model for some subgoal Gi.

  In this example, we create a goal g consisting of three formulas, and a tactic t composed of two built-in tactics: 
  simplify and solve-eqs. The tactic simplify apply transformations equivalent to the ones found in the command simplify. 
  The tactic solver-eqs eliminate variables using Gaussian elimination. Actually, solve-eqs is not restricted 
  only to linear arithmetic. It can also eliminate arbitrary variables. 
  Then, sequential composition combinator & applies simplify to the input goal and solve-eqs to each subgoal produced by simplify. 
  In this example, only one subgoal is produced.
*/
std::cout << "tactic example 1\n";
context c;
expr x = c.real_const("x");
expr y = c.real_const("y");
goal g(c);
g.add(x > 0);
g.add(y > 0);
g.add(x == y + 2);
std::cout << g << "\n";
tactic t1(c, "simplify");
tactic t2(c, "solve-eqs");
tactic t = t1 & t2;
apply_result r = t(g);
std::cout << r << "\n";

}

在你的情况下，你会想要一些类似的东西：

context ctx;
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 :(
tactic qe(ctx, "qe");
goal g(ctx);
g.add(qf);
cout << qe.apply(g);