CODEWITHSUNDEEP
z3
Raj
Raj

Reputation: 3462

Z3 Timeout with Solver

I have a simple question. How is it possible to determine if solver timed out with following API - 

Z3_lbool Z3_API Z3_solver_check (Z3_context c, Z3_solver s )

Since Z3_lbool is just true, false or undefined.

Upvotes: 1

Views: 882

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

You can use the API Z3_string Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s). If you are using C++, the object solver provides the method std::string reason_unknown(). Here is a small example that uses it:

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;

Upvotes: 1

Related Questions