Expose an API function to allow defining polymorphic recursive datatypes

[mben-romdhane]

The SMT2 format allows polymorphic datatypes to be defined recursively, but the only API exposed allows defining just one polymorphic data type. It would be nice to expose the most generic form of this API. Happy to volunteer a PR if this sounds good.

[NikolajBjorner]

I added ML to the API coherence workflow a bit late. Seems to have entirely ignored ocaml bindings for coherence.

[mben-romdhane]

Thank you for the quick response! I believe this is true of the C API as well (unless you are referring to my other issue).

[NikolajBjorner]

You can create "type variables" and you can create parametric data-type sorts and then bind them to a definition.
This is a multi-step process added after the initial APIs for parametric data-types. There is some example related to an earlier issue filed in August/September last year.

[NikolajBjorner]

z3/examples/c++/example.cpp

Line 1009 in 9ea16e9

void polymorphic_datatype_example() {