| Summary: | 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.
|
|---|