Можно ли запросить Python API z3 о том, истекло ли время ожидания?

Question

Я хочу ограничить время, которое z3 может потратить на какую-то проблему, которая работает, установив таймаут с помощью:

from z3 import *
solver = Solver()
solver.set(timeout=60000)
# add constraints to solver
result = solver.check()

Однако я хотел бы проверить, действительно ли произошло тайм-аут.result - это unknown в этом случае, но это может произойти и потому, что проблема не разрешима (я использую теории, которые, как правило, не разрешимы).

Итак, есть ли способузнать, произошел ли тайм-аут?

Answer 1

Конечно, просто используйте reason_unknown вызов:

from z3 import *
solver = Solver()
solver.set(timeout=1)
x, y = Ints('x y')
solver.add(x**y == x)
result = solver.check()
print result
print solver.reason_unknown()

Это печатает:

unknown
timeout