是否可以克隆Z3_context？

Question

我需要它在符号执行的背景下进行增量求解（Klee）。 在符号执行路径的分支点上，有必要将求解器上下文分成两部分：使用true和false条件。当然，有一个昂贵的解决方法 - 创建空的上下文并重播所有约束。

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

注意上下文的

分裂可以避免如果用深度优先象征探索，直到它到达“终点”，因此该路径将不再在未来的研究是探索当前执行路径。在这种情况下，只要分支点到达并且继续探索另一个条件分支，就足够了pop。但是在Klee的情况下，许多符号路径是“同时”探索的（真正和错误分支的探索是交错的），所以你需要解算器上下文求解器切换（每个方法都有Z3_context参数）和分支（没有方法，那是我需要的）。

谢谢！

Answer 1

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

Answer 2

我目前用于这类事情的方法是声明像p => A而不是A的公式，其中p是新布尔文字。然后在我的客户端维护与每个分支对应的警卫文字列表之间的关联，并使用check_assumptions（）。在我的情况下，我碰巧能够在每次搜索时分配所有的公式，但YMMV。即使对于深度优先的探索，我似乎也比使用push/pop获得更多的增量重用。