Open
Description
We've had a number of simplifier related issues pop up in the past. It's not sustainable to keep adding in each new simplify feature into our existing implementation. Here's a thread summarizing the various issues:
- Arbitrary algebraic simplification: currently we have our own implementation. However, every time we want a new simplification, we need to manually implement it (More simplify issues #335).
- No support for branch elimination (delete_config and assert_if should be part of simplify #117): our current hacky solution is
assert_if. - Simplify is becoming a really big one-size-fits-all hammer. It would be nice to be able to toggle certain optimizations (Enable/disable certain optimizations in simplify #119).
One idea for tackling these issues is to offload simplify to an SMT solver. Alex explored this a bit (#319), but ran into issues with the SMT solver