We present a number of first- and second-order extensions to SMT theories specifically aimed at representing and analyzing SQL queries with join, projection, and selection operations. We support reasoning about SQL queries with either bag or set semantics for database tables. We provide the former via an extension of a theory of finite bags and the latter via an extension of the theory of finite relations. Furthermore, we add the ability to reason about tables with null values by introducing a theory of nullable sorts based on an extension of the theory of algebraic datatypes. We implemented solvers for these theories in the SMT solver cvc5 and evaluated them on a set of benchmarks derived from public sets of SQL equivalence problems.

翻译：我们提出了若干一阶和二阶SMT理论扩展，专门用于表示和分析包含连接、投影和选择操作的SQL查询。我们支持对采用包语义或集合语义的数据库表进行SQL查询推理。前者通过有限包理论的扩展实现，后者则基于有限关系理论的扩展。此外，我们通过引入基于代数数据类型扩展的可空类型理论，增加了对含空值表进行推理的能力。我们在SMT求解器cvc5中实现了这些理论的求解器，并在源自公共SQL等价性问题集的基准测试上进行了评估。