Improve visualization of invariants for correctness witnesses

[vmordan]

The following improvements should be made:

• [x] Parse invariants as boolean expressions. It will allow to convert them to normal forms (such as CNF or DNF).
• [ ] Simplify produced boolean expressions. For example, we can substitute (1 == 0) for false.
• [ ] Support several views for invariants. The user should be able to change views on-the-fly in the visualized witness.
• [ ] Bind invariants to their scopes (such as functions) instead of first source lines.
• [ ] Extract common invariants (with corresponding scopes).

I attached a few examples of witnesses with non-trivial invariants: correctness_witnesses.zip