我需要它在符号执行(Klee)的上下文中进行增量求解。在符号执行路径的分支点,有必要将求解器上下文分成两部分:具有真假条件。当然,有一个昂贵的解决方法 - 创建空上下文并重放所有约束。
有没有办法拆分 Z3_context?你打算添加这样的功能吗?
笔记
如果使用深度优先的符号探索,可以避免上下文的分裂,即探索当前的执行路径直到它到达“结束”,因此将来不会再探索这条路径。在这种情况下,弹出直到到达分支点并继续探索另一个条件分支就足够了。但是在 Klee 的情况下,许多符号路径是“同时”探索的(对真假分支的探索是交错的),因此您需要求解器上下文求解器切换(每个方法中有 Z3_context 参数)和分支(没有用于此的方法,这就是我需要的)。
谢谢!