是否可以查询 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

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

Is it possible to query z3's Python API on whether a timeout occured?

python

python-3.x

z3

z3py