2

我需要它在符号执行(Klee)的上下文中进行增量求解。在符号执行路径的分支点,有必要将求解器上下文分成两部分:具有真假条件。当然,有一个昂贵的解决方法 - 创建空上下文并重放所有约束。

有没有办法拆分 Z3_context?你打算添加这样的功能吗?

笔记

如果使用深度优先的符号探索,可以避免上下文的分裂,即探索当前的执行路径直到它到达“结束”,因此将来不会再探索这条路径。在这种情况下,弹出直到到达分支点并继续探索另一个条件分支就足够了。但是在 Klee 的情况下,许多符号路径是“同时”探索的(对真假分支的探索是交错的),因此您需要求解器上下文求解器切换(每个方法中有 Z3_context 参数)和分支(没有用于此的方法,这就是我需要的)。

谢谢!

4

2 回答 2

4

不,当前版本的 Z3 (3.2) 不支持此功能。我们意识到这是一项重要功能,下一个版本中将提供等效功能。这个想法是分离 Context 和 Solver 的概念。在下一个版本中,我们将提供用于创建(和复制)求解器的 API。因此,您将能够为搜索的每个分支使用不同的求解器。简而言之,Context 用于管理/创建 Z3 表达式,Solver 用于检查可满足性。

于 2011-10-11T15:23:02.897 回答
3

我目前用于此类事情的方法是断言像 p => A 而不是 A 之类的公式,其中 p 是一个新的布尔文字。然后在我的客户端中,我维护与每个分支对应的保护文字列表之间的关联,并使用 check_assumptions()。在我的情况下,我碰巧能够在每次搜索期间保留所有分配的公式,但 YMMV。即使对于深度优先的探索,我似乎通过这种方式获得了比使用 push/pop 更多的增量重用。

于 2011-10-12T07:31:11.520 回答