未来版本是否考虑支持酸洗（或序列化）Z3 对象？我目前正在尝试将 Z3 Python API 生成的模型腌制到一个文件中，我收到错误消息 ctypes objects containing pointers cannot be pickled，我认为这意味着 Python API 只是 Z3 DLL 的包装器。
或者有没有更好的方法将 Z3 Python API 生成的对象保存到文件中以供将来使用？
谢谢！
【问题讨论】：
是的，Z3 Python API 是 Z3 共享库（即 Windows 上的 DLL）的包装器。
将方法__getstate__() 和__setstate(state)__ 添加到包装公式、模型等的Z3 Python 对象是可行的。如果这些方法可用，Python pickler 将使用它们。
因此，原则上，可以添加此功能。也就是说，我们可以在 Z3 API（C API）中添加用于将 Z3 表达式/公式和模块编码/解码为字节流的过程。然后使用这些 API 来实现 __getstate__() 和 __setstate(state)__。有一些细节：
共享：假设我们有一个 Z3 表达式的 Python 列表，这些表达式共享很多子表达式。 Python pickler 将为列表的每个元素调用__getstate__()，并且 Z3 将对共享子表达式进行多次编码。问题在于，对于 Python，每个 Z3 表达式都是一个“blob”，并且 Z3 编码器/序列化器不知道这些不同的表达式是更大的 Python 数据结构的一部分。因此，用户在挑选包含对许多不同 Z3 对象的引用的 Python 对象时应该小心。请注意，在某些情况下，很容易解决此问题。例如，我们可以使用 Z3 ASTVector 而不是 Z3 表达式的 Python 列表。然后，Z3 可以将ASTVector 编码为一个大“blob”，其中每个共享子表达式只编码一次。
Z3 对象（例如表达式和模型）与上下文相关联。请注意，Python API 中的大多数过程都有一个额外的ctx 参数。例如，Int('x') 在默认上下文中创建一个名为 x 的整数变量，Int('x', ctx) 在上下文 ctx 中创建它。多个上下文很有用，因为我们可以从不同的执行线程同时访问它们。当我们解开 Z3 对象时，我们必须决定将它存储在哪个上下文中。一种可能性是设置一个全局参数来指定要使用的上下文。如果未设置，则使用默认上下文。 这不是一个完美的解决方案。假设我们有一个 Python 数据结构，其中包含对来自不同上下文的 Z3 表达式的引用，我们将其腌制。然后，当我们 unpickle 数据时，所有表达式都将添加到同一个 Z3 上下文中。或许，这不是什么大问题，因为大多数用户只使用一个 Z3 上下文，而使用多个上下文的用户通常不会将来自不同上下文的表达式的引用存储在同一个 Python 对象中。
请随时提出替代解决方案。我们 Z3 团队中没有一个是 Python 专家。
【讨论】：
__getstate__ 或 __setstate__ 方法？
__getstate__ 和__setstate__。我们应该补充一点。这是一个有用的功能。
sexpr 来解决这个问题。