An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes

Amar Shah, Federico Mora, Sanjit A. Seshia

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 ye…