如何複製在pysmt創造了一個求解？

Question

在pysmt，假設我已經創建了一個解算器和增加了許多斷言。現在，我想製作解算器實例的副本，因爲我需要向解算器添加不同的斷言。我該怎麼做？我需要這樣做才能提高代碼的性能。

我試圖做這樣的事情副本（），克隆（）和deepcopy的（），但他們都沒有工作。所以我目前的解決方法是現在跟蹤所有的斷言，創造新的求解器的實例，並從頭開始每次建立起來。

Answer 1

對於您的情況，最簡單的似乎是如下：

您可以檢索使用「斷言（）」方法從求解器的所有斷言。

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