一句话：提出纯函数式、静态类型的符号求值库 Grisette，以有序守卫合并路径，显著缩小约束并加速求解。
约束求解器的发展使符号编译成为关键工程负担：需将程序转换为可高效求解的约束。Grisette 是面向领域特定符号编译器的可复用符号求值框架。它对所有执行路径求值，并把路径状态合并为有序守卫（ordered-guards）范式，避免守卫互斥，使约束规模缩减约 5 倍、求解时间缩短 2 倍以上。Grisette 完全以库形式实现，无需把宿主语言整体提升到符号域；其纯函数式设计支持符号编译记忆化和与宿主库的 monadic 集成，静态类型则在编译期捕获错误。作者在 Haskell 中实现该库，并在同时压力测试符号求值与约束求解的基准上评估。
The development of constraint solvers simplified automated reasoning about programs and shifted the engineering burden to implementing symbolic compilation tools that translate programs into efficiently solvable constraints. We describe Grisette, a reusable symbolic evaluation framework for implementing domain-specific symbolic compilers. Grisette evaluates all execution paths and merges their states into a normal form that avoids making guards mutually exclusive. This ordered-guards representation reduces the constraint size 5-fold and the solving time more than 2-fold. Grisette is designed entirely as a library, which sidesteps the complications of lifting the host language into the symbolic domain. Grisette is purely functional, enabling memoization of symbolic compilation as well as monadic integration with host libraries. Grisette is statically typed, which allows catching programming errors at compile time rather than delaying their detection to the constraint solver. We implemented Grisette in Haskell and evaluated it on benchmarks that stress both the symbolic evaluation and constraint solving.
@article{paperbot2100,
title = {Grisette: Symbolic Compilation as a Functional Programming Library},
author = {Sirui Lu and Rastislav Bodík},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571209}
}