Z3Opt：在時間範圍內尋找次優模型？

Question

Z3Opt是否具有在用戶指定的時間範圍內爲目標提供次優解決方案的功能？

Answer 1

您可以設置超時或中斷opt環境。然後，您可以查詢選擇上下文的目標值的上限和下限。您也可以查詢當前模型，它會返回模型以達到目前爲止的最佳綁定。