Три способа присвоить значения массиву в z3

Question

Насколько я знаю, существует три способа присвоения значений массиву в z3.

1. Использование assert для присвоения значений некоторым ячейкам:

(declare-const a1 (Array Int Int))
(declare-const a2 (Array Int Int))

(assert (= 1 (select a1 0)))
(assert (= 2 (select a2 0)))

z3 возвращает unsat при добавлении ограничения (assert (= a1 a2)).

используйте as const, чтобы сначала инициализировать массив, а затем присвоить значения определенным ячейкам:

(declare-const a3 (Array Int Int))
(assert
    (=
        (store ((as const (Array Int Int)) 64) 0 3)
        a3
    )
)
(declare-const a4 (Array Int Int))
(assert
    (=
        (store ((as const (Array Int Int)) 64) 0 4)
        a4
    )
)

Добавьте (assert (= a3 a4)), и мы снова получим unsat.

определить массив с помощью функции:

(define-const a5 (Array Int Int)
    (lambda ((i Int))
    (ite (= i 0) 5 64)))
(define-const a6 (Array Int Int)
    (lambda ((i Int))
    (ite (= i 0) 6 64)))

Но если мы добавим (assert (= a5 a6)), z3 вернет sat.Почему?

Кстати, есть ли (лучший) способ присвоения значений массиву в z3?

Answer 1

Это ошибка. Проверьте этот выпуск .