Algebraic Data Types (ADTs) are a programming construct classically found in functional programming languages but are increasingly found in all kinds of modern languages. ADTs are a convenient generalization of structures like enumerated types, lists, and binary trees.

A natural problem is the satisfiability of formulas over the theory ADT. This has applications in modeling languages, proof assistants, and program verification. We propose an eager solver for ADT satisfiability modulo theory (SMT) queries via a quantifier free reduction to Equality and Uninterpreted Functions (EUF) SMT queries. This improves on existing solvers for ADT since it can be used in tandem with any SMT solver that solves EUF queries and it can be easily used in a high performance computing setting