Semantic Congruence Closure Algorithms

serves as a glue in fast decision procedures based on the satisfiability modulo theory framework. In 1997, an approach for generating congruence closure of uninterpreted symbols was proposed by generating a canonical rewrite system on constants by abstracting nonconstant subterms in ground equations. This framework is not only time and space efficient, but generates canonical forms with respect to the congruence closure relation. Algorithms based on this have been integrated well into SMT solvers. This talk will discuss how semantic properties of function symbols, including commutativity, idempotency, nilpotency and identity, as well as associative-commutative can also be considered without having to need any sophisticated machinery, such as associative-commutative unification, associated compatible termination orderings and associative-commutative completion, typically needed for generating canonical rewrite systems of ground equations with asssocative-commutative function symbols. The use of semantic congruence closure for generating uniform interpolants if they exist will be shown; interpolants have been found useful for automatically generating loop invariants of programs.