Venue:      Room 337, Building 5, State Key Laboratory of Computer Science,Institute of Software, Chinese Academy of Sciences

 

 

 

Algorithms for generating congruence closure of conditional and unconditional equations on ground terms with uninterpreted and interpreted symbols are presented. A framework for generating  conditional equivalence closure of constant equations and constant Horn equations is discussed building on Tarjan's Union Find algorithm. A rewrite framework for generating a canonical constant Horn rewrite rules is given. This framework is then extended to include non-constant function symbols. Uninterpreted terms are flattened using new constants whereas equalities over interpreted terms belonging to the same theory are analyzed. The framework is general and flexible and can be used to develop congruence closure algorithms for cases when function symbols satisfy properties such as commutatively, associativity and commutativity, and/or idempotency and identity.Since the crucial  property exploited in congruence closure algorithm by Downey, Sethi and Tarjan as well as by Kapur (RTA97) is non-constant terms having unique signatures, signature computations are extended to ensure this property for extensions to interpreted symbols.The complexity of the conditional congruence closure is shown to be $O(n*log(n))$, which is the same as for unconditional ground equations. The proposed algorithm is motivated by our attempts to generate efficient and succinct interpolants for the quantifier-free theory of equality over uninterpreted function symbols which are often a conjunction of conditional equations and needs additional simplification.