With Z3 it is possible to declare custom datatypes (i.e., records) that take type parameters. For example, a Pair that takes the types T1 and T2 for its first and second element respectively, is declared as follows (taken from the Z3 Guide):
(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))
This type declaration can then be used to create pairs with different element types. For example, the constants p1 and p2 are both pairs with different element types (Int String and Bool Int respectively):
(declare-const p1 (Pair Int String))
(declare-const p2 (Pair Bool Int))
I want to declare such a parametrized datatype using Z3's Java API. However, the datatype declarations there seem to not have a feature to add type parameters to datatype declarations.
The Java API of Z3 does provide a method mkDatatypeSort in its Context class to declare a new datatype in Z3 (Link). However, this method does not take any arguments for type parameters. Also the constructors (taken as second argument of mkDatatypeSort) do not allow to define type parameters.
I expected that it is possible to declare datatypes with type parameters in Z3's Java API, but I am not able to do so. Am I missing something or does this feature just not exist in the Java API?
Is it possible to declare such datatypes with the Java API?
z3 API's (whether it's C/C++/Java/Python) don't allow for creation of parameterized types.
Note that parameterized-types are essentially a nicety in SMTLib: Essentially, each instantiation with different sorts will be a separate type of its own, with nothing to do with each other. So, the idea is to do this on your own: Write a function that takes the relevant sorts, and creates the corresponding "monomorphized" type on the fly. You'll have to change the accessor names slightly each time to avoid clashes, or you can add enough type-annotations to let the solver figure out the relevant types. (I'd go with the former as it is simpler, but latter is definitely possible too.)