爲什麼z3.check（）會在z3.push（）前立即放慢？

下面的Python代碼片段說明了Z3的一個階段性能行爲。如果不調用push()，則z3會在0.1s內檢查公式。與push()（沒有額外的斷言），z3需要0.8s。即使在交換s.append(f)和s.push()後也會發生類似的結果。爲什麼z3.check（）會在z3.push（）前立即放慢？

import time 
import z3 
f = z3.parse_smt2_file("smt-lib/QF_BV/RWS/Example_1.txt.smt2") 
s = z3.Solver() 
s.append(f) 
t1 = time.time() 
s.check() # 0.10693597793579102 seconds 
print(time.time() - t1) 

s = z3.Solver() 
t1 = time.time() 
s.append(f) 
s.push() 
s.check() # 0.830916166305542 seconds 
print(time.time() - t1)

任何想法爲什麼會發生這種放緩？而且，如何解決？

我正在使用z3-4.3.2.bb56885147e4-x64-osx-10.9.2。

來源

2014-10-17 Venkatesh-Prasad Ranganath

謝謝，這是一個很好的repro。 Z3爲第二個實例使用增量求解器。從用例來看，爲什麼會出現這種情況並不清楚，所以它指向了可用性錯誤。在內部，Z3使用工廠模式來創建解算器。我正在研究這是否是原因所在，或者它是否是先前求解器的副作用超越了狀態。 – 2014-10-17 05:35:07

@NikolajBjorner即使片段在不同的Python進程中執行，行爲也是一樣的。 – 2014-10-17 22:55:16

您的示例在第二個實例化中使用「push」。這產生巨大的差異。 Z3的位向矢量解算器（尚未）可以通過API增量使用。它僅適用於獨立聲明，不能與範圍（push/pop）互操作。第一次調用使用位矢量SAT解算器。沒有「推/流行」進行。第二次調用是在「push」調用之後進行的。然後Z3確定爲了跟蹤示波器依賴關係，它必須使用增量SMT內核，該內核不受益於更高效的位矢量解算器。

來源

2014-10-17 06:16:21

那麼，你會推薦在Z3外部積累斷言並使用求解器的非範圍實例嗎？ – 2014-10-17 23:03:34

爲什麼z3.check（）會在z3.push（）前立即放慢？

回答

相關問題