是否可以克隆 Z3_context？

Question

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

有没有办法拆分 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 更多的增量重用。