不同方式包含功能的Z3列出

Question

Axiomatising上列出了包含操作（on Rise4Fun）作爲

(declare-fun Seq.in ((List Int) Int) Bool) 

(assert (forall ((e Int)) 
    (not (Seq.in nil e)))) 

(assert (forall ((xs (List Int)) (e Int)) 
    (iff 
    (not (= xs nil)) 
    (= 
     (Seq.in xs e) 
     (or 
     (= e (head xs)) 
     (Seq.in (tail xs) e)))))) 

能使Z3 4.0反駁斷言

(declare-const x Int) 
(assert (Seq.in nil x)) 
(check-sat) ; UNSAT, as expected 

的在我的眼前等效axiomatisation

(assert (forall ((xs (List Int)) (e Int)) 
    (ite (= xs nil) 
    (= (Seq.in xs e) false) 
    (= 
     (Seq.in xs e) 
     (or 
     (= e (head xs)) 
     (Seq.in (tail xs) e)))))) 

結果在unknown。

這可能是觸發器的問題，或者有什麼特定於List域的東西可以解釋行爲上的差異嗎？

Answer 1

在rise4fun的腳本會禁用:mbqi引擎。因此，Z3將嘗試僅使用E匹配來解決問題。當沒有提供模式（aka觸發器）時，Z3會爲我們推斷觸發器。 Z3使用許多啓發式來推斷模式/觸發器。其中之一與您的腳本相關，並解釋發生了什麼。 Z3永遠不會選擇產生「匹配循環」的模式/觸發器。我們說一個模式/觸發P中的量詞Q上匹配循環時，Q的實例將產生一個新的匹配爲P. 讓我們考慮量詞

(assert (forall ((xs (List Int)) (e Int)) 
    (ite (= xs nil) 
    (= (Seq.in xs e) false) 
    (= 
     (Seq.in xs e) 
     (or 
     (= e (head xs)) 
     (Seq.in (tail xs) e)))))) 

Z3將不選擇(Seq.in xs e)爲圖案/觸發這個量詞，因爲它會產生一個匹配的循環。假設我們有一個基礎術語(Seq.in a b)。此術語匹配(Seq.in xs e)的模式。使用a實例化量詞將b將產生也與(Seq.in xs e)模式相匹配的術語(Seq.in (tail a) b)。 使用(tail a)和b實例化量詞將生成術語(Seq.in (tail (tail a)) b)，該術語也與(Seq.in xs e)的模式匹配，依此類推。

在搜索期間，Z3將使用多個閾值阻止匹配循環。但是，表現通常會受到影響。因此，默認情況下，Z3不會選擇(Seq.in xs e)作爲模式。相反，它將選擇(Seq.in (tail xs) e)。這種模式不會產生匹配的循環，但它也可以防止Z3證明第二個和第三個查詢是不可滿足的。 E匹配引擎的任何限制通常由:mbqi引擎處理。但是，腳本中禁用了:mbqi。

如果您在腳本中提供第二個和第三個查詢的模式。 Z3將證明所有示例爲unsat。這裏是一個明確的模式/觸發你的例子：

http://rise4fun.com/Z3/DkZd

第一個例子經歷，即使沒有，因爲只需要第一個量詞證明的例子是unsat使用模式。

(assert (forall ((e Int)) 
    (not (Seq.in nil e)))) 

注意(Seq.in nil e)是這個量詞一個完美的模式，它是由Z3選擇的一個。