From 316c0e577a178d54395f50e1454f8ca7316878f4 Mon Sep 17 00:00:00 2001
From: Allan Wirth <allan@mercari.com>
Date: Thu, 14 Aug 2025 18:00:46 +0900
Subject: [PATCH 1/3] Add support for DatatypeSort

---
 cvc5_pythonic_api/cvc5_pythonic.py        |  8 ++++++++
 test/pgm_outputs/example_datatypes.py.out |  3 +++
 test/pgms/example_datatypes.py            | 15 +++++++++++++++
 3 files changed, 26 insertions(+)

diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py
index 685dce9..97f0032 100644
--- a/cvc5_pythonic_api/cvc5_pythonic.py
+++ b/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."""
diff --git a/test/pgm_outputs/example_datatypes.py.out b/test/pgm_outputs/example_datatypes.py.out
index f5d842c..ab1962a 100644
--- a/test/pgm_outputs/example_datatypes.py.out
+++ b/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
diff --git a/test/pgms/example_datatypes.py b/test/pgms/example_datatypes.py
index fa6e06c..44c0027 100644
--- a/test/pgms/example_datatypes.py
+++ b/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])))

From 39620e63c48d47617e75cc6548d79932a13d7986 Mon Sep 17 00:00:00 2001
From: allan-mercari <146688091+allan-mercari@users.noreply.github.com>
Date: Fri, 15 Aug 2025 13:39:12 +0900
Subject: [PATCH 2/3] Update cvc5_pythonic_api/cvc5_pythonic.py

Co-authored-by: Daniel Larraz <daniel-larraz@users.noreply.github.com>
---
 cvc5_pythonic_api/cvc5_pythonic.py | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py
index 97f0032..c36e2fc 100644
--- a/cvc5_pythonic_api/cvc5_pythonic.py
+++ b/cvc5_pythonic_api/cvc5_pythonic.py
@@ -8688,14 +8688,11 @@ 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)
-        
+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."""

From ad619cd34637c3274350e0d5fcaa374fa756ab6f Mon Sep 17 00:00:00 2001
From: Daniel Larraz <daniel-larraz@users.noreply.github.com>
Date: Fri, 15 Aug 2025 07:54:08 -0500
Subject: [PATCH 3/3] Format with black

---
 cvc5_pythonic_api/cvc5_pythonic.py | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py
index c36e2fc..ffc4da5 100644
--- a/cvc5_pythonic_api/cvc5_pythonic.py
+++ b/cvc5_pythonic_api/cvc5_pythonic.py
@@ -8688,12 +8688,14 @@ def CreateDatatypes(*ds):
         result.append(dref)
     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."""