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

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