python - 酸洗 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 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 对象时应该小心。请注意，在某些情况下，很容易解决此问题。例如，我们可以使用 Z3ASTVector而不是 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 专家。