Pickling Z3 Python对象

Question

在未来的版本中，是否考虑对Z3对象进行酸洗（或序列化）支持？我目前正在尝试将z3pythonapi生成的模型pickle到一个文件中，得到错误消息ctypes objects containing pointers cannot be pickled，这意味着pythonapi只是z3dll的包装器。在

或者，有没有更好的方法将z3pythonapi生成的对象保存到文件中以备将来使用？在

谢谢！在

Answer 1

是的，z3pythonapi是Z3共享库（即Windows上的DLL）的包装器。 将方法__getstate__()和{}添加到包装公式、模型等的z3python对象中是可行的。如果这些方法可用，Python pickler将使用它们。 因此，原则上，可以添加此功能。也就是说，我们可以向z3api（C API）中添加用于将Z3表达式/公式和模块编码/解码为字节流的过程。然后在中使用这些api来实现__getstate__()和{}。有一些细节：

• 我们有很多共享表达式。Python pickler将为列表的每个元素调用__getstate__()，Z3将对共享子表达式进行多次编码。问题是，对于Python，每个Z3表达式都是一个“blob”，而Z3编码器/序列化程序不知道这些不同的表达式是更大的Python数据结构的一部分。因此，用户在pickle一个Python对象时应该小心，它包含对许多不同Z3对象的引用。请注意，在某些情况下，修复此问题很容易。例如，我们可以使用Z3ASTVector，而不是Z3表达式的Python列表。然后，Z3可以将ASTVector编码为一个大的“blob”，其中每个共享子表达式只编码一次。

• Z3对象，如表达式和模型，与上下文相关联。请注意，pythonapi中的大多数过程都有一个额外的ctx参数。例如，Int('x')在默认上下文中创建一个名为x的整数变量，Int('x', ctx)在上下文ctx中创建它。多个上下文很有用，因为我们可以从不同的执行线程并发地访问它们。当我们取消拾取Z3对象时，我们必须决定将其存储在哪个上下文中。一种可能性是设置一个全局参数来指定要使用的上下文。如果未设置，则使用默认上下文。这不是一个完美的解决方案。假设我们有一个Python数据结构，它包含对来自不同上下文的Z3表达式的引用，并对其进行pickle处理。然后，当我们取消拾取数据时，所有表达式都将添加到同一个Z3上下文中。也许，这不是一个大问题，因为大多数用户只使用一个Z3上下文，而使用多个上下文的用户通常不会在同一个Python对象中存储来自不同上下文的表达式的引用。

请随时提出其他解决方案。我们Z3团队中没有人是Python专家。在