Congruence Closure with Integer Offsets

摘要

Congruence closure algorithms for deduction in ground equa-tional theories are ubiquitous in many (semi-)decision procedures used for verification and automated deduction. They are also frequently used in practical contexts where some interpreted function symbols are present. In particular, for the verification of pipelined microprocessors, in many cases it suffices to be able to deal with integer offsets, that is, instead of only having ground terms t built over free symbols, all (sub)terms can be of the form t + k for arbitrary integer values k. In this paper we first give a different very simple and clean formulation for the standard congruence closure algorithm which we believe is of interest on itself. It builds on ideas from the abstract algorithms of [Kap97,BTOO], but it is easily shown to run in the best known time, O(n log n), like the classical algorithms [DST80,NO80,Sho84]. After that, we show how this algorithm can be smoothly extended to deal with integer offsets without increasing this asymptotic complexity.