【发布时间】：2017-05-22 10:36:46
【问题描述】：
是否有可能使用 Z3 API（例如 Python API）来保存求解器的当前状态，包括求解器所学的内容（在 SAT 求解中，我们会说“已学子句”）在 SMT2 格式的文件中？
因为我希望能够将求解器的状态保存在一个临时文件中，以便以后继续求解，以便有时间了解我应该对其进行哪些进一步的查询。
提前非常感谢...
【问题讨论】：
【发布时间】：2017-05-22 10:36:46
【问题描述】：
SMT2 没有保存给定求解器状态的规定，这无疑会因求解器而异。然而，每个求解器可能有不同的机制，但它肯定不会是 SMTLib2 格式。
由于您的问题完全针对 Z3，我建议您在 https://github.com/Z3Prover/z3/issues 上提问，看看他们是否有什么有趣的事情。然而，据我所知，目前这是不可能的。
【讨论】：
-
非常感谢 Levent！我的想法是所谓的学习子句应该只是求解器添加的一些附加断言，就像SAT求解中的学习子句，我错了吗？如果没有，有没有办法以某种方式打印它们？即使不是 SMT2 格式（我更喜欢 SMT2 格式只是为了更舒服）
-
即使这是可能的，它无疑会引用许多在求解器执行上下文之外没有意义的内部变量/数据结构。至少绝对不是任何文本/ASCII格式。不过，在 z3 github 页面上询问是您最好的选择，看看他们是否有任何建议。
-
@LeventErkok 我不明白你的意思，子句只是子句..应该有哪些数据结构？
-
@PatrickTrentin 我怀疑求解器会将其学习的引理表示为可以以 SMTLib 或 ASCII 可读格式轻松转储的子句。它将在求解器内部数据类型中，几乎不可能按照 OP 的要求呈现给外部使用。
-
@LeventErkok 我不明白你想象的这个内部数据类型是什么，在其他求解器中我只体验过它的一些索引、向量和映射，但是它们有一个非常简单的映射to 子句.. 在这些求解器中，相同的表示用于外部和内部生成的。
最后，Levent 是对的 :)
以下是来自 Z3 github 网站的 Nikolaj Bjorner 的一些观察。
"求解器的状态不能完全序列化为 SMT2 格式。 您可以根据当前断言将求解器打印为 smt2 格式， 在 Solver 对象上使用 sexpr() 方法但未学习的子句/单位。"
...
“我们不公开打印内部状态的方法。您也许可以中断求解器，然后使用“翻译”方法克隆它并访问翻译后的求解器使用内部打印实用程序的状态。您必须稍微更改代码才能达到此状态。 求解器上的打印功能不会访问任何求解器的内部状态，而是查看断言的公式并打印它们。 我不翻译学习的引理。例如，smt_context.cpp 第 176 行中的代码被禁用，因为它对任何性能增强没有帮助。同样，sat_solver 中的复制代码不会复制学习的子句，即使它保留了学习的单元文字和二进制子句。”
您可以在link 看到 Nicolaj 的上述 cmets。
【讨论】：