0
還是純粹的解決時間?這個問題是針對z3被稱爲外部二進制文件的情況。我正在問這個問題,因爲在我的一些例子中,約束解決時間很短,我懷疑它會和文件讀取時間相提並論。此外,小值的總時間有多準確(例如,< 1秒)?z3(v4.4.0)統計信息中報告的時間是否包含讀取SMT約束文件所需的時間?
還是純粹的解決時間?這個問題是針對z3被稱爲外部二進制文件的情況。我正在問這個問題,因爲在我的一些例子中,約束解決時間很短,我懷疑它會和文件讀取時間相提並論。此外,小值的總時間有多準確(例如,< 1秒)?z3(v4.4.0)統計信息中報告的時間是否包含讀取SMT約束文件所需的時間?
是的,總的時間應該包括需要閱讀問題的時間。這些數字「相當」精確,但不完全確切。在我們自己的性能實驗中,我們通常使用更高精度的外部定時器,但通常我們不需要測量加載時間。
如果您正在進入加載時間和求解時間都很小的區域,那麼最好切換到API而不是轉儲.smt2文件,然後調用外部二進制文件。