python - 使用 z3 Python API 在循环内求解超时

Question

根据较早的建议，我正在尝试在使用 z3Py 时为求解器设置提前超时。

同样，没有所有细节，这就是我正在尝试的：

for bits in range(A, B, incrmt)
    s = Solver();
    s.set("timeout", 30) #30, 3000, 30000, 60000 no change
    s.add(some constraints)
    if(s.check() == sat):
        print "Sat, %d," %(bits)
    else:
        print "Sat Unknown, %d," %(bits)
        break
    sys.stdout.flush()

从本质上讲，永远不会发生超时（即使以毫秒为单位的时间非常短）。

Answer 1

您在 Linux 或 FreeBSD 上使用 Z3 吗？这些平台上存在与计时器相关的错误。我解决了这个问题，但它还不是正式版本的一部分。有关详细信息，请参阅以下帖子。

• 如何使用 C-API 为 z3_solver 设置超时？