Z3Py: создание списка констант неинтерпретированной сортировки

Question

У меня есть неинтерпретированная сортировка A

sortA = DeclareSort('A')

и функция foo:

foo = Function('foo',sortA,sortA,BoolSort())

Теперь я хочу определить список констант вида A. Моя попытка была:

X = [ Consts("c_%s" % i,sortA) for i in range(10) ]

Но это не работает, поскольку

s.add(foo(X[0],X[1]))

выдает ошибку «Ожидается выражение Z3». Буду благодарен за любую помощь :)

Answer 1

Consts создает список констант, и этот список не является выражением Z3 (но представляет собой список выражений Z3 в Python). Вместо этого Const работает как ожидалось.