python - 如何复制在 pysmt 中创建的求解器？

Question

在 pysmt 中，假设我创建了一个求解器并添加了许多断言。现在，我想制作求解器实例的副本，因为我需要向求解器添加不同的断言。我该怎么做？我需要这样做以提高代码的性能。

我试图做一些事情，比如 copy()、clone() 和 deepcopy()，但它们都不起作用。所以我现在的解决方法是跟踪所有断言并创建新的求解器实例并每次都从头开始构建它。

Answer 1

对于您的方案，最简单的似乎如下：

您可以使用“assertions()”方法从求解器中检索所有断言。

from z3 import *
x, y = Ints('x y')
s1 = Solver()
s1.add(x <= y)
print s1
s2 = Solver()
s2.add(s1.assertions())
print s2