以SMT2格式保存Z3求解器的状态(&Q) [英] Saving the "state" of a Z3 solver in SMT2 format

问题描述

是否可以使用Z3 API(例如，Python API)将求解器的当前状态保存到SMT2格式的文件中，包括求解器已学习的内容(在SAT求解中，我们称其为"已学习的子句")？

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

提前表示感谢...

推荐答案

SMT2没有规定保存给定的求解器状态，这无疑会因求解器的不同而大不相同。但是，每个求解器可能有不同的执行此操作的机制，但它肯定不会是SMTLib2格式。

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

这篇关于以SMT2格式保存Z3求解器的状态(&Q)的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！