Support higher-order function sorts and partial application

[daniel-larraz]

Z3Py models a lambda as an array, so defining a function by a lambda means declaring it with the lambda's sort as the range and equating the application with the lambda. cvc5 keeps function and array sorts distinct, and neither half of that pattern could be expressed:

body = Lambda([x], And(lo <= x, x <= hi))

Function('setof', RealSort(), RealSort(), body.sort())
# RuntimeError: invalid argument '(-> Real Bool)' for 'codomain',
#               expected non-function sort as codomain sort

f(x)   # f : (-> Real Real Bool)
# SMTException: Incorrect number of arguments to f

Declaring the range as an array sort instead does not help: g(lo, hi) == body then fails with sort mismatch, the (Array Real Bool) vs (-> Real Bool) clash from #100.

All of it is reachable through cvc5's native higher-order support. The pythonic layer just never wired it up.

Result

This program now runs unchanged under Z3Py and cvc5, and prints the same thing under both — only the solver construction differs:

if BACKEND == 'z3':
    from z3 import *
    def make_solver(): return Solver()
else:
    from cvc5_pythonic_api import *
    def make_solver():
        s = SolverFor('HO_ALL'); s.set('ho-elim', True); return s
# ------- identical source below this line -------
x, lo, hi = Reals('x lo hi')
body  = Lambda([x], And(lo <= x, x <= hi))
setof = Function('setof', RealSort(), RealSort(), body.sort())
defn  = ForAll([lo, hi], setof(lo, hi) == body)

s = make_solver(); s.add(defn); s.add(Not(setof(0, 10)[3]))
print('3 in [0,10]  :', s.check())      # unsat under both
s = make_solver(); s.add(defn); s.add(setof(0, 10)[42])
print('42 in [0,10] :', s.check())      # unsat under both
print(simplify(Lambda([x], x + 1)[3]))  # 4 under both

Changes

Function flattens a function-sort range (first commit). cvc5 normalizes higher-order sorts, so Real -> (-> Real Bool) is built as (-> Real Real Bool). Applying the leading domains yields the range sort again, so the distinction stays invisible:

setof.sort()                          # (-> Real Real Real Bool)
setof(lo, hi).sort() == body.sort()   # True

FreshFunction shares the same helper.

FuncDeclRef.__call__ builds partial applications (first commit). Given too few arguments -- or when the function is itself a partial application -- it emits an HO_APPLY chain, since neither case is expressible with APPLY_UF. The result carries the rest of the function sort and is callable again, so setof(lo, hi) == body typechecks.

The printer gains an HO_APPLY case (first commit). It had none, so printing a partial application raised Cannot print: Kind.HO_APPLY. The curried spine is collapsed, so f(x)(y) reads as f(x, y) -- an equal term, printed the way a saturated application is. The head of the spine need not be a name (If(c, f, g)(i) is a function-sorted term too), so the group is composed directly rather than through seq1, which measures its header.

[] is accepted as a second spelling of application (second commit). Z3Py applies a lambda, and anything defined by one, with []; without it there was no way to write the use site that both accept -- [] was rejected here, () and a saturated call are rejected by Z3Py, so the intersection was empty even though the whole definition was already portable.

Select is deliberately left alone. It is an array operation, and a lambda has a function sort here, not an array sort. Nothing is lost by that: Z3Py defines Select(a, i) as a[i] --

def Select(a, *args):
    args = _get_args(args)
    if z3_debug():
        _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
    return a[args]

-- so a select of a lambda rewritten as L[i] goes on working under both. I checked .eq() on Select(x, ...) against x[...] in Z3Py for 1-dim and 2-dim arrays, integer indices, Store results, K, nested selects, model values, and 1- and 2-argument lambdas: equal in every case.

Scope

This makes the terms constructible, not the problem decidable. cvc5 reasons about function terms only under a logic carrying the HO_ prefix, and a quantified definition needs ho-elim to be discharged rather than answered unknown:

ground definition,     HO_ALL             -> unsat
quantified definition, HO_ALL             -> unknown
quantified definition, HO_ALL + ho-elim   -> unsat

Both are documented in the docstrings and exercised by the new test. Applying a lambda directly needs neither -- a beta-redex reduces before the solver sees a function term, so Lambda([x], x + 1)[3] works under a plain Solver().

I did not have Solver sniff assertions for function sorts and silently upgrade the logic: overriding a deliberately pinned logic seems worse than an error naming HO_ALL.

Where this accepts more than Z3Py

Worth flagging for review, since it is one-directional -- code written against cvc5 using these will not port back:

• f[i] and f[i, j] on a plain uninterpreted function. Z3Py raises TypeError.
• L2[3] -- partial indexing of a two-argument lambda. Z3Py raises select requires 3 arguments.
• f(i) -- partial application generally, which is the point of the first commit.

Keeping [] uniform across function-sorted terms was a deliberate choice over restricting it to exactly Z3Py's set; the alternative rules all draw awkward lines (rejecting f[i] but allowing g(i)[j], say). Happy to narrow it if you would rather the two agree exactly.

Also unchanged: decl() still raises on a partial application and children() still includes the function, both following the existing convention that only APPLY_UF is destructured.

Relation to #100

This addresses the remaining item there. The two items reported in that issue were fixed by #118 and #120; this is the function/array interop underneath them.

Testing

• New test/pgms/higher_order.py covering the path end to end: the flattened sort, partial application and its printing, a non-name application head, both spellings agreeing via eq, Select still refusing a function, and check() in both directions.
• test_doc.py: 2124 doctests, 0 failures.
• test_unit.py: OK.
• black --check --required-version 24: clean.
• pyright: 635 errors against 633 on main. The two are ctx.tm.mkTerm on an optional context in the new __getitem__, one more instance each of a pattern the file already has 119 and 93 of.
• Regression-checked the paths this touches: saturated application, decl()/children(), FreshFunction, datatype constructor/selector/tester application (they subclass FuncDeclRef but define their own __call__), and the arity errors for too many arguments and for f().

🤖 Generated with Claude Code