Pav*_*kov 6 compiler-construction programming-languages constraint-programming smt z3
任何或多或少的实用编程语言和编译器都必须处理约束.最常见的约束是类型.通常,类型推导和统一是通过简单的算法(例如Hindley-Milner)完成的,其中最终程序中的所有项都被赋予唯一类型.如果没有发生,则会出现错误指示.
在编译器中可能存在更复杂的约束,其中完全统一是不可能的,并且解决方案仅在某些限制下存在.可能的例子是
数据流分析.仿射相等约束的解可以用于循环矢量化.
内存管理.如果我们对引用和数据访问模式有一些约束,编译器可以从优化引用计数和垃圾收集中受益.
从另一点来看,约束求解器(如Z3或Yices)在为不同类型的约束寻找可满足的模型方面非常强大.
我正在寻找有关编译器如何从SMT求解器的强大功能以及他们正在解决的任务类型中受益的成功案例.我列出了一些区域,但我没有找到任何具体的例子.你能建议吗？