如何调试具有量词的SMT脚本？

Question

目前，我对SMT求解器的工作方式有了一些肤浅的理解(E-匹配、MBQI和CVC4 4/5的归纳推理等算法的基本知识)。然而，通过尝试和错误进行调试是非常令人沮丧的。

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

1. --一个写得不好的脚本经常进入无限循环，但我不知道这是我的错误，还是太长时间才做出反应。SMT解决者
2. 倾向于向用户隐藏内部信息，所以很难弄清楚为什么会被困在里面。有没有办法打印“解题上下文”？

还是我用错了SMT解决方法？我应该设计我自己的验证算法，只使用SMT求解器进行局部决策？

任何帮助都是非常感谢的！

Answer 1

这是一个非常主观的问题，主要是基于意见。但是有几点一般性的评论：

• 不直接用SMTLib编程。它不适合人类消费。相反，使用更高级的API，并从您熟悉的语言中编写它们的脚本。任何语言都有可用的绑定，包括C/C++/Java/Python/O‘’Caml/Haskell/Scala等。只要这样做，就可以消除大多数常见的错误。

• 打开求解器的详细输出。您可能会注意到日志输出中的模式。不幸的是，这是非常具体的解决方法，而且很难破译；但也可以指示，例如，在存在量词的情况下，您是否被困在电子匹配循环中。

如果您的验证问题(Hoare三元组、分离逻辑、抽象解释，.)有自定义算法，那么首先必须应用这些技术并将局部/子引理委托给SMT求解器。不要期望SMT解决程序能够做大量的证明，以及任何需要实际归纳的东西。。

• 试图通过设置过多的约束来降低复杂性，并查看哪些约束对此有所帮助。根据您的发现，您可能可以进行案例拆分，例如，如果过度约束枚举了一个相当小的search-space.

。

同样，这些都是非常笼统的评论，它们是否会适用于你的具体问题，这是任何人的猜测。但是，如果您还没有这样做的话，我将从在高级API中进行编码开始。