是否有可能使用 Z3 API(例如 Python API)保存求解器的当前状态,包括求解器学到了什么(在 SAT 求解中我们会说“学到的”条款”)在 SMT2 格式的文件中?
因为我希望能够将求解器的状态保存在一个临时文件中,以便稍后恢复求解,以便有一些时间了解我应该对其进行哪些进一步的查询。
提前致谢...
最佳答案
SMT2 没有保存给定求解器状态的规定,这无疑会因求解器而异。然而,每个求解器可能有不同的机制,但它肯定不会采用 SMTLib2 格式。
由于您的问题完全是针对 Z3 的,我建议您在 https://github.com/Z3Prover/z3/issues 上提问看看他们是否有什么有趣的事情。然而,据我所知,目前这是不可能的。
关于python - 以 SMT2 格式保存 Z3 解算器的 "state",我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/44110746/