目前，我对 SMT 求解器的工作原理（E-matching、MBQI 和 CVC4/5 的归纳推理等算法的基础知识）有一些肤浅的了解。但是，通过反复试验进行调试非常令人沮丧。
是否有关于如何调试大量使用量词的 SMT 脚本的指导？
或者我可能以错误的方式使用 SMT 求解器？我应该设计自己的验证算法，只使用 SMT 求解器进行本地决策？
感谢任何帮助！
【问题讨论】：
这是一个非常主观的问题，主要基于意见。但是有几点一般性的评论：
不要直接在 SMTLib 中编程。它不适合人类消费。相反，请使用更高级别的 API，并使用您更熟悉的语言编写脚本。可以从任意数量的语言中获得绑定，包括 C/C++/Java/Python/O'Caml/Haskell/Scala 等。这样做可以消除您犯的大部分常见错误。
打开求解器的详细输出。您可能会注意到日志输出中的模式。不幸的是，这是非常特定于求解器的，并且很难破译；但也可以指出，例如，在量词存在的情况下，您是否陷入了电子匹配循环。
如果有针对您的验证问题的自定义算法（Hoare 三元组、分离逻辑、抽象解释等），那么您首先必须应用这些技术并将本地/子引理委托给 SMT 求解器。不要指望 SMT 求解器能够进行大型证明，以及开箱即用需要实际归纳的任何事情。
尝试通过设置过度约束来降低复杂性，看看哪些有帮助。根据您的发现，您也许可以进行案例拆分，例如，如果过度约束枚举了一个相当小的搜索空间。
同样，这些都是非常笼统的评论，它们是否适用于您的特定问题是任何人的猜测。但如果你还没有这样做的话，我会先在更高级别的 API 中编码。
【讨论】：