是否可以查询z3的pythonapi是否发生超时？

Question

我想限制z3处理某个问题的时间，这可以通过设置超时来实现：

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

但是，我想检查是否确实发生了超时^{<在这种情况下，cd1>}是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