The task of SQL query equivalence checking is important in various real-world applications (including query rewriting and automated grading) that involve complex queries with integrity constraints; yet, state-of-the-art techniques are very limited in their capability of reasoning about complex features (e.g., those that involve sorting, case statement, rich integrity constraints, etc.) in real-life queries. To the best of our knowledge, we propose the first SMT-based approach and its implementation, VeriEQL, capable of proving and disproving bounded equivalence of complex SQL queries. VeriEQL is based on a new logical encoding that models query semantics over symbolic tuples using the theory of integers with uninterpreted functions. It is simple yet highly practical -- our comprehensive evaluation on over 20,000 benchmarks shows that VeriEQL outperforms all state-of-the-art techniques by more than one order of magnitude in terms of the number of benchmarks that can be proved or disproved. VeriEQL can also generate counterexamples that facilitate many downstream tasks (such as finding serious bugs in systems like MySQL and Apache Calcite).

翻译：SQL查询等价性检查在涉及完整性约束的复杂查询的多种实际应用（包括查询重写和自动评分）中至关重要；然而，现有技术在推理实际查询中的复杂特性（如涉及排序、case语句、丰富完整性约束等）方面能力极为有限。据我们所知，本文首次提出基于SMT的方法及其实现VeriEQL，能够证明和反驳复杂SQL查询的有界等价性。VeriEQL基于一种新颖的逻辑编码，该编码通过带未解释函数的整数理论对符号元组上的查询语义进行建模。该方法简洁而高度实用——我们对超过20,000个基准测试的综合评估表明，VeriEQL在可证明或反驳的基准测试数量上，比所有现有技术提升一个数量级以上。VeriEQL还能生成反例，以支持多种下游任务（例如发现MySQL和Apache Calcite等系统中的严重缺陷）。