Use solver to eliminate constraints in toDNF

This significantly speeds up the generation of a rewrite system for some of my benchmark code. In
the most extreme case the only generates 20k rules instead of 1.6 million.