使用 z3 Python API 的循环内求解器超时 [英] Solver timeout within loop using z3 Python API

问题描述

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

Per an earlier suggestion, I'm trying to set early timeout for a solver while using z3Py.

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

Again, without all the particulars, this is what I'm attempting:

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()

本质上，超时永远不会发生(即使以毫秒为单位的时间小得可笑).

Essentially, timeout never occurs (even with ridiculously small times in ms).

推荐答案

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

Are you using Z3 on Linux or FreeBSD? There was a bug related to timers on these platforms. I fixed the problem, but it is not part of the official release yet. See the following post for more details.

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

这篇关于使用 z3 Python API 的循环内求解器超时的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！