3

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

我得到的是

(存在 ((x Int) (and (<= xy) (<= y (* 2 x))))

而我想获得类似的东西

(<= 0 年)

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

4

2 回答 2

4

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 发行版文件夹中的example.cpp文件中来测试它。c++

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);
}
于 2012-10-26T03:34:56.373 回答
3

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

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);
于 2012-10-26T00:21:21.820 回答