Are there any non-sorting workarounds supported in some Z3 bindings?

Question

I am not very familiar with Z3, but I must use it to carry out a project.

I use Z3 binding , it has a text interface like SMT-LIB v2 capable of eliminating universal quantifiers, but it does not yet support declare-sort , while my model needs some kind of custom type definition (I cannot figure out how to use Int only in my model ..)

In this case, if I want to use binding, how can I work to get the declare-sort function in my model? Is there something similar in Z3?

or what are the usual tips for working on some type that is not supported in Z3?

Answer 1

I believe that the best answer is to send Siddharth Agarwal directly.