Implementation of a Fast Congruence Closure Algorithm

Abstract

In this paper an abstract algorithm for computing the congruence closure of a set of ground equations using the standard union-find infrastructure is given as well as an abstract algorithm that decides whether a ground equation is a semantic consequence of a set of ground equations using the output of the congruence closure algorithm. Furthermore an efficient C++ implementation of both algorithms is given using fast weighted union and long find with path compression. Additionally we argue that the given congruence closure algorithm runs in O(n log n) time for n being the total size of the input equations and that the decision algorithm performs in linear time in the size of the equation that is to be checked, independently of the size of the equations that induced the congruence closure.

Category: Miscellaneous