有没有办法简化路径条件

发布于 2024-12-17 07:48:08 字数 251 浏览 2 评论 0原文

例如，在下面的代码中，路径条件将为 x>0 && x+1>0。但由于 x>0 意味着 x+1>0，z3 或 pex API 有没有办法只获取 x>0 而不是两个都。

if(x>0)
 if(x+1>0)
   //get path condition.

谢谢

原文

For example, in the code below the path condition will be x>0 && x+1>0. But since x>0 implies x+1>0, is there any way in z3 or pex API to get only x>0 and not both.

if(x>0)
 if(x+1>0)
   //get path condition.

Thanks

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

最单纯的乌龟 2024-12-24 07:48:08

使用 Z3 API，您可以通过断言 A 且 not B 来检查 A 是否蕴含 B (Z3_assert_cnstr函数）；并检查结果是否不可满足（Z3_check 函数）。一个简单的想法是在 Z3 上下文中继续断言路径条件。在断言 A 之前，您需要检查上下文是否暗示了它。您可以使用以下 C 代码来完成此操作。

Z3_push(ctx); // create a backtracking point
Z3_assert_cnstr(ctx, Z3_mk_not(ctx, A));
Z3_lbool r = Z3_check(ctx);
Z3_pop(ctx);  // remove backtracking point and 'not A' from the context
if (r != Z3_L_FALSE) 
   Z3_assert_cnstr(ctx, A); // assert A only if it is not implied.

Z3 3.2 有一些语言用于指定求解和简化表达式的策略。
在这种语言上，您可以编写：

(declare-const x Int)
(assert (> x 0))
(assert (> (+ x 1) 0))
(apply (and-then simplify propagate-bounds))

这个简单的策略将按预期生成 (>= x 1) 。它基于更便宜（但不完整）的方法。
另一个问题是此功能仅在交互式 shell 中可用。
计划在下一版本的编程 API 中提供这些功能。

With the Z3 API, you can check whether A implies B by asserting A and not B (Z3_assert_cnstr function); and checking whether the result is unsatisfiable or not (Z3_check function). One simple idea is to keep asserting the path conditions in a Z3 context. Before asserting A, you check whether it is implied by the context or not. You can accomplish that using the following piece C of code.

Z3_push(ctx); // create a backtracking point
Z3_assert_cnstr(ctx, Z3_mk_not(ctx, A));
Z3_lbool r = Z3_check(ctx);
Z3_pop(ctx);  // remove backtracking point and 'not A' from the context
if (r != Z3_L_FALSE) 
   Z3_assert_cnstr(ctx, A); // assert A only if it is not implied.

Z3 3.2 has a little language for specifying strategies for solving and simplifying expressions.
On this language, you can write:

(declare-const x Int)
(assert (> x 0))
(assert (> (+ x 1) 0))
(apply (and-then simplify propagate-bounds))

This simple strategy will produce (>= x 1) as expected. It is based on much cheaper (but incomplete) methods.
Another problem is that this functionality is only available in the interactive shell.
The plan is to have these capabilities available in the programmatic API in the next release.

回复收藏 0 原文

~没有更多了~