複製一個Z3Context

Question

我需要能夠複製一個Z3Context實例，以便能夠向一個實例添加新的定義而不會影響另一個實例。

這可能嗎？

我應該看看API的哪一部分？

我提到我在使用Java API。

謝謝

Answer 1

沒有克隆上下文的方法。使用起來也有點難：在克隆一個上下文後，在新的上下文中，對應於術語和公式的指針會是什麼？相反，有各種翻譯方法可讓您在上下文之間導入術語，公式，求解器和目標。例如，使用

 Z3_ast Z3_API Z3_translate(Z3_context source, Z3_ast a, Z3_context target); 

在兩個上下文之間複製一個術語/公式。 The

 Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target); 

方法讓你克隆求解器。您可以在兩個不同的上下文或同一個上下文之間克隆求解器，特別是如果您只是使用克隆來探索不同的斷言變體。