我需要它在符号执行（Klee）的上下文中进行增量求解。
在符号执行路径的分支点，有必要将求解器上下文分为两部分：条件为真和条件为假。当然，有一个昂贵的解决方法 - 创建空上下文并重播所有约束。
有没有办法分割Z3_context？您打算添加这样的功能吗？
Note
如果使用深度优先符号探索，即探索当前执行路径直到它到达“结束”，则可以避免上下文的分割，因此将来不会再探索该路径。在这种情况下就足够了pop直到到达分支点，继续探索另一个条件分支。但是在 Klee 的情况下，“同时”探索许多符号路径（对真分支和假分支的探索是交错的），因此您需要求解器上下文求解器切换（每个方法中有 Z3_context 参数）和分支（没有方法可以实现此目的，这就是我需要的）。
Thanks!
不可以，当前版本的Z3（3.2）不支持此功能。我们意识到这是一项重要的功能，并且在下一个版本中将提供等效的功能。
这个想法是将上下文和求解器的概念分开。在下一个版本中，我们将提供用于创建（和复制）求解器的 API。因此，您将能够对搜索的每个分支使用不同的求解器。简而言之，Context 用于管理/创建 Z3 表达式，Solver 用于检查可满足性。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
