I’ve been learning about CHR recently for this purpose (egraph rewriting https://egraphs-good.github.io/ ) and I think it’s a pretty cool application. I’d be interested to hear tips about how I might make it go faster or references to prior work in this direction.
While some users here make use of constraints, it seems only a very few understand CHR. CHR is something I need to learn but still have not.
The only thing that I can offer of help is
Tips for CHR Programming Compiled by Amira Zaki, Thom Fruhwirth, Jon Sneyers
So while many may be interested in CHR and/or E-graph rewriting, many of us would be following your lead.