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

公理“nil 没有最后一个元素”：

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

公理“如果 xs 是列表 x:nil 那么 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 几乎一无所知。