Replace quadratic equiv

[chriseth]

Replaces the "quadratic equivalence" code by a rule-based system.

TODO:

• investigate expectation difference
• check performance

[chriseth]

These differences appeared before the old code was removed, will investigate.

[chriseth]

Ah nice, the rules capture some more cases because of the fact that e * (e + off) = 0 is considered both in the form
expr: e, offset: off and expr: e + off, offset: -off, but the old code did not have that.

[chriseth]

Performance is good. It takes 250 ms on keccak when run before the solver runs (which is currently not the case).

The keccak test goes down from 17.3 seconds to 13.3.