Feature request: add regex translator to Python API

[ahelwer]

Both myself and @pschanely (somewhat) independently implemented the same function converting Python regexes to Z3 regexes using the output of python's sre_parse module. Here is my implementation and here is Phillip's. Given the obvious utility of allowing users to express regexes in a simple, familiar & well-specified syntax, should this function be added to the Z3 Python API? I would be happy to make the necessary changes.

[NikolajBjorner]

When in a separate file and without features outside of regex seems like a good idea for python use.
For example, add file z3rex or z3regex (but not z3x.py).

[LeventErkok]

@ahelwer It'd be nice if you can precisely document what parts of sre are supported and what parts aren't. (I'm assuming anchors, named groups etc. will fall in to the latter category.) This way other tools targeting z3's regex engines can rely on the exact grammar you support to provide a consistent experience.