Rewrite and reduce ATL formula

[NicEastvillage]

Many optimizations can be done by rewriting the ATL formula. If we can reduce it to simply true or false then we do not even need to run the certain-zero algorithm. This feature requires an investigation of boolean formula equivalences and an extensible design that can apply rewriting rules repeatedly.

A few example rewrites:

• A & !A → false
• A | !A → true
• A & (A | B) → A
• A & (!A | B) → A & B
• <<p1>> (true U A) → <<p1>> F A
• <<p1>> F false → false
• ...

[NicEastvillage]

Highly related to #216. Probably same phase of compiler