Deciding and Interpolating Algebraic Data Types by Reduction (Technical Report)

TL;DR

This paper presents a simple reduction-based method for deciding satisfiability of algebraic data type constraints, enabling decision procedures and Craig interpolation in ADTs within SMT solving.

Contribution

It introduces a straightforward reduction of ADT constraints to EUF and LIA, facilitating decision procedures and interpolation in algebraic data types.

Findings

Reduction approach enables decision procedures for ADTs.

Supports Craig interpolation in ADT extensions.

Integrates with SMT solvers for improved reasoning.

Abstract

Recursive algebraic data types (term algebras, ADTs) are one of the most well-studied theories in logic, and find application in contexts including functional programming, modelling languages, proof assistants, and verification. At this point, several state-of-the-art theorem provers and SMT solvers include tailor-made decision procedures for ADTs, and version 2.6 of the SMT-LIB standard includes support for ADTs. We study an extremely simple approach to decide satisfiability of ADT constraints, the reduction of ADT constraints to equisatisfiable constraints over uninterpreted functions (EUF) and linear integer arithmetic (LIA). We show that the reduction approach gives rise to both decision and Craig interpolation procedures in (extensions of) ADTs.