Construct DatatypeRef and DatatypeSortRef for datatype terms and sorts

[daniel-larraz]

Neither _to_expr_ref nor _to_sort_ref had a datatype case, so a term of a datatype sort came back as a plain ExprRef and its sort as a plain SortRef:

List = Datatype('List')
List.declare('cons', ('car', IntSort()), ('cdr', List))
List.declare('nil')
List = List.create()

l = Const('l', List)
type(l).__name__             # 'ExprRef' before, 'DatatypeRef' after
l.sort()                     # SortRef before, DatatypeSortRef after
l.sort().num_constructors()  # AttributeError before, 2 after
l.sort().accessor(0, 0)      # AttributeError before, car after

Datatype.create() already returns a proper DatatypeSortRef, so only the round-trip through these two constructors lost it.

Changes

One branch added to each constructor. isDatatype() is disjoint from every sort predicate already tested in both chains — I checked Int, Bool, Array, Set, String, Seq, BitVec, FP, RoundingMode, uninterpreted and function sorts all report False — so the branches go at the end and cannot shadow an existing case.

Tuple sorts are datatypes as well, so TupleSort terms and sorts are now properly wrapped too:

pair, mk_pair, (first, second) = TupleSort('pair', [IntSort(), BoolSort()])
mk_pair(Int('i'), Bool('b')).sort().num_constructors()   # 1

DatatypeRef.sort() no longer needs to build the sort itself and delegates to _sort, the same cleanup #118 made for FuncDeclRef.

Relation to #100

This fixes the first of the two problems reported in #100 — the missing DatatypeRef cast — and makes the reporter's Const backpatch unnecessary. The lambda-sort half was fixed by #118.

Worth noting for whoever closes #100: neither PR unblocks the reporter's original knuckledragger use case, which needs a function declaration whose range is a lambda's sort. cvc5 rejects a function sort as a codomain, and declaring the range as an array sort instead makes f(x) == lambda_body fail on the Array Real Bool vs (-> Real Bool) mismatch from the issue. Bridging function and array sorts is separate work.

Testing

• test_doc.py: 2094 doctests, 0 failures; 22 new examples covering the wrapping, the sort methods and the datatype constructor applications.
• test_unit.py: OK.
• black --check --required-version 24: clean.
• pyright: 620 errors, down from 621 on main — none new.

🤖 Generated with Claude Code

[alex-ozdemir]

LGTM