用 Rust 和 Z3 自动合成无循环程序

Synthesizing Loop-Free Programs with Rust and Z3 (2020)

手动编写某些底层程序既繁琐又容易出错，比如仅用三条指令隔离最右侧零位。我尝试用 Rust 实现了一个程序合成器，利用 Z3 求解器自动寻找满足规格的程序。这种方法基于 Gulwani 等人的研究，采用反例引导的迭代合成（CEGIS）策略，专注于无循环且基于组件的程序构建。通过限定组件库，合成器能高效重连输入输出，自动发现最优指令序列。这不仅适用于编译器中的 Peephole 优化器生成，还能在复杂位运算问题上超越人工效率。虽然目前在某些高难度基准测试上性能仍有待优化，但这为自动化代码生成提供了新的思路。