Modelling "swapping two elements in an array creates permutation" in Z3

Question

I'd like to model in Z3 that swapping two elements in an array creates a permutation.

Swapping two elements can be modelled very naturally:

(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))))

But how do I model "a2 is a permutation of a0" and check this is a valid statement?

In a similar question (Equal lists are permutations of one another. Why does Z3 answer 'unknown'?) the author provides a permutation function which checks whether two arrays are permutations of each other. However they are two problems with this. First, the function could consider two arrays as permutations if e.g. one array contains an object x two times and another arrays contains x only once. Second, Z3 can't solve even very simple assertions involving this function (hence the question).

In the answer, someone suggests to use sequences to model the problem. The permutation function in this answer also has the problem that it's wrong if arrays can contain an object multiple times. Also, modelling the swapping of two elements seems very unnatural to me to express with sequences.

Answer 1

Two common solutions (in software verification) for proving equality modulo permutation of two arrays or sequences are 1. abstracting the sequences into multisets, and proving the equality of those, and 2. maintaining a permutation witness, i.e. a function that maps each element from its new to its original index (see also this encoding of a sorting algorithm or, for the unfearful, this encoding of the quickselect algorithm).

Below is your original coded, plus code that maintains a permutation witness pw_i. The witness is updated after each modification (swap) of the original array, such that it always gives you, for each index k, the original array index of the element that can now be found at index k. The initial witness pw0 is the identity function.

(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)