Kui Ren

SMT solvers are a cornerstone in numerous domains, such as program verification, repair, and synthesis. While formula simplification is a crucial preprocessing step that directly impacts solver efficiency, existing approaches predominantly rely on handcrafted heuristics. Recent advances have explored using compiler optimizations to automate and enhance formula simplifications. Despite their promise, the synergy between compiler optimizations and SMT simplifications remains insufficiently understood and underexploited. This article presents a comprehensive study of the interplay between compiler optimizations and SMT formula simplifications. We show that iterative search for optimization configurations significantly improves formula simplifications, yielding a geometric mean speed-up of 2.96 \(\times\) over default solvers and 2.12 \(\times\) over SLOT on large-scale benchmarks. We present strong evidence for the effectiveness of machine learning-based methods in automating the selection of optimization configurations tailored to specific problem instances, achieving geometric mean speed-ups of 1.15 \(\times\) over Z3 and 1.54 \(\times\) over CVC5. Finally, we discuss promising directions for improving the applicability and effectiveness of compiler optimization-driven approaches to SMT simplifications.