API объявления массива данных в C #

Question

Учитывая, что у меня есть пользовательский тип данных (скажем, Клиент), я хочу определить следующий тип данных массива:

Customers[].

Глядя на Z3 C # API: http://z3prover.github.io/api/html/class_microsoft_1_1_z3_1_1_context.html

var customerArraySort = context.MkArraySort(<domain>, <range>);

1. Что означают <domain> и <range>?
2. Будет ли следующее создавать сортировку массива Customer []?

var customerArraySort = context.MkArraySort(customerSort, context.IntSort);

Answer 1

(Отказ от ответственности: у меня нет опыта работы с Z3 или опыта в доказательстве теорем)

Context.MkArraySort задокументировано здесь: http://z3prover.github.io/api/html/class_microsoft_1_1_z3_1_1_context.html#ac25b9e8235bb453b4fd33de33d15e917

Существует две перегрузки с параметрами с одинаковыми именами, за исключением того, что один принимает один аргумент Sort domain, другой принимает аргумент массива Sort[] domain.

Оба метода являются фабричными методами для ArraySort объектов класса, которые представляют сортировку массива.

• domain и range - это термины в математике, которые относятся к вводу и выводу функции соответственно: https://www.wolframalpha.com/examples/mathematics/mathematical-functions/domain-and-range/

(Я принимаю, что документация для Z3 отсутствует, например, краткие и бесполезные описания методов и примеры).