Improve visualization of invariants for correctness witnesses
Created by: vmordan
The following improvements should be made:
-
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)
forfalse
. -
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