这个简单的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指南说明了在内射函数/反函数的情况下。也许你可以在这里进行类似的转换。