如何快速复制pyz3解算器

Question

我遇到了一个情况，我真的很喜欢为Z3求解器复制功能。我的意思是，我有一个用一些约束实例化的解算器。我现在想复制它，这样我就有两个独立的求解器。目前，我正在通过创建一个新的解算器来实现这一点，并在s.assertions上迭代并将它们重新添加进来。对于小规模的解决方案，这是好的。对于较大的解算器，这可能会严重影响制作副本的时间，因为Z3正在重新创建它已经完成的工作。在

虽然这不是一个显示阻止，它将是非常有益的能够直接复制求解器。普通的deepcopy方法会抛出一个错误，即不能深度复制ctypes（这是有意义的），所以我猜任何更好的解决方案都必须由z3或z3py来实现。在

有没有人知道一种更有效的方法来复制所述的解算器，而不会产生Z3重新求解它已经知道的问题的开销？在

Answer 1

如果构建Z3的最新源，则解算器对象具有一个translate方法，该方法将新上下文作为参数（可以是相同的上下文），并在该上下文中创建解算器的副本。在

s = Solver()
...add some assertions...
solver2 = s.translate(main_ctx()) # create a copy in the same context
solver3 = s.translate(ctx) # create a copy in some other context