0

目前，我对 SMT 求解器的工作原理（E-matching、MBQI 和 CVC4/5 的归纳推理等算法的基础知识）有一些肤浅的了解。但是，通过反复试验进行调试非常令人沮丧。

是否有关于如何调试大量使用量词的 SMT 脚本的指导？

  1. 写得不好的脚本经常陷入无限循环，但我无法判断这是我的错误，还是响应时间太长。
  2. SMT 求解器倾向于对用户隐藏内部结构，因此很难弄清楚它为什么会卡住。有没有办法打印“解决上下文”？

或者也许我以错误的方式使用 SMT 求解器？我应该设计自己的验证算法，只使用 SMT 求解器进行本地决策？

任何帮助表示赞赏！

4

1 回答 1

2

这是一个非常主观的问题，并且很大程度上基于意见。但是有几点一般性的评论：

  • 不要直接在 SMTLib 中编程。它不适合人类消费。相反，请使用更高级别的 API，并使用您更熟悉的语言编写脚本。可以从任何数量的语言中获得绑定，包括 C/C++/Java/Python/O'Caml/Haskell/Scala 等。只要这样做就可以摆脱您犯的大多数平凡错误。

  • 打开求解器的详细输出。您可能会注意到日志输出中的模式。不幸的是，这是非常特定于求解器的，并且很难破译；但也可以表明，例如，您是否在量词存在的情况下陷入电子匹配循环。

  • 如果有针对您的验证问题的自定义算法（Hoare 三元组、分离逻辑、抽象解释等），那么您首先必须应用这些技术并将本地/子引理委托给 SMT 求解器。不要指望 SMT 求解器能够进行大型证明，以及开箱即用需要实际归纳的任何事情。

  • 尝试通过施加过度约束来降低复杂性，看看哪些有帮助。例如，根据您的发现，如果过度约束枚举了一个相当小的搜索空间，您也许可以进行案例拆分。

同样，这些都是非常笼统的评论，它们是否适用于您的特定问题是任何人的猜测。但是，如果您还没有这样做的话，我会从使用更高级别的 API 编码开始。

于 2021-10-14T16:00:02.103 回答