在 Z3 中建模“交换数组中的两个元素会创建排列”

Question

我想在 Z3 中建模，交换数组中的两个元素会创建一个排列。

交换两个元素可以非常自然地建模：

(declare-sort Obj)
; a0 is original array, a2 is array after swap
(declare-const a0 (Array Int Obj))
(declare-const a1 (Array Int Obj))
(declare-const a2 (Array Int Obj))
(declare-const i Int)
(declare-const j Int)

(assert (= a1 (store a0 i (select a0 j))))
(assert (= a2 (store a1 j (select a0 i))))

但是我如何模拟“a2 是 a0 的排列”并检查这是一个有效的陈述？

在一个类似的问题 (Equal lists are permutations of one another. Why does Z3 answer 'unknown'?) 中，作者提供了一个 permutation 函数来检查两个数组是否是彼此的排列。然而，这有两个问题。首先，该函数可以将两个数组视为排列，例如一个数组包含对象x 两次，而另一个数组仅包含一次x。其次，Z3 甚至无法解决涉及此函数的非常简单的断言（因此提出了问题）。

在答案中，有人建议使用序列来建模问题。这个答案中的置换函数也有一个问题，如果数组可以多次包含一个对象，那就错了。另外，用序列来表达两个元素的交换对我来说似乎很不自然。

Answer 1

证明两个数组或序列的相等模置换的两种常见解决方案（在软件验证中）是 1. 将序列抽象为多集，并证明它们的相等性，以及 2. 维护置换见证，即映射的函数从新索引到原始索引的每个元素（另请参阅this encoding of a sorting algorithm，或者，对于无畏的人，this encoding of the quickselect algorithm）。

以下是您的原始代码，以及维护置换见证的代码pw_i。见证在原始数组的每次修改（交换）后都会更新，因此它总是为您提供每个索引 k 元素的 original 数组索引，可以现在可以在索引k找到。 初始见证pw0 是身份函数。

(set-option :auto_config false)
(set-option :smt.mbqi false)

(declare-sort Obj)

; a0 is original array, a2 is array after swap
(declare-const a0 (Array Int Obj))
(declare-const a1 (Array Int Obj))
(declare-const a2 (Array Int Obj))
(declare-const i Int)
(declare-const j Int)

; Permutation witness
(declare-const pw0 (Array Int Int))
(declare-const pw1 (Array Int Int))
(declare-const pw2 (Array Int Int))
; The initial permutation witness is the identity function
(assert (forall ((k Int)) (= (select pw0 k) k)))

; (check-sat) ; Sanity check (must not return UNSAT)

(push)
  ; Check that the initial permutation witness is the identity function
  (assert (not (forall ((k Int)) (= (select a0 k) (select a0 (select pw0 k))))))
  (check-sat) ; UNSAT unexpected
(pop)

; Swap two elements of the array
(assert (= a1 (store a0 i (select a0 j))))
(assert (= a2 (store a1 j (select a0 i))))

; Update the permutation witness correspondingly
(assert (= pw1 (store pw0 i (select pw0 j))))
(assert (= pw2 (store pw1 j (select pw0 i))))

(push)
  ; Check that pw2 indeed witnesses the permutation of a2 w.r.t. a0
  (assert (not (forall ((k Int)) (= (select a2 k) (select a0 (select pw2 k))))))
  (check-sat) ; UNSAT unexpected
(pop)

; (check-sat) ; Sanity check (must not return UNSAT)


(declare-const a3 (Array Int Obj))
(declare-const a4 (Array Int Obj))
(declare-const pw3 (Array Int Int))
(declare-const pw4 (Array Int Int))

(push)
  ; Another swap ...
  (assert (= a3 (store a2 j (select a2 (+ i 1)))))
  (assert (= a4 (store a3 (+ i 1) (select a2 j))))
  ; ... but we forgot to update the permutation witness
  (assert (= pw4 pw2))

  (assert (not (forall ((k Int)) (= (select a4 k) (select a0 (select pw4 k))))))
  (check-sat) ; Must not return UNSAT
(pop)

(push)
  ; A swap gone wrong ...
  (assert (= a3 (store a2 j (select a2 (+ i 1)))))
  (assert (= a4 (store a3 (+ i 1) (select a3 j)))) ; Last occurrence of a3 should be a2 (fix --> UNSAT)
  ; ... but the permutation witness is updated correctly
  (assert (= pw3 (store pw2 j (select pw2 (+ i 1)))))
  (assert (= pw4 (store pw3 (+ i 1) (select pw2 j))))

  (assert (not (forall ((k Int)) (= (select a4 k) (select a0 (select pw4 k))))))
  (check-sat) ; Must not return UNSAT
(pop)