z3 - 选项 `rlimit` 和 `timeout` 之间有什么关系？

Question

建议在 this Z3 issue comment那个选项rlimit优先于 timeout :

Combining timeouts with a search algorithm makes everything non-deterministic, so now you don't even have to change the random seed to make it fail! Use rlimits ((set-option :rlimit <n>) and similar) for a deterministic way of resource bounding.

我试图找到有关 rlimit 的更多信息在 Z3 的帮助 ( z3 -pd ) 中，但提供的描述非常简短。

具体来说，我有以下问题:

第一季度 : 什么样的“求解器资源”rlimit限制 - 只是时间还是内存？

Q2 : 是 :rlimit 1000相当于 :timeout 1000因为求解器必须在 1000 之后终止毫秒？

Q3 : jar 头rlimit可以重复设置(如 timeout 可以)还是只设置一次？

Answer 1

Q1:rlimit 限制了什么样的“求解器资源”——只是时间还是内存？
A1:无论我们认为什么都是有道理的。这个想法是计算“基本操作”之类的东西，但是随着我们继续并添加新的“操作”，该定义会发生变化。无法保证对于不同版本的 Z3 会保持相同。但是，只要您继续使用相同的二进制文件，它就是确定性的。
问题 2: :rlimit 1000 是否等同于 :timeout 1000，因为求解器必须在 1000 毫秒后终止？
A2:不，没有等价，但一旦超过rlimit Z3 将终止。我们最近修复了一些没有终止的错误，我相信在某个地方仍然存在一些错误，但我们当然会修复它们。
Q3: rlimit 可以重复设置(如超时可以)还是只设置一次？
A3:是的，你可以做

(set-option :rlimit 12345)
(check-sat)
...```