как я могу узнать, сколько значений имеет массив в z3?

Question

Я использую Z3py, но когда я определяю массив

array = Array('array', IntSort(), IntSort())

Я не знаю, как узнать, сколько значений имеет массив.

Answer 1

Массивы в Z3 (и в SMT) имеют неограниченный размер. См., Например, Создание массива с фиксированным размером и его инициализация