Z3Python: StringSort support

问题:

I'm building a symbolic execution engine for Python using Z3 with it's Python module.

I need to reason about strings, but it doesn't appear to be supported in the current API for Python

I found it can be done somehow: https://github.com/cs-au-dk/Artemis/tree/master/contrib/Z3-str

How can I get Z3 to reason about strings using it's python API? (maybe extend it?)

If not possible, though I may try to implement it as arrays of ints (where each int represents a char in the string) and write some helpers to reason about them. Would that work?

I'm using the 4.3.2 version with python3.

回答1:

The link you found is Z3-str, which is a theory plug-in on Z3. Z3-str was implemented using the External Theory Plugins API (for C) of an old version of Z3. These plugin APIs are deprecated in Z3 4.3.2.