grantjenks
commented
3 years ago Quick look shows Z3 supports Int and Real which are probably close enough to int() and float() https://ericpony.github.io/z3py-tutorial/guide-examples.htm
To make the integration work, the type information would need to be inspected. That way, Python variables could be converted to Z3 variables. For pattern matching, that means associating a type with a name.
This is also interesting because it supports expressions like < and >.
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