Теория массивов в Z3: (1) модель сложна для понимания, (2) не умею реализовывать функции и (3) разница с последовательностями

Question

Следуя вопросу, опубликованному в статье Насколько выразительными могут быть массивы в Z3(Py)? Например , я выразил следующую формулу в Z3Py:

Exists i::Integer s.t. (0<=i<|arr|) & (avg(arr)+t<arr[i])

Это означает: есть ли позицияi::0<i<|arr|в массиве, значение которогоa[i]больше, чем среднее значение массиваavg(arr)плюс заданный порогt.

Решение в Z3Py:

      t = Int('t')
avg_arr = Int('avg_arr')
len_arr = Int('len_arr')

arr = Array('arr', IntSort(), IntSort())

phi_1 = And(0 <= i, i< len_arr)
phi_2 = (t+avg_arr<arr[i])

phi = Exists(i, And(phi_1, phi_2))

s = Solver()
s.add(phi)
print(s.check())
print(s.model())

Обратите внимание, что (1) формула выполнима и (2) каждый раз, когда я ее выполняю, я получаю другую модель. Например, я только что получил:[avg_a = 0, t = 7718, len_arr = 1, arr = K(Int, 7719)].

У меня сейчас три вопроса:

1. Что значитarr = K(Int, 7719)]иметь в виду? Означает ли это, что массив содержит одинIntэлемент со значением7719? В таком случае, что делаетKиметь в виду?
2. Конечно, эта реализация неверна в том смысле, что значения среднего и длины не зависят от самого массива. Как я могу реализовать простойavgиlenфункции?
3. Гдеiиндекс в модели, заданной решателем?

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