Support for more regular expression operations

[Pat-Lafon]

Fixes #272

(First two commits) My attempt at adding the new regular expression operations: power, allchar, and diff. I also noticed that option was exposed but not implemented so I've added that as well.

(Third commit) I was looking to test my inclusions to the code base but I realized that I'm not sure about the semantics of regular expressions in Z3? I ran into some weird behavior I don't understand so I just added a simple test from https://z3prover.github.io/api/html/z3py_8py_source.html#l11172 to get some advice. test_regex_union works as expected, checking that (a|b) matches with a and b but not c. However, I found that I get SatResult::Sat in more cases than I expect like in test_regex_union2 which just checks that c matches with (a|b). I would expect to get SatResult::Unsat but I don't?

[waywardmonkeys]

In upstream Z3, you have to look at some of the SMTLIB tests to find things that actually exercise this code (rather than via the native API).

[waywardmonkeys]

@Pat-Lafon Do you want to try rebasing this on top of current master and see if CI passes? We're preparing for a new release.