Add z3 integration

[grantjenks]

An integration with Z3 seems possible and useful. Z3 knows nothing about Python so I think the trick is to encode Python’s object model in Z3 code.

For example, when matching sequences, Z3 would be told that each matching element must be equal. This might also apply to NamedTuples and data classes pretty easily.

The general class of equality would be difficult to capture without translating Python byte code to Z3 statements but the common cases of built-in types (ints, strs, lists, etc) and class factories (data class, named tuple, etc) may be possible.

I know z3 supports integers but does it also handle strings and floats? Hi