在 Z3 中编码部分地图

Question

我想在 Z3 中对部分地图进行编码，支持询问地图是否是为某个键定义的。

它还应该支持(update_map m1 m2) 操作，它使用m2 中的映射更新m1，从而m2 的映射覆盖m1 的映射。

我尝试使用数组和自定义option 数据类型对其进行编码，并且我公理地指定了update_map 函数。但是，似乎 Z3 甚至无法处理我的 update_map 规范：它在以下代码上返回 unknown：

(declare-datatypes (T) ((option None (Some (option-value T)))))
(define-sort map (K V) (Array K (option V)))

(declare-sort V)
(declare-sort K)

(define-const empty_map (map K V)
  ((as const (Array K (option V))) None))

(define-fun get ((m (map K V)) (k K)) (option V)
  (select m k))

(define-fun put ((m (map K V)) (k K) (v V)) (map K V)
  (store m k (Some v)))

(declare-fun update_map ((map K V) (map K V)) (map K V))

(assert (forall ((m1 (map K V)) (m2 (map K V)) (k K))
    (=> (= (get m2 k) None)
        (= (get (update_map m1 m2) k) (get m1 k)))))
(assert (forall ((m1 (map K V)) (m2 (map K V)) (k K) (v V))
    (=> (= (get m2 k) (Some v))
        (= (get (update_map m1 m2) k) (Some v)))))

(check-sat)

所以我有两个问题：

1. 是否有更好的方法来编码地图，使我能够证明关于update_map 的事实？
2. 谁能分享一些关于为什么 Z3 不理解这个规范的直觉？例如，让 Z3 难以做到这一点的“核心功能”是什么？ [我已经知道量词被认为是困难的并且一阶逻辑是不可判定的，我正在寻找更具体的东西;-)]

Answer 1

Z3 无法证明可满足性，即它无法为您的公式构建模型。不幸的是，我不知道更确切的原因 - 可能是 Z3 对数组、量词或其组合的模型查找能力的限制。

如果您最终对寻找模型不感兴趣，而是对反例（unsat cores）感兴趣，那么添加一个无法满足的公式并尝试改为 unsat。 IE。尝试以下方法（免责声明：我实际上并没有尝试过，但我相信你明白了）：

(assert (not
  (=
    (get
      (update_map
        (put empty_map 2 -2)
        (put empty_map 1 -1))
      -1))))

作为在数组顶部公理化映射的替代方法，请查看Dafny's map axiomatisation。公理以 Boogie 语言提供，但翻译成 Z3 通常是直截了当的。