是否可以克隆Z3_context？

Question

我需要它在符號執行的背景下進行增量求解（Klee）。 在符號執行路徑的分支點上，有必要將求解器上下文分成兩部分：使用true和false條件。當然，有一個昂貴的解決方法 - 創建空的上下文並重播所有約束。

有沒有辦法拆分Z3_context？你打算添加這樣的功能嗎？

注意上下文的

分裂可以避免如果用深度優先象徵探索，直到它到達「終點」，因此該路徑將不再在未來的研究是探索當前執行路徑。在這種情況下，只要分支點到達並且繼續探索另一個條件分支，就足夠了pop。但是在Klee的情況下，許多符號路徑是「同時」探索的（真正和錯誤分支的探索是交錯的），所以你需要解算器上下文求解器切換（每個方法都有Z3_context參數）和分支（沒有方法，那是我需要的）。

謝謝！

Answer 1

不，當前版本的Z3（3.2）不支持此功能。我們認識到這是一項重要的功能，下一版本將提供相應的功能。 這個想法是分離上下文和求解器的概念。在下一個版本中，我們將有用於創建（和複製）求解器的API。因此，您將能夠爲搜索的每個分支使用不同的求解器。簡而言之，Context用於管理/創建Z3表達式，Solver用於檢查可滿足性。

Answer 2

我目前用於這類事情的方法是聲明像p => A而不是A的公式，其中p是新布爾文字。然後在我的客戶端維護與每個分支對應的警衛文字列表之間的關聯，並使用check_assumptions（）。在我的情況下，我碰巧能夠在每次搜索時分配所有的公式，但YMMV。即使對於深度優先的探索，我似乎也比使用push/pop獲得更多的增量重用。