z3（v4.4.0）统计中报告的时间是否包括读取SMT约束文件所需的时间？

Question

还是纯粹是求解时间？这个问题适用于 z3 被称为外部二进制文件的情况。我在我的一些例子中问这个问题，约束解决时间很短，我怀疑将与文件读取时间相当。另外，小值（例如

Answer 1

是的，总时间应该包括阅读问题所需的时间。这些数字“相当”准确，但并不完全准确。在我们自己的性能实验中，我们通常使用精度更高的外部定时器，但通常我们不需要测量加载时间。

如果您进入加载时间和求解时间都非常小的区域，那么最好切换到 API，而不是转储 .smt2 文件然后调用外部二进制文件。