我想用Z3用于通过C / C ++ API消除线性整数运算公式量词。 考虑一个简单的例子：存在（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智力）（和（<= XY）（<= Y（* 2×））））
而我想获得像
（<= 0 y）的
是否有可能与Z3得到它？ 提前谢谢了。
尼古拉已经指出，策略可以用来进行量词消去。 在这篇文章中，我想强调如何安全地混合C ++和C的API。 在Z3 C ++ API使用引用计数来管理存储器。 expr本质上是一种“智能指针”，可自动管理引用计数我们。 我在下面的帖子讨论过这个问题： 阵列选择并使用C ++ API店 。
所以，当我们调用一个C API返回一个Z3_ast，我们应该使用函数包裹的结果to_expr ， to_sort或to_func_decl 。 的签名to_expr是：
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);
}
该简化器没有任何再调用量词消去手续。 量词消除和许多其他特殊用途的简化重写提供了战术。
在C ++包装Z3 ++的.h公开用于创建策略对象的方法。 你将不得不创建一个策略对象为“乂”字诀。 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);
