Z3 Время ожидания с помощью Solver

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;