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

Question

我想限制 z3 在某些问题上花费的时间，这可以通过设置超时来实现:

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

但是，我想检查是否确实发生了超时。在这种情况下，结果是未知，但据我所知，这也可能发生，因为问题是不可判定的(我使用的理论通常是不可判定的)。

那么，有没有办法判断是否发生超时呢？

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