我可以在Z3中創建一個新的解算器嗎？

我可以在Z3中創建一個新的求解器嗎？在Z3中，創建解算器的標準過程如下所示：我可以在Z3中創建一個新的解算器嗎？

context ctx; solver sv（ctx）;

經過插入斷言和檢查的過程之後，我想要創建一個新的求解器，比如說sv2，它相當於sv。但我找不到支持功能或API。解決費用昂貴，這是我不想從頭開始創建sv2的方式。

陳婷

2015-10-05 Ting Chen

你是什麼意思的「等值」？您可以根據需要創建儘可能多的解算器，但不會包含第一個解析器的斷言。你當然可以將它們複製到新的求解器中，但我看不出如何使任何更便宜的東西。 –

是的，就像你說的那樣，將舊解算器中的所有斷言複製到新解釋器並不會使任何便宜。我相信通過這種方式，我必須解決我在舊解算器中已經解決的問題。那麼有沒有便宜的方法。我的意思是從一箇舊的求解器中創建一個新求解器，同時保持其狀態，從而逐步解決問題。 –

這樣做，可以通過多種方法推/拉或下假設（都在同一求解器和上下文）來解決，看Soft/Hard constraints in Z3，Z3/SMT: When should I prefer push/pop to reset?的常用方式。另外，搜索這些關鍵詞，關於這個問題還有很多問題和答案。

2015-10-05 12:47:49

回答