python - 以 SMT2 格式保存 Z3 解算器的 "state"

Question

是否有可能使用 Z3 API(例如 Python API)保存求解器的当前状态，包括求解器学到了什么(在 SAT 求解中我们会说“学到的”条款”)在 SMT2 格式的文件中？

因为我希望能够将求解器的状态保存在一个临时文件中，以便稍后恢复求解，以便有一些时间了解我应该对其进行哪些进一步的查询。

提前致谢...

Answer 1

SMT2 没有保存给定求解器状态的规定，这无疑会因求解器而异。然而，每个求解器可能有不同的机制，但它肯定不会采用 SMTLib2 格式。

由于您的问题完全是针对 Z3 的，我建议您在 https://github.com/Z3Prover/z3/issues 上提问看看他们是否有什么有趣的事情。然而，据我所知，目前这是不可能的。