是否可以使用Z3 API（例如Python API）将求解器的当前状态保存到SMT2格式的文件中，包括求解器已了解的内容（在SAT求解中，我们会称其为“学习的子句”）？
因为我希望能够将求解器的状态保存在一个临时文件中以便以后恢复求解，所以我有时间了解我应该对它进行哪些进一步的查询。
提前谢谢了...
最佳答案
SMT2没有保存给定求解器状态的规定，这无疑会因求解器而异。每个求解器可能具有不同的机制，但是绝对不会采用SMTLib2格式。
由于您的问题完全是Z3特有的，所以我建议在https://github.com/Z3Prover/z3/issues上询问它是否可能有任何有趣的问题。据我所知，这目前尚不可能。
关于python - 以SMT2格式保存Z3求解器的“状态”，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/44110746/