Non-Ground Congruence Closure
Hendrik Leidinger, Christoph Weidenbach
TL;DR
The paper tackles the exponential grounding bottleneck in congruence closure by introducing CC($\mathcal{X}$), a non-ground congruence closure that reason over a finite ground term set $\mathcal{M}$ using constrained terms. It formalizes a complete, sound calculus with Merge and Deduction rules, augmented by subsumption and condensation to guarantee termination and manage redundancy. The authors provide implementation refinements and an extensive evaluation showing CC($\mathcal{X}$) often outperforms classical ground CC, especially when the ground term set is large or the problem has many ground instances. The work has practical impact for SMT and related equality reasoning tasks by delaying grounding and leveraging finite ground terms, enabling scalable reasoning about non-ground equations. Future directions include handling inputs with fewer constants, optimizing class copying, and extending equality checks for non-ground terms.
Abstract
Congruence closure on ground equations is a well-established and efficient algorithm for deciding ground equalities. It constructs an explicit representation of ground equivalence classes based on a given set of input equations, allowing ground equalities to be decided by membership. In many applications, these ground equations originate from grounding non-ground equations. We propose an algorithm that directly computes a non-ground representation of ground congruence classes for non-ground equations. Our approach is sound and complete with respect to the corresponding ground congruence classes. Experimental results demonstrate that computing non-ground congruence classes often outperforms the classical ground congruence closure algorithm in efficiency.