Lambda sort and DatatypeRef in _to_expr_ref

[philzook58]

I'm looking at getting cvc5 to be an alternate backend to my project and there are a couple z3 incompatibilities.

There's a missing cast to DatatypeRef here

cvc5_pythonic_api/cvc5_pythonic_api/cvc5_pythonic.py

Line 949 in be54c23

def _to_expr_ref(a, ctx, r=None):

which I backpatched as

def Const(name, sort):
    # _to_expr doesn't have a DatatypeRef case
    x = cvc5.pythonic.Const(name, sort)
    if isinstance(sort, DatatypeSortRef):
        x = DatatypeRef(x.ast, x.ctx, x.reverse_children)
    return x

And the sort returned by lambdas is not right

cvc5_pythonic_api/cvc5_pythonic_api/cvc5_pythonic.py

Line 9031 in be54c23

def sort(self):

I tried patching this as

def _qsort(self):
    if self.is_lambda():
        return ArraySort(self.var_sort(0), self.body().sort())
    else:
        return BoolSort(self.ctx)


QuantifierRef.sort = _qsort

but I get a deeper error which I don't understand

________________________________________________________________ ERROR collecting tests/test_kernel.py ________________________________________________________________
tests/test_kernel.py:9: in <module>
    import knuckledragger.theories.Interval
knuckledragger/theories/Interval.py:9: in <module>
    setof = kd.define("setof", [i], smt.Lambda([x], smt.And(i.lo <= x, x <= i.hi)))
knuckledragger/kernel.py:132: in define
    f(*args) == body
../../../.local/lib/python3.10/site-packages/cvc5/pythonic/cvc5_pythonic.py:375: in __eq__
    return BoolRef(c.solver.mkTerm(Kind.EQUAL, a.as_ast(), b.as_ast()), c)
cvc5.pxi:2556: in cvc5.cvc5_python_base.Solver.mkTerm
    ???
cvc5.pxi:1538: in cvc5.cvc5_python_base.TermManager.mkTerm
    ???
E   RuntimeError: Subexpressions must have the same type:
E   Equation: (= (setof i) (lambda ((x Real)) (and (<= (lo i) x) (<= x (hi i)))))
E   Type 1: (Array Real Bool)
E   Type 2: (-> Real Bool)

Are lambda sorts distinct from Arrays?