Z3: я должен использовать массивы, IntVectors или что-то еще?

Question

Мне интересно, какой тип данных я должен использовать для своего приложения z3.Насколько я понимаю, единственными вариантами для структур данных, подобных целочисленным массивам, являются Array (IntSort (), IntSort ()) и IntVector ().

Причины, по которым я считаю массивы избыточными: каждый элемент массива записывается толькооднажды я не делаю ничего подобного Store((Store(X, y, z1)), y, z2)Кроме того, каждый массив имеет предопределенную длину <= 256 (и каждое целое число в массиве находится в диапазоне от 0 до 63). </p>

Причины, по которым я думаю, что BitVectors не будет работать: я хочу использовать переменные Int для индексациив массивы.Например, у меня может быть z = Int('z'), некоторые пункты ограничивают z, а затем Or(arr[z] == 2, arr[z + 1] == 2).Мое понимание после игры с z3 и чтения заключается в том, что векторы не поддерживают это.

Есть ли способ получить мощность индексации переменных без использования дорогостоящих операций с массивами?

Answer 1

Если у вас есть небольшие массивы фиксированной длины без доступа к символьному индексу, тогда я настоятельно рекомендую использовать IntVector (см. https://z3prover.github.io/api/html/namespacez3py.html#a7e166f891df8f17fd23290bec963b03c)

. Обратите внимание, что здесь важно, нужен ли вам доступс символьным индексом. (То есть всегда ли вы обращаетесь к массиву с известными постоянными индексами или вам нужна возможность чтения / записи в символически адресуемом месте.) Из вашего описания видно, что вы всегда статически знаете адрес,так что IntVector - ваш лучший выбор. Если адреса могут быть символическими, то вы должны использовать старые добрые массивы SMTLib, которые стоят дороже.