Моделирование назначения массива в Z3

Question

Я работаю над проектом для проверки программы. У меня есть следующий оператор, который будет смоделирован в Z3:

temp = a[i]; 
a[i] = a[j]; 
a[j] = temp; 

Все переменные имеют целочисленный тип. Кто-нибудь даст мне несколько советов о том, как создавать ограничения для моделирования вышеуказанных утверждений?

Answer 1

Вот общий «рецепт».

Мы представляем массивные обновления с использованием (store a i v). Результатом является новый массив, равный a, но в позиции i содержится значение v. Доступ к массиву a[i] должен быть закодирован как (select a i). Задания, такие как i = i + 1, обычно кодируются путем создания переменных Z3, которые представляют значение i до и после назначения. То есть, мы будем кодировать его как (= i1 (+ i0 1)). Имейте в виду, что формула (= i (+ i 1)) эквивалентна false.

Вот пример, приведенный выше, в формате SMT 2.0.

http://www.rise4fun.com/Z3/G5Zk

Вот скрипт находится в ссылке выше.

(declare-const a0 (Array Int Int)) 
(declare-const a1 (Array Int Int)) 
(declare-const a2 (Array Int Int)) 
(declare-const temp0 Int) 
(declare-const temp1 Int) 
(declare-const i0 Int) 
(declare-const j0 Int) 

(assert (= temp0 (select a0 i0))) 
(assert (= a1 (store a0 i0 (select a0 j0)))) 
(assert (= a2 (store a1 j0 temp0))) 

(check-sat) 
(get-model)