是否可以克隆 Z3_context? [英] Is it possible to clone Z3_context?

问题描述

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

I need it for incremental solving in the context of symbolic execution (Klee). In points of branching of symbolic execution paths it is necessary to split solver context into 2 parts: with true and false conditions. Of course, there is an expensive workaround - create empty context and replay all constraints.

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

注意

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

splitting of context can be avoided if use depth-first symbolic exploration, that is exploring current execution path until it reaches "end" and hence this path won't be explored anymore in future. In this case it is enough to pop until branch point reached and continue to explore another condition branch. But in case of Klee many symbolic paths are explored "simultaneously" (exploration of true and false branches is interleaved), so you need solver context solver switching (there is Z3_context argument in each method) and branching (there are no methods for this, that is what I need).

谢谢！

推荐答案

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

No, the current version of Z3 (3.2) does not support this feature. We realize this is an important capability, and an equivalent feature will be available in the next release. The idea is to separate the concepts of Context and Solver. In the next release, we will have APIs for creating (and copying) solvers. So, you will be able to use a different solver for each branch of the search. In a nutshell, the Context is used to manage/create Z3 expressions, and the Solver for checking satisfiability.

这篇关于是否可以克隆 Z3_context?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！