CC(X): Semantic Combination of Congruence Closure with Solvable Theories

We present a generic congruence closure algorithm for deciding ground formulas in the combination of the theory of equality with uninterpreted symbols and an arbitrary built-in solvable theory X. Our algorithm CC(X) is reminiscent of Shostak combination: it maintains a union-find data-structure modulo X from which maximal information about implied equalities can be directly used for congruence closure. CC(X) diverges from Shostak's approach by the use of semantic values for class representatives instead of canonized terms. Using semantic values truly reflects the actual implementation of the decision procedure for X. It also enforces to entirely rebuild the algorithm since global canonization, which is at the heart of Shostak combination, is no longer feasible with semantic values. CC(X) has been implemented in Ocaml and is at the core of Ergo, a new automated theorem prover dedicated to program verification.

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Sylvain Conchon, Evelyne Contejean, Johannes Kanig, Stéphane Lescuyer
• Keywords: Congruence Closure, ENTCS 2008, Semantic Values, Shostak Combination