Z3 API incompatibility: DatatypeSort function

[allan-mercari]

Thank you for your awesome work on the CVC5 solver, it is very exciting. I'm trying to port a program that uses the z3 Python API to try out CVC5, but hit a roadblock.

Consider the following example from the Z3 documentation for constructing a datatype that contains a reference inside a sequence.

SomeType = Datatype('SomeType')
SomeTypeSort = DatatypeSort('SomeType')
SomeType.declare('nil')
SomeType.declare('some', ('someof', SeqSort(SomeTypeSort), ))
SomeTypeSort = SomeType.create()

However, currently the DatatypeSort function is not available in the cvc5 pythonic API so this code fails.

[this is a copy+paste of a discussion I made here as this is a much better place for it.]

[yoni206]

Hi thanks for this issue! I'll look further into in order to respond.