Создайте массив с фиксированным размером и инициализируйте его

Я собираюсь создать массив с фиксированным размером и инициализировать его некоторыми значениями.

Например, следующий код C ++:

a[0] = 10;
a[1] = 23;
a[2] = 27;
a[3] = 12;
a[4] = 19;
a[5] = 31;
a[6] = 41;
a[7] = 7;

Есть ли в Z3 утилиты для его моделирования?

Ответы на вопрос(2)

Я согласен с ЛеонардоответТем более, что массивы предназначены для моделирования БОЛЬШИХ входных диапазонов. На самом деле не существует способа определения массивов фиксированного размера (если только вы не используете конечную сортировку ввода, такую какBitVecSort(3)).

Так как пример Z3Py (Python) был снят, я хотел добавить свое собственное решение. Эта функция определяет диапазон записей массива, начиная с начального адреса. (Утверждения хранятся вSolver объект.)

def assert_array(solver, array, address, data):
    for (offset, value) in enumerate(data):
        solver.add(array[address + offset] == value)

Обратите внимание, чтоarray[idx] является эквивалентом Z3Py(select array idx) в SMT 2.0. Массив в вопросе может быть смоделирован следующим образом:

s = Solver()
a = Array('a', IntSort(), IntSort())
data = [10, 23, 27, 12, 19, 31, 41, 7]
assert_array(s, a, 0, data)

print s
#[a[0] == 10,
# a[1] == 23,
# a[2] == 27,
# a[3] == 12,
# a[4] == 19,
# a[5] == 31,
# a[6] == 41,
# a[7] == 7]

Z3 поддерживает теорию массивов, но обычно используется для кодирования неограниченных массивов или массивов очень большого размера. Под большой я имею в виду число обращений к массиву (т. Е. Выбирает) в вашей формуле намного меньше, чем фактический размер массива. Мы должны спросить себя: «Действительно ли нам нужны массивы для моделирования / решения проблемы X?». Для массивов фиксированного размера, как в вашем примере, мы можем использовать разные переменные для каждой позиции массива. Пример:a0 заa[0], a1 заa[1]и т. д. Конечно, если мы не используем теории, то кодируем доступ к массиву, такой какa[i] должен быть закодирован как большой термин if-then-else, такой как

(ite (= i 0) a0 (ite (= i 1) a1 ...))

Если размер массива известен и мал, то обычно это наиболее эффективный подход для кодирования проблемы.

С другой стороны, если вы решите использовать теорию массивов, вы можете закодировать инициализацию в своем вопросе как:

(declare-const a (Array Int Int))
(assert (= (select a 0) 10))
...
(assert (= (select a 7) 7))

Вот весь пример, закодированный в формате SMT 2.0:

http://rise4fun.com/Z3/iwo

Обратите внимание, что для кодирования обновления в этом массиве. Например, оператор Ca[3] = 5, мы должны создать новую переменную массива, представляющую массив после этого присваивания. Самый компактный способ используетstore выражение:

(declare-const a1 (Array Int Int))
(assert (= a1 (store a 3 5)))

Вот полный пример с обновлением.

http://rise4fun.com/Z3/Kpln

Вы также можете рассмотреть API-интерфейсы Python / C ++ /. Net. Они позволяют нам кодировать подобные примеры гораздо более компактным способом. Идея состоит в том, чтобы реализовать функции, которые кодируют часто используемые шаблоны, такие как инициализация массива. Вот ваш пример инициализации массива в Python:

http://rise4fun.com/Z3Py/AAD

 20 февр. 2017 г., 11:04
Последняя ссылка мертва

Ваш ответ на вопрос