z3（v4.4.0）統計信息中報告的時間是否包含讀取SMT約束文件所需的時間？

Question

還是純粹的解決時間？這個問題是針對z3被稱爲外部二進制文件的情況。我正在問這個問題，因爲在我的一些例子中，約束解決時間很短，我懷疑它會和文件讀取時間相提並論。此外，小值的總時間有多準確（例如，< 1秒）？

Answer 1

是的，總的時間應該包括需要閱讀問題的時間。這些數字「相當」精確，但不完全確切。在我們自己的性能實驗中，我們通常使用更高精度的外部定時器，但通常我們不需要測量加載時間。

如果您正在進入加載時間和求解時間都很小的區域，那麼最好切換到API而不是轉儲.smt2文件，然後調用外部二進制文件。