Synchronizing Constrained Horn Clauses
Dmitry Mordvinov, Grigory Fedyukovich · EPiC series in computing · 2018
Simultaneous occurrences of multiple recurrence relations in a system of non-linear constrained Horn clauses are crucial for proving its satis ability. A solution of such system is often inexpressible in the constraint language. We propose to synchronize recurrent computations, thus increasing the chances for a solution to be found. We introduce a notion of CHC product allowing to formulate a lightweight iterative algorithm of merging recurrent computations into groups and prove its soundness. The evaluation over a set of systems handling lists and linear integer arithmetic confirms that the transformed systems are drastically more simple to solve than the original ones.