Is a PythonAPI for z3str3 available?

[swag2198]

[This is less of an issue and more of a beginner trying to use z3str3 for a problem.]
I am trying to solve a set of string constraints over one or more string variables, like this one having 2 string variables x and y:

len(x) <= 3
x[0:1] == "a"
y[2:4] is uppercase regex

Ideally, I would like to know if there is any solution to the set of constraints (sat/unsat) and if there are any, any random satisfying assignment to x and y would suffice. For example here, x = "ab" and "y=avSWac" is a satisfying assignment to the variables. Preferably, I wish to do this in python but C++ is also fine.

I realize these constraints are handled by z3str3 as expressed in the input language description here. But I am new to z3 and z3str3 and I am not able to find any python API handling string variables and constraints. My questions are:

• Does there exist a python API handling string-related things like the numerical/real one?
• Where can I find an end-to-end example solving a string problem (say my example above) in Python or C++?

I am really lost in this repository and cannot find a starting point to use the code or the examples. Any help will be really appreciated.

Thank you.