這個簡單的Z3證明爲什麼這麼慢？

Question

以下Z3代碼超時的在線REPL：

; I want a function 
(declare-fun f (Int) Int) 

; I want it to be linear 
(assert (forall ((a Int) (b Int)) (
    = (+ (f a) (f b)) (f (+ a b)) 
))) 

; I want f(2) == 4 
(assert (= (f 2) 4)) 

; TIMEOUT :(
(check-sat) 

所以做這個版本，它正在尋找一個功能上的實數：

(declare-fun f (Real) Real) 
(assert (forall ((a Real) (b Real)) (
    = (+ (f a) (f b)) (f (+ a b)) 
))) 
(assert (= (f 2) 4)) 
(check-sat) 

它的速度更快，當我給它一個矛盾：

(declare-fun f (Real) Real) 
(assert (forall ((a Real) (b Real)) (
    = (+ (f a) (f b)) (f (+ a b)) 
))) 
(assert (= (f 2) 4)) 
(assert (= (f 4) 7)) 
(check-sat) 

我對定理證明者很不瞭解。這裏有什麼特別慢的？證明者是否有很多證明存在f（2）= 4的線性函數的麻煩？

Answer 1

是緩慢的很可能是由於過多的量詞實例，造成問題的模式/觸發。如果您還不知道這些，請查看Z3 guide的相應部分。底線：模式是一種句法啓發式，指示SMT解算器何時實例化量詞。模式必須涵蓋所有量化變量和解釋函數，例如在模式中不允許使用加法（+）。 A 匹配循環是其中每個量詞實例化引起進一步量詞實例化的情況。

在你的情況下，Z3可能挑選模式集:pattern ((f a) (f b))（因爲你沒有明確提供模式）。這表明Z3實例化每個a, b的量詞，其中在當前證明搜索中已經發生了基礎術語(f a)和(f b)。最初，證明搜索包含(f 2);因此，量詞可以被a, b實例化，其綁定到2, 2。這產生了(f (+ 2 2))，其可以用於再次實例化量詞（並且還與(f 2)結合）。 Z3因此陷入了匹配循環。

這裏是一個片段爭論我的觀點：

(set-option :smt.qi.profile true) 

(declare-fun f (Int) Int) 

(declare-fun T (Int Int) Bool) ; A dummy trigger function 

(assert (forall ((a Int) (b Int)) (! 
    (= (+ (f a) (f b)) (f (+ a b))) 
    :pattern ((f a) (f b)) 
    ; :pattern ((T a b)) 
))) 

(assert (= (f 2) 4)) 

(set-option :timeout 5000) ; 5s is enough 
(check-sat) 
(get-info :reason-unknown) 
(get-info :all-statistics) 

有了明確規定的圖案，你會得到你原來的行爲（模指定的超時）。此外，統計數據會報告量詞的大量實例（如果您增加超時時間，還會更多）。

如果您評論第一個模式並取消第二個模式的註釋，即如果用一個不會顯示在證明搜索中的虛擬觸發器「量出」量詞，則Z3立即終止。不過，Z3仍然會報告unknown，因爲它「知道」它沒有考慮到量化限制（這是對sat的要求;也不能顯示unsat）。

有時可能重寫量詞以獲得更好的觸發行爲。例如，Z3指南說明了在內射函數/反函數的情況下。也許你可以在這裏進行類似的轉換。