In Herbie we use e-graphs to do algebraic rewriting of mathematical expressions. For example, in the Rust standard library's acosh function, e-graphs rewrite log(sqrt(x^2 + 1))… into log(1 + sqrt(x^2 + 1) - 1) into log1p(sqrt(x^2 + 1) - 1) into log1p(x^2 / (sqrt(x^2 + 1) + 1)) into log1p(x / (sqrt(1 + (1/x)^2) + (1/x))), Still, they're bad at some things, and one that really stands out is basic sums and products. Canceling like terms, distributing products over sums, and factoring things is...
