Constraint simplification #162

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 is open for discussion!