Supplementary z3 simplification projects

[Notselwyn]

Hey all, I recently opened a #7397 with simplifications critical for my application, but heard from the maintainer that such simplifications will never be implemented.

Does there happen to be an existing project which aims to extend z3 simplifications? For context, I'm using Python, and the simplifications I'm looking for are in #7397.

[philzook58]

I am tinkering on something related https://github.com/philzook58/knuckledragger , but it probably isn't where you need it to be.

There is functionality for reusing the z3 simplifier tactics here https://github.com/philzook58/knuckledragger/blob/05da06c980ff5e1788245463585da2059c422f54/kdrag/utils.py#L8

Tinkering with round tripping python z3 asts through egglog https://github.com/philzook58/knuckledragger/blob/main/kdrag/solvers/untrusted.py https://www.philipzucker.com/egglog_z3_simp/
and maude https://fadoss.github.io/maude-bindings/

Unclear if this is worth the clunkiness of the round trip.

Slowly working on a pattern matcher and unifier https://github.com/philzook58/knuckledragger/blob/05da06c980ff5e1788245463585da2059c422f54/kdrag/utils.py#L29 which could be used to implement your own rewrite rules in combination with z3.substitute. For example some bitvector rewrite theorems https://github.com/philzook58/knuckledragger/blob/main/kdrag/theories/bitvec.py