Unify equivalence condition simplification in the verifier

[thebendavis]

Currently we perform some simplification of equivalence conditions in the verifier itself, as well as some additional simplification/rewriting in the Binary Ninja plugin to improve the presentation for the operator. Unifying all simplification and rewriting logic into a single place would make this easier to reason about and maintain, and performing this unification in the verifier means it could be leveraged by not only the Binary Ninja plugin but also other possible consumers of verifier results.

[thebendavis]

Making simplified equivalence conditions available in the verifier will allow us to make our integration tests less exposed to low-level changes, see discussion in #417 (comment)

[jim-carciofini]

If this functionality could be implemented as a well encapsulated component, this might be a good task for me to cut my teeth on Haskel.