Z3 统计:时间衡量什么? [英] Z3 statistics: what does time measure?

问题描述

使用 -st 命令选项运行 Z3 3.1 时，我得到了奇怪的统计结果.如果按 Ctrl-C，Z3 报告 total_time <;时间.否则，如果您等到 Z3 完成:total_time > time.

I am getting strange statistics results when run Z3 3.1 with -st command option. If you press Ctrl-C, Z3 reports total_time < time. Otherwise, if you wait until Z3 finishes: total_time > time.

1. 总时间"和时间"衡量什么?
2. 这是一个错误(虽然很小)(上述差异)?

谢谢！

推荐答案

这是 Z3 for Linux(3.0 和 3.1 版)中的一个错误.该错误不会影响 Windows 版本.该修复程序将在下一个版本 (Z3 3.2) 中提供.用于跟踪 time 的计时器不正确.

This is a bug in Z3 for Linux (versions 3.0 and 3.1). The bug does not affect the Windows version. The fix will be available in the next release (Z3 3.2). The timer used to track time is incorrect.

顺便说一句，total-time 测量总执行时间，time 仅测量上次 check-sat 命令消耗的时间.所以，我们必须有 total-time >= time.

BTW, total-time measures the total execution time, and time only the time consumed by the last check-sat command. So, we must have that total-time >= time.

备注:此答案已根据 Swen Jacobs 提供的反馈进行了更新.

Remark: this answer has been updated using the feedback provided by Swen Jacobs.

这篇关于Z3 统计:时间衡量什么?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！