訪問Z3列表中的最後一個元素

Question

如何訪問Z3列表中的最後一個元素？

(declare-const lst (List Int)) 
(assert (not (= lst nil))) 
(assert (= (head lst) 1)) 
(assert (= (last_element lst) 2)) 
(check-sat) 

Answer 1

AFAIK，Z3沒有內置函數來訪問列表的最後一個元素。由於SMT-Lib2不支持遞歸函數（請參閱this answer），因此您必須自行聲明並公開未解釋的last_element函數。

聲明：

(declare-fun last_element ((List Int) (Int)) Bool) 

公理 「零沒有最後一個元素」：

(assert (forall ((x Int)) (! 
    (not (last_element nil x)) 
    :pattern ((last_element nil x)) 
))) 

公理「如果XS是列表X：無然後X是xs「的最後一個元素」：

(assert (forall ((xs (List Int)) (x Int)) (! 
    (implies 
    (= xs (insert x nil)) 
    (last_element xs x)) 
    :pattern ((last_element xs x)) 
))) 

公理 「如果X是XS尾的最後一個元素，那麼它也是XS本身的最後一個元素」：

(assert (forall ((xs (List Int)) (x Int)) (! 
    (implies 
    (last_element (tail xs) x) 
    (last_element xs x)) 
    :pattern ((last_element xs x)) 
))) 

看到這個rise4fun-link一個例。

請注意：基於模型量詞實例化的連接示例開關（MBQI，見Z3 guide），並且因此依賴於E-匹配。這也是提供顯式模式的原因，請參閱this question。如果你想給MBQI一個嘗試，你可能不得不改變公理化，但我幾乎不瞭解MBQI。