如何快速复制 pyz3 求解器答案

【问题标题】：How to quick copy pyz3 solvers如何快速复制 pyz3 求解器
【发布时间】：2016-04-01 19:17:08
【问题描述】：

我遇到了一种情况，我非常喜欢 Z3 Solver 的复制功能。我的意思是，我有一个带有一些约束的求解器。我现在想复制它，以便我有两个独立求解器。目前，我正在通过创建一个新的求解器并迭代 s.assertions 并将它们重新添加来做到这一点。对于小型求解器来说，这很好。对于较大的求解器，这会严重影响制作副本的时间，因为 Z3 正在重新创建它已经完成的工作。

虽然这不是一个展示停止器，但能够直接复制求解器将非常有益。正常的 deepcopy 方法会引发一个错误，即无法对 ctypes 进行 deepcopy（这是有道理的），所以我猜想任何更好的解决方案都必须由 z3 或 z3py 来实现。

任何人都知道一种更有效的方法来复制所述求解器，并且不会产生 Z3 重新求解它已经知道的东西的开销？

【问题讨论】：

标签： python python-3.x z3 z3py

【解决方案1】：

如果您构建 Z3 的最新源，Solver 对象有一个 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

【讨论】：