我需要它在符号执行（Klee）的上下文中进行增量求解。在符号执行路径的分支点，有必要将求解器上下文分成两部分：具有真假条件。当然，有一个昂贵的解决方法 - 创建空上下文并重放所有约束。
有没有办法拆分 Z3_context？你打算添加这样的功能吗？
笔记
如果使用深度优先的符号探索，可以避免上下文的分裂，即探索当前的执行路径直到它到达“结束”，因此将来不会再探索这条路径。在这种情况下，弹出直到到达分支点并继续探索另一个条件分支就足够了。但是在 Klee 的情况下，许多符号路径是“同时”探索的（对真假分支的探索是交错的），因此您需要求解器上下文求解器切换（每个方法中有 Z3_context 参数）和分支（没有用于此的方法，这就是我需要的）。
谢谢！
不，当前版本的 Z3 (3.2) 不支持此功能。我们意识到这是一项重要功能，下一个版本中将提供等效功能。这个想法是分离 Context 和 Solver 的概念。在下一个版本中，我们将提供用于创建（和复制）求解器的 API。因此，您将能够为搜索的每个分支使用不同的求解器。简而言之，Context 用于管理/创建 Z3 表达式，Solver 用于检查可满足性。
我目前用于此类事情的方法是断言像 p => A 而不是 A 之类的公式，其中 p 是一个新的布尔文字。然后在我的客户端中，我维护与每个分支对应的保护文字列表之间的关联，并使用 check_assumptions()。在我的情况下，我碰巧能够在每次搜索期间保留所有分配的公式，但 YMMV。即使对于深度优先的探索，我似乎通过这种方式获得了比使用 push/pop 更多的增量重用。