Title: Solving Horn Clauses on Inductive Data Types Without Induction,
Abstract: We address the problem of verifying the satisfiability of Constrained Horn
Clauses (CHCs) based on theories of inductively defined data structures, such
as lists and trees. We propose a transformation technique whose objective is
the removal of these data structures from CHCs, hence reducing their
satisfiability to a satisfiability problem for CHCs on integers and booleans.
We propose a transformation algorithm and identify a class of clauses where it
always succeeds. We also consider an extension of that algorithm, which
combines clause transformation with reasoning on integer constraints. Via an
experimental evaluation we show that our technique greatly improves the
effectiveness of applying the Z3 solver to CHCs. We also show that our
verification technique based on CHC transformation followed by CHC solving, is
competitive with respect to CHC solvers extended with induction. This paper is
under consideration for acceptance in TPLP.