Add support for DatatypeSort (#110)

This adds support for the (confusingly named) `DatatypeSort` function/class that is used to create unresolved datatype sorts in the Z3 Python API.

This closes #109

---------

Co-authored-by: Daniel Larraz <daniel-larraz@users.noreply.github.com>

Author: allan-mercari

cvc5_pythonic_api/cvc5_pythonic.py

@@ -8689,6 +8689,13 @@ def CreateDatatypes(*ds):
     return tuple(result)
 
 
+def DatatypeSort(name, ctx=None):
+    """Create a reference to a sort that will be declared as a recursive datatype"""
+    ctx = _get_ctx(ctx)
+    s = ctx.tm.mkUnresolvedDatatypeSort(name)
+    return SortRef(s, ctx)
+
+
 class DatatypeSortRef(SortRef):
     """Datatype sorts."""
 

test/pgm_outputs/example_datatypes.py.out

@@ -13,3 +13,6 @@ t is a 'cons': True
 
 [a = 51]
 proved
+
+Sorts match: True
+Operation on resolved sort works: True

test/pgms/example_datatypes.py

@@ -42,3 +42,18 @@
     solve(List.head(List.cons(a, List.nil)) > 50)
 
     prove(Not(List.is_nil(List.cons(a, List.nil))))
+
+    print()
+
+    # Test DatatypeSort for unresolved datatype sorts.
+    SomeType = Datatype('SomeType')
+    SomeTypeSort = DatatypeSort('SomeType')
+    SomeType.declare('nil')
+    SomeType.declare('some', ('someof', SeqSort(SomeTypeSort), ))
+    SomeTypeSort = SomeType.create()
+
+    nil = SomeTypeSort.nil
+    some = SomeTypeSort.some(Unit(nil))
+
+    print("Sorts match:", SomeTypeSort == SomeTypeSort.someof(some)[0].sort())
+    print("Operation on resolved sort works:", simplify(SomeTypeSort.is_nil(SomeTypeSort.someof(some)[0])))