z3 - 在 Z3 中建模 "swapping two elements in an array creates permutation"

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，它总是为您提供可以修改的元素的 原始 数组索引。 现在可以在索引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)