访问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。