z3 - Z3 上下文序列化/反序列化？

Question

是否可以序列化/反序列化 Z3 上下文（来自 C#）？如果没有，是否计划使用此功能？

我认为此功能对于现实世界的应用程序很重要。

Answer 1

当前 API 不直接支持此功能。下一个版本将支持多个求解器，我们将提供将断言从一个求解器复制到另一个求解器并检索断言的命令。使用这些命令，可以通过将表达式转储到文件（SMT 2.0 格式）中来实现序列化。要反序列化，我们只需将文件读回即可。请注意，如果您跟踪您在逻辑上下文中断言的断言，则该解决方案已经可以使用当前 API 实现。

话虽如此，我已经看到在许多使用 Z3 的项目中使用了以下方法。他们有自己的公式表示。当他们调用 Z3 时，他们将他们的表示转换为 Z3 的表示。在大多数情况下，性能开销是最小的。这种方法给了他们很大的灵活性。序列化就是一个很好的例子。一些编程环境（例如，Python）已经为序列化提供了一些内置支持。