约束求解器在编程语言和编译器中的使用

Question

任何或多或少实用的编程语言和编译器都必须处理约束。最常见的约束是类型。通常类型推导和统一是通过一个简单的算法（例如Hindley-Milner）完成的，最终程序中的所有项都被分配了唯一的类型。如果没有发生，则有错误指示。

编译器中可能存在更复杂的约束，其中不可能完全统一，并且解决方案仅在某些限制下存在。可能的例子是

• 数据流分析。仿射等式约束的解可用于循环向量化。

• 内存管理。如果我们对引用和数据访问模式有一些限制，编译器可以从优化引用计数和垃圾收集中受益。

另一方面，约束求解器，如 Z3 或 Yices，在为不同类型的约束寻找可满足模型方面非常强大。

我正在寻找有关编译器如何从 SMT 求解器的强大功能中受益以及他们正在解决什么样的任务的成功案例。我列出了一些领域，但我没有找到任何具体的例子。可以推荐吗？

Answer 1

SMT 求解器通常用于实现需要大量静态验证的编程语言。例如，使用依赖类型、细化类型或静态强制合同的语言通常使用 SMT 求解器。

例如Liquid Haskell 以及微软的Dafny 和Chalice 都使用Z3。其他语言，如 ATS 或 Whiley，实现了自己的求解器。