Constrained Horn Clauses Satisfiability via Catamorphic Abstractions

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