I've recently been on a tear writing about Egraphs modulo T, first writing about polynomials specifically and later about the general case. My main insight is that pattern-matching, specifically relational e-matching, is related to quantifier elimination and the related notion of cell decomposition, which in fact lots of theories have. So I wanted to try to make this explicit in one of the easiest possible cases: linear equations. LIN-graphs A LIN-graph has terms which are linear combinations...
