Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties

TL;DR

This paper introduces modular, flexible algorithms for computing congruence closure over AC symbols with semantic properties, improving efficiency and integration into SMT solvers.

Contribution

It presents novel, modular algorithms for AC congruence closure that do not rely on complex orderings or unification, extending to various algebraic properties.

Findings

Algorithms are modular and simple to prove correct.

They do not require complex AC compatible orderings.

Suitable for integration into SMT solvers.

Abstract

Algorithms for computing congruence closure of ground equations over uninterpreted symbols and interpreted symbols satisfying associativity and commutativity (AC) properties are proposed. The algorithms are based on a framework for computing a congruence closure by abstracting nonflat terms by constants as proposed first in Kapur's congruence closure algorithm (RTA97). The framework is general, flexible, and has been extended also to develop congruence closure algorithms for the cases when associative-commutative function symbols can have additional properties including idempotency, nilpotency, identities, cancellativity and group properties as well as their various combinations. Algorithms are modular; their correctness and termination proofs are simple, exploiting modularity. Unlike earlier algorithms, the proposed algorithms neither rely on complex AC compatible well-founded orderings on nonvariable terms nor need to use the associative-commutative unification and extension rules in completion for generating canonical rewrite systems for congruence closures. They are particularly suited for integrating into the Satisfiability modulo Theories (SMT) solvers. A new way to view Groebner basis algorithm for polynomial ideals with integer coefficients as a combination of the congruence closures over the AC symbol * with the identity 1 and the congruence closure over an Abelian group with + is outlined.