英文:
Z3Py Timeout parameter
问题
是Z3 Python API中的超时参数意味着严格的执行时间上限吗？因为如果我将其设置为十分钟，它会运行超过那个时间几分钟。
求解器始终会终止。问题不在于此。问题在于它总是超过指定的超时时间。
英文:
Is the timeout parameter in the Z3 python API meant to be a strict upper bound for the execution time? Because if I set it to ten minutes it runs for a few minutes more than that.
The solver always terminates. That’s not the problem. It’s just that it always overshoots the timeout specified.
答案1
得分: 1
你是在考虑经过的（即墙上的）时间还是 CPU 时间吗？
我认为 z3 的超时机制使用了 rlimit：https://www.rdocumentation.org/packages/unix/versions/1.5.5/topics/rlimit
正如该页面中所述：
RLIMIT_CPU：对进程可以消耗的 CPU 时间量（而非经过的时间）的时间限制（以秒为单位）。当进程达到软限制时，它会收到 SIGXCPU 信号。
因此，经过的时间不一定与 CPU 时间匹配，因为可能会有其他进程阻止 z3 运行。
英文:
Are you looking at elapsed (i.e., wall-)time or CPU-time?
I believe z3's timeout mechanism uses rlimit: https://www.rdocumentation.org/packages/unix/versions/1.5.5/topics/rlimit
As noted in that page:
> RLIMIT_CPU : a limit in seconds on the amount of CPU time (not elapsed
> time) that the process may consume. When the process reaches the soft
> limit, it is sent a SIGXCPU signal.
So, elapsed time doesn't necessarily match CPU time, as there might be other processes that stop z3 from running.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论