一句话：提出理论套利，将无界 SMT 约束转为有界约束以大幅加速求解。
SMT 求解器是程序分析等领域的基础工具，但实数、整数等无界约束因取值无限而难以高效求解，位向量、浮点数等有界约束则可判定且优化充分。本文提出“理论套利”，用新的抽象解释策略推断变量取值范围，将无界约束转换为有界约束；转换结果是原问题的欠近似，从而可利用有界理论的高效算法与优化。作者实现工具 STAUB，支持整数与实数理论。实验显示，单靠理论套利可将单个约束加速数量级，在非线性整数基准上平均最高加速 1.4×；它还使基于编译器优化的 SLOT 技术可用于无界 SMT 理论，额外最高加速 3×；集成到终止性证明工具后整体性能提升 9%。
SMT solvers are foundational tools for reasoning about constraints in practical problems both within and outside program analysis. Faster SMT solving improves the performance of practical tools and expands the set of tractable problems. Existing approaches to improving solver performance either focus on general algorithms applied below the level of individual theories, or focus on optimizations within a single theory. Unbounded constraints in which the number of possible variable values is infinite, such as real numbers and integers, pose a particularly difficult challenge for solvers. Bounded constraints in which the set of possible values is finite such as bitvectors and floating-point numbers, on the other hand, are decidable and have been the subject of extensive performance improvement efforts. This paper introduces a theory arbitrage: we transform unbounded constraints, which are often expensive to solve, into bounded constraints, which are typically cheaper to solve. By converting unbounded problems into bounded ones, theory arbitrage takes advantage of better performance on bounded constraints and unlocks optimization techniques that only apply to bounded theories. The transformation is achieved by harnessing a novel abstract interpretation strategy to infer bounds. The bounded transformed constraint is then an underapproximation of the semantics of the unbounded original. We realize our method for the theories of integers and real numbers with a practical tool (STAUB). Our evaluation demonstrates that theory arbitrage alone can speed up individual constraints by orders of magnitude and achieve up to a 1.4 × speedup on average across nonlinear integer benchmarks. Furthermore, it enables the use of the recent compiler optimization-based technique SLOT for unbounded SMT theories, unlocking a further speedup of up to 3 × . Finally, we incorporate STAUB into a practical termination proving tool and observe an overall 9 % improvement in performance.
@article{MikekZ24,
title = {SMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories},
author = {Benjamin Mikek and Qirun Zhang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656387}
}