Catamorphic Abstractions for Constrained Horn Clause Satisfiability

TL;DR

This paper introduces a method to transform sets of Constrained Horn Clauses involving catamorphisms into equivalent forms, enabling more efficient satisfiability checking and improving solver performance on list and tree algorithms.

Contribution

It presents a novel transformation technique that removes catamorphisms from CHCs, allowing existing solvers to handle complex ADT properties more effectively.

Findings

Transformation preserves satisfiability.

Significant performance improvements on benchmarks.

Effective handling of list and tree processing algorithms.

Abstract

Catamorphisms are functions that are recursively defined on list and trees and, in general, on Algebraic Data Types (ADTs), and are often used to compute suitable abstractions of programs that manipulate ADTs. Examples of catamorphisms include functions that compute size of lists, orderedness of lists, and height of trees. It is well known that program properties specified through catamorphisms can be proved by showing the satisfiability of suitable sets of Constrained Horn Clauses (CHCs). We address the problem of checking the satisfiability of those sets of CHCs, and we propose a method for transforming sets of CHCs into equisatisfiable sets where catamorphisms are no longer present. As a consequence, clauses with catamorphisms can be handled without extending the satisfiability algorithms used by existing CHC solvers. Through an experimental evaluation on a non-trivial benchmark consisting of many list and tree processing algorithms expressed as sets of CHCs, we show that our technique is indeed effective and significantly enhances the performance of state-of-the-art CHC solvers.