Argument Reduction of Constrained Horn Clauses Using Equality Constraints

Constrained Horn Clauses (CHCs) have recently been studied extensively as a common, uniform foundation for automated program verification. Various program verification problems have been shown to be reducible to CHC solving, and accordingly, CHC solvers have been developed by several research groups. We propose a new optimization method for CHC solving, which reduces the number of predicate arguments by finding (conditional) equality constraints among the predicate arguments. The optimization is especially effective for data-driven CHC solvers such as HoIce, as it significantly reduces the number of data required to infer a solution for CHCs. We have implemented our method and confirmed its effectiveness through experiments.