- English only
Lab for Automated Reasoning and Analysis LARA
This is an old revision of the document!
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
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:
- start with
- 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 .
- 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
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.