Z3：在C++中優化超時

我想了解如何使用C++ API爲Z3優化類設置超時。Z3：在C++中優化超時

這我我的代碼：

context c; 
optimize opt(c); 
z3::params par(c); 
par.set("timeout", 1000); 
opt.set(par);

，但我得到「未知參數 '超時'」異常就行了opt.set（PAR）。是否可以設置優化類的超時時間（超時後，我想獲得找到的最佳解決方案）？

謝謝！

來源

2016-07-30 Daniele Ferone

你的意思是睡眠？或特定的Z3 – Charlie

[「z3最小化和超時」]（https://stackoverflow.com/questions/35203432/z3-minimization-and-timeout）基本上是相同的問題，但使用Python API。那裏的用戶似乎沒有找到一個好的解決方案。對於C++ API，使用'set_param（「smt.timeout」，1000）;'在opt.check（）'期間在我的系統上工作以超時，但也許它只在解決嚴格約束時才起作用。從另一個問題來看，似乎無論如何都不會使用這種方法來返回最優模型。我刪除了我的部分答案，所以也許Z3開發者會將這個問題視爲未答覆。 –

我知道這是一個老問題，但如果有人仍然在尋找一個答案，你需要：

Z3_global_param_set（「超時」，超時）;

而你的超時應該以C字符串的形式給出。

來源

2017-03-23 10:30:20

Z3：在C++中優化超時

回答

相關問題