本文介绍了使用 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.
这篇关于使用 z3 Python API 的循环内求解器超时的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!