在此Z3问题评论中建议选项rlimit优先于timeout:
将超时与搜索算法相结合使得一切都是非确定性的,所以现在您甚至不必更改随机种子以使其失败!使用rlimits(
(set-option :rlimit <n>)和类似的)来确定资源边界的方式.
我试图rlimit在Z3的帮助(z3 -pd)中找到更多信息,但提供的描述只有很短.
具体来说,我有以下问题:
rlimit限制了 - 只是时间还是记忆？:rlimit 1000相当于:timeout 1000求解器必须在1000几毫秒后终止？rlimit重复设置(timeout可以)还是只设置一次？A1:无论我们认为什么都有道理.这个想法是计算类似"基本操作"的东西,但是这个定义随着我们的进行而改变并添加新的"操作".对于不同版本的Z3,无法保证它保持不变.但是,只要您继续使用相同的二进制文件,它就是确定性的.
A2:不,没有等价,但一旦超过rlimit,Z3将终止.我们最近修复了一些没有终止的bug,我确信那里还有一些bug,但我们当然会修复它们.
A3:是的,你可以做到
...
(set-option :rlimit 12345)
(check-sat)
...