def _to_z3(x):

    if x in _z3_interpreted:
        return _z3_interpreted[x]

    elif type(x) is UninterpretedSort:
        if x not in _z3_uninterpreted_sorts:
            _z3_uninterpreted_sorts[x] = z3.DeclareSort(x.name)
        return _z3_uninterpreted_sorts[x]

    elif type(x) is FunctionSort:
        assert False, "FunctionSort's aren't converted to Z3"

    elif type(x) in (Var, Const) and first_order_sort(x.sort):
        return z3.Const(x.name + ':' + str(x.sort), to_z3(x.sort))

    elif type(x) in (Var, Const) and type(x.sort) is FunctionSort and len(x.sort.sorts) == 1:
        # convert to first order
        s = x.sort.sorts[0]
        return z3.Const(x.name + ':' + str(s), to_z3(s))

    elif type(x) in (Var, Const) and type(x.sort) is FunctionSort:
        assert type(x) is Const, "Cannot convert high-order variables to Z3, only constants"
        return z3.Function(x.name, *(
            to_z3(s) for s in x.sort
        ))

    elif type(x) is Apply and len(x.terms) == 0:
        # convert application to use of first order symbol
        return to_z3(x.func)

    elif type(x) is Apply:
        return to_z3(x.func)(*(to_z3(t) for t in x.terms))

    elif type(x) in _z3_operators:
        return _z3_operators[type(x)](*(to_z3(y) for y in x))

    elif type(x) in _z3_quantifiers:
        if len(x.variables) == 0:
            return to_z3(x.body)
        else:
            return _z3_quantifiers[type(x)](
                [to_z3(v) for v in x.variables],
                to_z3(x.body),
            )

    else:
        assert False, type(x)
Convert a term or a sort to a Z3 object.
dataset/ETHPy150Open Microsoft/ivy/ivy/z3_utils.py/_to_z3