复制一个 Z3Context

Duplicate a Z3Context

我需要能够复制一个 Z3Context 实例，以便能够在不影响另一个实例的情况下向一个实例添加新定义。

这可能吗？

我应该看 API 的哪一部分？

我提到我正在使用 Java API。

谢谢

没有克隆上下文的方法。使用起来也会有些困难：克隆上下文后，新上下文中的术语和公式对应的指针是什么？相反，有多种翻译方法可以让您在上下文之间导入术语、公式、求解器和目标。例如，使用

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

在两个上下文之间复制一个term/formula。 

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

方法可让您克隆求解器。您可以在两个不同的上下文或相同的上下文之间克隆求解器，特别是如果您只是使用克隆来探索断言的不同变体。