带求解器的 Z3 超时

【问题标题】：Z3 Timeout with Solver带求解器的 Z3 超时
【发布时间】：2012-06-01 17:14:29
【问题描述】：

我有一个简单的问题。如何使用以下 API 确定求解器是否超时 -

Z3_lbool Z3_API Z3_solver_check (Z3_context c, Z3_solver s )

因为 Z3_lbool 只是 true、false 或未定义。

【问题讨论】：

标签： z3

【解决方案1】：

您可以使用 API Z3_string Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s)。如果您使用 C++，对象求解器提供方法std::string reason_unknown()。这是一个使用它的小例子：

context c;
expr x = c.real_const("x");
expr y = c.real_const("y");
solver s(c);

s.add(x >= 1);
s.add(y < x + 3);

params p(c);
p.set(":timeout", static_cast<unsigned>(1)); // in milliseconds
s.set(p);

std::cout << s.check() << std::endl;
std::cout << "reason unknown: " << s.reason_unknown() << std::endl;

【讨论】：