序列化Z3 Python对象

Question

未来的版本中是否考虑支持对Z3对象进行序列化（也就是“打包”）？我现在正在尝试将Z3 Python API生成的模型保存到文件中，但遇到了错误信息ctypes objects containing pointers cannot be pickled，我理解这意味着Python API只是Z3 DLL的一个包装。

或者有没有更好的方法可以将Z3 Python API生成的对象保存到文件中，以便将来使用？

谢谢！

Answer 1

没错，Z3的Python接口其实是对Z3共享库的一个封装（在Windows上就是一个DLL文件）。我们可以给Z3的Python对象（比如那些用来表示公式、模型等的对象）添加一些方法，比如__getstate__()和__setstate(state)__。如果这些方法存在，Python在保存对象时就会用到它们。

从理论上讲，这个功能是可以添加的。也就是说，我们可以在Z3的API（C语言的接口）中增加一些程序，用来把Z3的表达式、公式和模块转换成字节流。这些API会被用来实现__getstate__()和__setstate(state)__。这里有一些细节：

• 共享: 假设我们有一个包含Z3表达式的Python列表，而这些表达式之间有很多相同的子表达式。Python在保存这个列表时，会对每个元素调用__getstate__()，这时Z3会多次编码那些共享的子表达式。问题在于，对于Python来说，每个Z3表达式都是一个“块”，而Z3的编码器并不知道这些不同的表达式其实是一个更大的Python数据结构的一部分。所以，当我们保存一个包含多个不同Z3对象的Python对象时，用户需要小心。值得注意的是，在某些情况下，这个问题是比较好解决的。例如，我们可以使用Z3的ASTVector，而不是Python的Z3表达式列表。这样，Z3就可以把ASTVector作为一个大的“块”来编码，每个共享的子表达式只会被编码一次。

• Z3对象，比如表达式和模型，是和一个上下文相关联的。注意，Python API中的大多数程序都有一个额外的ctx参数。例如，Int('x')会在默认上下文中创建一个名为x的整数变量，而Int('x', ctx)则是在上下文ctx中创建它。多个上下文是有用的，因为我们可以从不同的执行线程同时访问它们。当我们反序列化一个Z3对象时，我们需要决定将它存储在哪个上下文中。一个可能的办法是设置一个全局参数，来指定使用哪个上下文。如果没有设置，就会使用默认上下文。这并不是一个完美的解决方案。假设我们有一个Python数据结构，里面包含了来自不同上下文的Z3表达式的引用，然后我们保存了它。等我们反序列化这个数据时，所有表达式都会被放到同一个Z3上下文中。也许这并不是个大问题，因为大多数用户只使用一个Z3上下文，而那些使用多个上下文的用户通常不会在同一个Python对象中存储来自不同上下文的表达式引用。

如果你有其他解决方案，欢迎随时提出。Z3团队的成员中没有人是Python专家。