證明在Z3

Question

感性的事實，我想證明在Z3，微軟的SMT求解器的電感事實。我知道，Z3，一般也不會提供這種功能，如Z3 guide解釋（第8節：數據類型），但它看起來就像當我們限制了我們想要證明的事實域中，這是可能的。請看下面的例子：

(declare-fun p (Int) Bool) 
(assert (p 0)) 

(assert (forall ((x Int)) 
    (=> 
    (and (> x 0) (<= x 20)) 
    (= (p (- x 1)) (p x))))) 
(assert (not (p 20))) 

(check-sat) 

求解器與unsat正確響應，這意味着(p 20)是有效的。問題是，當我們放鬆這個約束時（我們用上面例子中的20替換大於20的整數），求解器迴應unknown。

我發現這種奇怪的，因爲它並不需要Z3長，解決了原來的問題，但是，當我們由一個增加上限也突然變得不可能。我曾嘗試的模式添加到量詞如下：

(declare-fun p (Int) Bool) 
(assert (p 0)) 

(assert (forall ((x Int)) 
    (! (=> 
    (and (> x 0) (<= x 40)) 
    (= (p (- x 1)) (p x))) :pattern ((<= x 40))))) 
(assert (not (p 40))) 

(check-sat) 

這似乎更好地工作，但現在的上限是40，這是否意味着我可以最好不要用Z3來證明這些事實，或我錯誤地闡述了我的問題嗎？

Answer 1

Z3使用了很多啓發控制量詞實例。其中一個是基於「實例化深度」。 Z3使用「深度」屬性標記每個表達式。所有用戶提供的斷言都被標記爲深度0.當量詞被實例化時，新表達式的深度被碰撞。 Z3不會使用標記深度大於預定義閾值的表達式來實例化量詞。在你的問題，達到閾值：(p 40)是深度0，(p 39)是深度1，(p 38)是深度2等

爲了提高門檻，你應該使用的選項：

(set-option :qi-eager-threshold 100) 

這裏使用此選項的示例：http://rise4fun.com/Z3/ZdxO。

當然，採用這種設置，Z3將超時，例如，用於(p 110)。

在未來，Z3將有「有限量化」提供更好的支持。在大多數情況下，處理這種量詞的最佳方法是擴展它。 使用編程API，我們可以在將它們發送到Z3之前輕鬆「實例化」表達式。 這裏是在Python（http://rise4fun.com/Z3Py/44lE）的示例：

p = Function('p', IntSort(), BoolSort()) 

s = Solver() 

s.add(p(0)) 
s.add([ p(x+1) == p(x) for x in range(40)]) 
s.add(Not(p(40))) 

print s.check() 

最後，在Z3，含有算術符號模式不是非常有效的。問題在於Z3在解決之前對公式進行預處理。然後，包含算術符號的大多數模式將永遠不匹配。有關如何有效使用模式/觸發器的更多信息，請參閱this article。作者還提供了slide deck。