Etching Z3 Python Objects

Yes, the Z3 Python API is a wrapper around the Z3 shared library (i.e. DLL on Windows). It is possible to add methods __getstate__()

and __setstate(state)__

to Z3 Python objects that wrap formulas, models, etc. If these methods are available, their Python sorter will use them. So, in principle, this functionality can be added. That is, we can add to the Z3 API (C API) procedures to encode / decode Z3 expressions / formulas and modules into byte streams. These APIs are then used to implement __getstate__()

and __setstate(state)__

. There are several details:

• Shared: Suppose we have a list of Z3 expressions in Python, and those expressions have many subexpressions. The Python thumbnail will call __getstate__()
  
  for each list item, and Z3 will encode common subexpressions multiple times. The problem is that for Python every Z3 expression is a "blob" and the Z3 encoder / serializer doesn't know that these different expressions are part of a larger Python data structure. Thus, users should be careful when pickling a Python object that contains references to many different Z3 objects. Note that in some cases this is easy to fix. For example, we can use Z3 ASTVector
  
  instead of the Z3 Python list of expressions. Z3 can then encode ASTVector
  
  as one big blob,where each generic subexpression is encoded only once.

• Z3 objects such as expressions and models are associated with context. Note that most procedures in the Python API have an additional parameter ctx
  
  . For example, Int('x')
  
  creates an integer variable named x
  
  in the default context and Int('x', ctx)
  
  creates it in the contextctx
  
  ... Multiple contexts are useful because we can access them simultaneously from different threads of execution. When we unpack the Z3 object, we have to decide in which context we will save it. It is possible to set a global parameter that determines the used context. If not set, 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 break it down. Then, when we unpack the data, all expressions will be added to the same Z3 context. This may not be a big problem, since most users only use one Z3 context, and those using multiple contexts usually don't store references to expressions from different contexts in the same Python object.

Please feel free to suggest alternative solutions. None of us on the Z3 team are Python experts.