An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes
This addresses a bottleneck in automated reasoning for ADTs, which is important for programming language verification and planning, but is incremental as it builds on existing SMT solving techniques.
The paper tackled the scalability problem of SMT solvers for algebraic data types (ADTs) by introducing an eager approach that reduces ADT queries to uninterpreted functions, and demonstrated that it outperforms state-of-the-art solvers on existing and new benchmarks.
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.