z3 - ソルバーでの Z3 タイムアウト

Question

簡単な質問があります。次の API を使用してソルバーがタイムアウトしたかどうかを判断するにはどうすればよいですか?

Z3_lbool Z3_API Z3_solver_check (Z3_context c, Z3_solver s )

Z3_lbool は真、偽、または未定義であるためです。

Answer 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;