选项 rlimit 和 timeout 之间的关系是什么？
What is the relation between options `rlimit` and `timeout`?
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.
我试图在 Z3 的帮助 (z3 -pd) 中找到有关 rlimit 的更多信息，但那里提供的描述非常简短。
具体来说，我有以下问题：
- Q1:
rlimit 限制什么样的 "solver resources" - 只是时间还是内存？
- Q2：
:rlimit 1000 是否等同于 :timeout 1000 因为求解器必须在 1000 毫秒后终止？
- Q3:
rlimit 可以重复设置（如 timeout 可以）还是只设置一次？
Q1：rlimit 限制什么样的“求解器资源”——只是时间还是内存？
A1：我们认为有道理的。这个想法是计算“基本操作”之类的东西，但是随着我们继续添加新的“操作”，这个定义会发生变化。不能保证不同版本的 Z3 会保持相同。但是，只要您一直使用相同的二进制文件，它就是确定性的。
问题 2：:rlimit 1000 是否等同于 :timeout 1000，因为求解器必须在 1000 毫秒后终止？
A2：不，不存在等效性，但是一旦超过 rlimit，Z3 就会终止。我们最近修复了一些没有终止的错误，我敢肯定那里的某个地方仍然存在一些错误，但我们当然会修复它们。
Q3：rlimit 可以重复设置（超时可以）还是只设置一次？
A3：是的，你可以
(set-option :rlimit 12345)
(check-sat)
...```
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.
我试图在 Z3 的帮助 (z3 -pd) 中找到有关 rlimit 的更多信息，但那里提供的描述非常简短。
具体来说，我有以下问题：
- Q1:
rlimit限制什么样的 "solver resources" - 只是时间还是内存？ - Q2：
:rlimit 1000是否等同于:timeout 1000因为求解器必须在1000毫秒后终止？ - Q3:
rlimit可以重复设置（如timeout可以）还是只设置一次？
Q1：rlimit 限制什么样的“求解器资源”——只是时间还是内存？
A1：我们认为有道理的。这个想法是计算“基本操作”之类的东西，但是随着我们继续添加新的“操作”，这个定义会发生变化。不能保证不同版本的 Z3 会保持相同。但是，只要您一直使用相同的二进制文件，它就是确定性的。
问题 2：:rlimit 1000 是否等同于 :timeout 1000，因为求解器必须在 1000 毫秒后终止？
A2：不，不存在等效性，但是一旦超过 rlimit，Z3 就会终止。我们最近修复了一些没有终止的错误，我敢肯定那里的某个地方仍然存在一些错误，但我们当然会修复它们。
Q3：rlimit 可以重复设置（超时可以）还是只设置一次？
A3：是的，你可以
(set-option :rlimit 12345)
(check-sat)
...```