Как определить сортировку в Z3 Java API?

Question

Как мне определить сортировку в Z3 Java API?Мне нужно сделать что-то вроде следующего:

(define-sort Set (T) (Array T Bool))

Answer 1

Есть много примеров в https://github.com/Z3Prover/z3/blob/master/examples/java/JavaExample.java

В частности: https://github.com/Z3Prover/z3/blob/master/examples/java/JavaExample.java#L1711-L1830

- полностью проработанный пример параметрического представления дерева.