A framework for generating congruence closure and conditional congruence closure of ground terms over uninterpreted as well as interpreted symbols satisfying various properties is proposed. It is based on some of the ...A framework for generating congruence closure and conditional congruence closure of ground terms over uninterpreted as well as interpreted symbols satisfying various properties is proposed. It is based on some of the key concepts from Kapur's congruence closure algorithm(RTA97)for ground equations based on introducing new symbols for all nonconstant subterms appearing in the equation set and using ground completion on uninterpreted constants and puri?ed equalities over interpreted symbols belonging to different theories. In the original signature, the resulting rewrite systems may be nonterminating but they still generate canonical forms. A byproduct of this framework is a constant Horn completion algorithm using which ground canonical Horn rewrite systems can be generated for conditional ground theories.New effcient algorithms for generating congruence closure of conditional and unconditional equations on ground terms over uninterpreted symbols are presented. 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 effcient and succinct interpolants for the quanti?er-free theory of equality over uninterpreted function symbols which are often a conjunction of conditional equations and need additional simpli?cation. A completion algorithm to generate a canonical conditional rewrite system from ground conditional equations is also presented. The framework is general and ?exible and is used later to develop congruence closure algorithms for cases when function symbols satisfy simple properties such as commutativity, nilpotency, idempotency and identity as well as their combinations. Interesting outcomes include algorithms for canonical rewrite systems for ground equational and conditional theories on uninterpreted and interpreted symbols leading to generation of canonical forms for ground terms, constrained terms and Horn equations.展开更多
文摘A framework for generating congruence closure and conditional congruence closure of ground terms over uninterpreted as well as interpreted symbols satisfying various properties is proposed. It is based on some of the key concepts from Kapur's congruence closure algorithm(RTA97)for ground equations based on introducing new symbols for all nonconstant subterms appearing in the equation set and using ground completion on uninterpreted constants and puri?ed equalities over interpreted symbols belonging to different theories. In the original signature, the resulting rewrite systems may be nonterminating but they still generate canonical forms. A byproduct of this framework is a constant Horn completion algorithm using which ground canonical Horn rewrite systems can be generated for conditional ground theories.New effcient algorithms for generating congruence closure of conditional and unconditional equations on ground terms over uninterpreted symbols are presented. 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 effcient and succinct interpolants for the quanti?er-free theory of equality over uninterpreted function symbols which are often a conjunction of conditional equations and need additional simpli?cation. A completion algorithm to generate a canonical conditional rewrite system from ground conditional equations is also presented. The framework is general and ?exible and is used later to develop congruence closure algorithms for cases when function symbols satisfy simple properties such as commutativity, nilpotency, idempotency and identity as well as their combinations. Interesting outcomes include algorithms for canonical rewrite systems for ground equational and conditional theories on uninterpreted and interpreted symbols leading to generation of canonical forms for ground terms, constrained terms and Horn equations.
