Add FuncSortRef and fix QuantifierRef.sort for lambda expressions

[daniel-larraz]

QuantifierRef.sort() hardcoded the Boolean sort, so a lambda expression reported Bool instead of its actual function sort:

>>> i = Int('i')
>>> f = Function('f', IntSort(), IntSort())
>>> Lambda([i], f(i)).sort()
Bool          # before
(-> Int Int)  # after

Changes

Returning the real sort is only half the fix: _to_sort_ref had no branch for function sorts, so the result was an opaque SortRef with no way to reach the domain or range. This PR adds FuncSortRef and routes function sorts to it, which gives every function sort — a lambda's or an uninterpreted function's — these accessors:

>>> L = Lambda([i, j], f2(i, j))
>>> L.sort().arity(), L.sort().domain(), L.sort().domain_n(1), L.sort().range()
(2, Int, Int, Int)

>>> g = Function('g', IntSort(), RealSort(), BoolSort())
>>> g.sort().range()
Bool

The names deliberately mirror ArraySortRef. Z3Py models lambdas as arrays, so a lambda's sort there is an array sort and Z3Py code reaches for .domain() / .range() / .domain_n(i); matching those names lets such code carry over. cvc5 keeps function and array sorts genuinely distinct, so is_array_sort() still reports False for them and Store/Select remain array-only — is_func_sort() is added to test for the new sort.

Finally, FuncDeclRef.arity/domain/range now delegate to self.sort() rather than each re-deriving from getSort().getFunction*(). This is behavior-preserving — every FuncDeclRef is built from a function sort — and puts the three cvc5 calls in one place. The # type: ignore comments follow the existing ArrayRef.domain/range precedent.

Relation to #115

This supersedes #115, which fixed the QuantifierRef.sort() half. That fix alone leaves Lambda(...).sort() as a bare SortRef, so Z3Py code calling .domain() / .range() on it trades a wrong answer for an AttributeError. This PR closes that gap. Note also that #115's CI failure is unrelated to its change — it predates c66c2b7 (#116), which updated the multiple_solvers expected output.

Testing

• test_doc.py: 2080 doctests, 0 failures; the 32 new examples are all collected and passing.
• test_unit.py: OK.
• black --check --required-version 24: clean.
• pyright: 621 errors before and after this change — none new.

🤖 Generated with Claude Code

[Copilot]

Pull request overview

This PR fixes sort reporting for lambda expressions and introduces a dedicated wrapper for function sorts so callers can introspect function sort domain/range consistently across lambdas and uninterpreted functions.

Changes:

• Route cvc5 function sorts through a new FuncSortRef via _to_sort_ref, exposing .arity(), .domain() / .domain_n(i), and .range().
• Fix QuantifierRef.sort() to return the actual function sort for Lambda(...) instead of hardcoding Bool.
• Simplify FuncDeclRef.arity/domain/range by delegating to self.sort()’s accessors (centralizing the cvc5 function-sort queries).

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[alex-ozdemir]

LGTM