# An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes

arXiv: https://arxiv.org/abs/2310.12234 · HTML: https://mlsanity.com/paper/2310.12234/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 5 of its 46 references that are in the map.
- First posted on arXiv 18 Oct 2023.

## Builds on (most cited first, 5 of 5)

- [Coming to Terms with Quantified Reasoning](https://mlsanity.com/paper/1611.02908/) (2016)
- [Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates](https://mlsanity.com/paper/2004.07749/) (2020)
- [Beyond the Elementary Representations of Program Invariants over Algebraic Data Types](https://mlsanity.com/paper/2104.04463/) (2021)
- [Deciding and Interpolating Algebraic Data Types by Reduction (Technical Report)](https://mlsanity.com/paper/1801.02367/) (2018)
- [The VLSAT-3 Benchmark Suite](https://mlsanity.com/paper/2112.03675/) (2021)

## Abstract (arXiv)

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 lazy approach. In this paper, we present an SMT solver that takes a fundamentally different approach, an 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.