• English only

# Lab for Automated Reasoning and Analysis LARA

This is an old revision of the document!

# Congruence Closure Algorithm and Correctness

## Congruences on all Ground Terms

Let be a set of ground equalities and disequalities representing the formula

Then the following are equivalent:

• is satisfiable
• there exists a congruence on ground terms in which is true
• is true in the least congruence containing

## Congruences on Ground Terms Occurring in the Formula

Instead of a congruence on the (typically infinite) set of all ground terms, we compute congruences on the set of the ground terms ocurring in .

Note that and that applying reflexivity, symmetry, transitivity keeps the relation in .

We need modify congruence condition to apply only to terms in , using the following congruence condition:

Algorith:

• apply the congruence rule above as well as reflexivity, symmetry and transitivity until the fixpoint
• denote result by .

Theorem: conjunction of formulas in is satisfiable iff for each we have .

Proof:

• for each pair we have that is a semantic consequence of
• we use to construct a structure in which holds
• take as domain the equivalence classes of ; let denote the equivalence class of
• define as if , and arbitrary otherwise

## Implementing Congruence Closure

Congruence is an equivalence relation, so the algorithm is a special case of union-find algorithms for finding partitions.

We represent expressions as directed acyclic graphs, which are syntax trees for expressions, with sharing. This data structure is called E-graph.

Within this structure we have union of inverted trees, representing union-find data structure.

Inverted tree representing equivalence classes.

Example: Let denote with -fold application of . Consider

Apply the congruence closure algorithm to check its satisfiability.