Z3 offers simplify, which is really really useful. But it only works with the built in z3 rewrite rules, which are not contextual. It would be awesome to be able to add user defined rewrite rules or rewrite under solver contexts. There may be some kind of way to use a solver to get contextual rewriting but I’m not sure. There are some tactics discussed here https://microsoft.github.io/z3guide/programming/Example%20Programs/Formula%20Simplification/ but also caleb did some clever hacky worka...
