z3 - 访问 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 不支持递归函数（请参阅此答案），因此您必须自己声明和公理一个未解释的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 指南），因此依赖于 E 匹配。这也是提供显式模式的原因，请参阅此问题。如果您想尝试 MBQI，您可能必须更改公理化，但我对 MBQI 几乎一无所知。