Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types

TL;DR

This paper introduces Catalia, a novel solver that automatically synthesizes catamorphisms to improve satisfiability checking of Constrained Horn Clauses over algebraic data types, outperforming existing solvers.

Contribution

It presents a new framework for automatically discovering catamorphisms to enhance CHC solving over ADTs, with an implementation that outperforms state-of-the-art tools.

Findings

Catalia outperforms existing solvers on CHC-COMP 2024 benchmarks.

Catalia's approach enables expressing models involving inductively defined functions.

ChocoCatalia, based on Catalia, won the ADT-LIA category at CHC-COMP 2025.

Abstract

We propose a novel approach to satisfiability checking of Constrained Horn Clauses (CHCs) over Algebraic Data Types (ADTs). CHC-based automated verification has gained considerable attention in recent years, leading to the development of various CHC solvers. However, existing solvers for CHCs over ADTs are not fully satisfactory, due to their limited ability to find and express models involving inductively defined functions/predicates (e.g., those about the sum of list elements). To address this limitation, we consider catamorphisms (generalized fold functions), and present a framework for automatically discovering appropriate catamorphisms on demand and using them to express a model of given CHCs. We have implemented a new CHC solver called Catalia based on the proposed method. Our experimental results for the CHC-COMP 2024 benchmark show that Catalia outperforms state-of-the-art solvers in solving satisfiable CHCs over ADTs. Catalia was also used as a core part of the tool called ChocoCatalia, which won the ADT-LIA category of CHC-COMP 2025.