z3py：在求解器上應用策略

Question

我需要一個解算器來支持push和pop的特定邏輯。所以我使用SolverFor()函數生成一個。由於一些斷言只是不斷斷言，如a == 2，我想在使用propagate-values策略之前簡化solver.check()。所以我的問題是：

有沒有辦法在求解器上應用策略？

我知道我可以做到這一點Goal。但在我看來，Goal不支持push和pop。

任何意見表示讚賞。謝謝。

Answer 1

戰術對象只支持非增量式求解。他們也不提供push和pop方法。它們主要用於解決非平凡的問題。爲了方便起見，我們提供了一個將策略對象包裝爲解算器對象的API。包裝是非常基本的，包裝對象保持一堆斷言，每個check是從頭開始使用包裝戰術。

Z3中的默認Solver對象是通用求解器。默認情況下，它執行不斷的傳播。我們可以控制這個求解器設置參數的行爲。在將來的版本中，我們將爲解算器對象提供附加控制。我們將能夠使用可用策略的一個子集來定製解算器對象。

這就是說，你是正確的，Goal對象不支持push和pop。 在內部，Goal對象支持在恆定時間運行的複製操作。內部使用共享數據結構來節省內存。我將在未來的版本中明確公開此功能。請注意，此功能只是節省空間/內存。解決每個目標的努力不會被保存。 我說：「明確地揭露」，因爲該功能可以與下面的技巧來模擬：

def copy_goal(g): 
    return Tactic('skip')(g)[0] 

x = Int('x') 
g = Goal() 
g.add(x < 10) 
g.add(x > 0) 
g1 = copy_goal(g) 
g1.add(x != 5) 
print g 
print g1 

上面的例子，請訪問：http://rise4fun.com/Z3Py/O3RO

備註：戰術smt實現了通用求解器我上面提到的。