Constraint simplification

[CatarinaGamboa]

We need to improve the simplification of expressions with various variable instances.
We could try to do something similar to constant propagation, and to flattening variable derivation chains.

For example:

Here I would want the most simplified version to be something like "b >= 100 && b + 100" is not a subtype of Byte(b). Then

We could try using constraint simplification via equivalence analysis, as an algorithm like:

1. Find equivalences (in variables for this case)
2. Pick canonical names - use vars from code and not internal vars if possible
3. Substitute Equivalences - Simplify equivalences, remove duplicate checks
4. Remove redundancies

In that example:

1. Equivalences: {b, b_34, b_38}
2. Use b

#b_39 == #b_38 + 100  →  #b_39 == b + 100
#b_38 == #b_34        →  (redundant, defines equivalence)
#b_34 >= 100          →  b >= 100
b > 0                 →  b > 0
#b_34 > 0             →  b > 0  (duplicate)
b == #b_34            →  (redundant, defines equivalence)

simplifies to
#b_39 == b + 100 && b >= 100 && b > 0
4) b > 100 -> b > 0 so we can drop the weaker constraint.

This has to be in coordination with liquidjava verifier.
This is open for discussion!