Pickling Z3 Python Objects

Question

Is support for pickling (or serializing) Z3 objects being considered for future releases? I am currently trying to pickle the model produced by the Z3 Python API to a file, and I get the error message ctypes objects containing pointers cannot be pickled, which I take to mean that the Python API is merely a wrapper around the Z3 DLL.

Or is there a better way to save the objects produced by the Z3 Python API to files for future use?

Thanks!

Answer 1

Yes, the Z3 Python API is a wrapper over the Z3 shared library (i.e., a DLL on Windows). It is feasible to add methods __getstate__() and __setstate(state)__ to the Z3 Python objects that wrap formulas, models, etc. If these methods are available, the Python pickler will use them. So, in principle, this functionality can be added. That is, we can add to the Z3 API (the C API) procedures for encoding/decoding Z3 expressions/formulas and modules into byte streams. These APIs are then used in to implement __getstate__() and __setstate(state)__. There are some details:

• Sharing: suppose we have a Python list of Z3 expressions, and these expressions share a lot of sub-expressions. The Python pickler would invoke __getstate__() for each element of the list, and Z3 would encode the shared sub-expressions multiple times. The problem is that, for Python, each Z3 expression is a "blob", and the Z3 encoder/serializer does not know that these different expressions are part of a bigger Python data-structure. So, users should be careful when pickling a Python object that contains references to many different Z3 objects. Note that, in some cases, it is easy to fix this issue. For example, we can use a Z3 ASTVector instead of a Python list of Z3 expressions. Then, Z3 can encode the ASTVector as one big "blob" where each shared sub-expression is encoded only once.

• Z3 objects, such as expressions and models, are associated with a context. Note that most procedures in the Python API have an extra ctx parameter. For example, Int('x') creates an integer variable named x in the default context, and Int('x', ctx) creates it in the context ctx. Multiple contexts are useful because we can concurrently access them from different execution threads. When we unpickle a Z3 object, we have to decide in which context we will store it. A possibility is to set a global parameter that specifies the context to be used. If it is not set, then the default context is used. This is not a perfect solution. Suppose we have a Python data-structure that contains references to Z3 expressions from different contexts, and we pickle it. Then, when we unpickle the data, all expressions would be added to the same Z3 context. Perhaps, this is not a big problem, since most users use only one Z3 context, and the ones that use multiple contexts usually do not store references to expressions from different contexts in the same Python object.

Please feel free to suggest alternative solutions. None of us in the Z3 team is a Python expert.