用C/C++ API消除Z3中的LIA
我想使用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) (<= y (* 2x)
而我想要得到这样的东西
(<= 0 y)
有可能通过Z3获得它吗？在此之前，非常感谢您。
回答 2
Stack Overflow用户
发布于 2012-10-26 03:34:56
Nikolaj已经指出，战术可以用来消除量词。在这篇文章中，我想强调如何安全地混合C++和APIs。Z3 C++ API使用引用计数来管理内存。expr本质上是一个“智能指针”，它自动为我们管理引用计数器。我在以下文章中讨论了这个问题：Array select and store using the C++ API。
因此，当我们调用返回Z3_ast的wrap时，我们应该使用函数to_expr、to_sort或to_func_decl包装结果。to_expr的签名是：
inline expr to_expr(context & c, Z3_ast a);通过使用此函数，我们可以避免内存泄漏和崩溃(当访问Z3收集的垃圾对象时)。下面是使用to_expr()的完整示例。您可以通过在example.cpp发行版的c++文件夹中的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);
}Stack Overflow用户
发布于 2012-10-26 00:21:21
简化器不再调用量词消除过程。量化词的消除和许多其他特殊目的的简化重写是可用的战术。
C++包装器z3++.h公开用于创建策略对象的方法。你必须为“量化宽松”策略创建一个战术目标。THe 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);https://stackoverflow.com/questions/13072081
复制相似问题
腾讯云开发者
