Add support for DatatypeSort

Author: Allan Wirth

cvc5_pythonic_api/cvc5_pythonic.py

@@ -8688,6 +8688,14 @@ def CreateDatatypes(*ds):
         result.append(dref)
     return tuple(result)
 
+class DatatypeSort:
+    """Unresolved datatype sorts."""
+    
+    def __init__(self, name, ctx=None):
+        self.name = name
+        self.ctx = _get_ctx(ctx)
+        self.ast = self.ctx.tm.mkUnresolvedDatatypeSort(name)
+        
 
 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])))