z3 - 是否可以克隆 Z3_context？

Question

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

有没有办法拆分 Z3_context？您打算添加此类功能吗？

注意

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

谢谢!

Answer 1

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