Z3 上下文序列化/反序列化? [英] Z3 Context serialization/deserialization?

问题描述

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

Is it possible to serialize/deserialize a Z3 context (from C#)? If not, is this feature planned ?

我认为这个功能对于现实世界的应用程序很重要.

I think this feature is important for real world applications.

推荐答案

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

This is not directly supported in the current API. The next release will support multiple solvers, and we will provide commands for copying the assertions from one solver to another, and retrieving the assertions. With these commands, one can implement serialization by dumping the expressions in a file (in SMT 2.0 format). To deserialize, we just read the file back. Note that, this solution can already be implemented using the current API if you keep track of the assertions you asserted into the logical context.

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

That being said, I've seen the following approach used in many projects that use Z3. They have their own representation for formulas. When they invoke Z3, they translate their representation into Z3's representation. In most cases the performance overhead is minimal. This approach gives them a lot of flexibility. Serialization is a good example. Some programming environment (e.g., Python) already provide some built-in support for serialization.

这篇关于Z3 上下文序列化/反序列化?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！