Stubfiles for the Python API

[wraith1995]

For usability in python projects that use mypy/other static type checkers/LSP implementations/etc, it would be nice if the Python APIs included stubfiles. I might be willing to take this on if there is no opposition/other plans.

[NikolajBjorner]

no opposition. Could be tedious as Python API is hand-written.
Copilot can fill in a lot. I tried a few rounds and it fills in signatures for functions.

def get_version() -> str: ...

def is_int(e: ExprRef) -> bool: ...
def is_real(e: ExprRef) -> bool: ...
def is_arith(e: ExprRef) -> bool: ...
def is_bv(e: ExprRef) -> bool: ...
def is_algebraic_number(e: ExprRef) -> bool: ...
def is_seq(e: ExprRef) -> bool: ...
def is_re(e: ExprRef) -> bool: ...
def is_array(e: ExprRef) -> bool: ...
def is_datatype(e: ExprRef) -> bool: ...

def get_param(name: str) -> str: ...
def set_param(name: str, value: str) -> None: ...

def ExprRef.sexpr(self) -> str: ...
def ExprRef.decl(self) -> FuncDeclRef: ...
def ExprRef.children(self) -> Sequence[ExprRef]: ...
def ExprRef.num_args(self) -> int: ...
def ExprRef.arg(self, i: int) -> ExprRef: ...
def ExprRef.num_sorts(self) -> int: ...

[wraith1995]

Looks like a good start. This is a bit better than I got with mypy's stubgen so I will follow these ideas once I have a solid moment.

[wraith1995]

@NikolajBjorner Kind related to my efforts to do this with stubgen, but I am a bit curious: is there any particular reason to use ctypes instead of pybind11? I am not proposing a change (though I might run a pybind11 binding generator to see what happens), but I am curious because 1) stubgen or pybind11-stubgen tend to do a good job and 2) pybind11 is what I've used for a few python bindings at this point and I've been fairly satisfied sans some pains with Python's gc.