Z3：在 C++ 中优化的超时答案

【问题标题】：Z3: timeout for optimize in C++Z3：在 C++ 中优化的超时
【发布时间】：2016-12-05 01:40:58
【问题描述】：

我正在尝试了解如何使用 C++ API 为 Z3 的优化类设置超时。

这是我的代码：

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

但我在 opt.set(par) 行上得到“未知参数‘超时’”异常。是否可以为优化类设置超时（超时后，我想获得找到的最佳解决方案）？

谢谢！

【问题讨论】：

你是说喜欢睡觉？或 Z3 特有的东西
"z3 minimization and timeout" 基本上是同一个问题，但使用的是 Python API。那里的用户似乎没有找到好的解决方案。对于 C++ API，在我的系统上使用 set_param("smt.timeout", 1000); 可以在 opt.check() 期间超时，但它可能仅在解决硬约束时才有效。从另一个问题看来，无论如何都不会使用这样的方法返回最佳模型。我删除了我的部分答案，所以也许 Z3 开发人员会认为这个问题没有答案。

【解决方案1】：

我知道这是一个老问题，但如果有人仍在寻找答案，您需要：

Z3_global_param_set("timeout", timeout);

你的超时时间应该是一个 C 字符串。

【讨论】：