Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add z3 integration #13

Open
grantjenks opened this issue Feb 16, 2021 · 1 comment
Open

Add z3 integration #13

grantjenks opened this issue Feb 16, 2021 · 1 comment

Comments

@grantjenks
Copy link
Owner

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

@grantjenks
Copy link
Owner Author

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 >.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant