Algebraic data types (ADTs) are a construct classically found in functional programming languages that capture data structures like enumerated types, lists, and trees. In recent years, interest in ADTs has increased. For example, popular programming languages, like Python, have added support for ADTs. Automated reasoning about ADTs can be done using satisfiability modulo theories (SMT) solving, an extension of the Boolean satisfiability problem with constraints over first-order structures. Unfortunately, SMT solvers that support ADTs do not scale as state-of-the-art approaches all use variations of the same \emph{lazy} approach. In this paper, we present an SMT solver that takes a fundamentally different approach, an \emph{eager} approach. Specifically, our solver reduces ADT queries to a simpler logical theory, uninterpreted functions (UF), and then uses an existing solver on the reduced query. We prove the soundness and completeness of our approach and demonstrate that it outperforms the state-of-theart on existing benchmarks, as well as a new, more challenging benchmark set from the planning domain.

翻译：代数数据类型（ADTs）是函数式编程语言中经典的一种构造，用于封装枚举类型、列表和树等数据结构。近年来，人们对ADTs的兴趣日益增长。例如，像Python这样的流行编程语言已增加了对ADTs的支持。关于ADTs的自动推理可以通过可满足性模理论（SMT）求解实现，该理论是布尔可满足性问题在带一阶结构约束上的扩展。然而，支持ADTs的SMT求解器在可扩展性上存在不足，因为当前最先进的方法均采用同一类“懒惰”方法的变体。本文提出一种采用根本性不同方法（即“急切”方法）的SMT求解器。具体而言，我们的求解器将ADTs查询简化为一种更简单的逻辑理论——未解释函数（UF），然后使用现有求解器处理简化后的查询。我们证明了该方法的同时，证明了其可靠性和完备性，并展示了其在现有基准测试以及来自规划领域的新颖、更具挑战性的基准测试集上优于当前最先进方法的表现。