Can optimize sorts of arithmetic expressions on bounded types

[Bart Bogaerts]

Currently, the type of (x+y) is derived to be int or nat, even when both x and y are bounded. This could be optimized to [xmin+ymin, xmax+ymax]. (or can even be further optimizedThe same holds for product, minus, div,

Also, the same holds for aggregates,...

The reason for this is that type-derivation should be safe, therefore often \mathbb{N} or \mathbb{Z} are derived as types. However, once we have a structure, we might do better type derivation.

In summary: our system would do the following: * Do symbolic type-derivation * Generate BDD's (symbolic bounds) * Improve bounds or type-derivation using the structure (maybe by introducing new types (type a + type b, type a union type b,...)

--> this last step could also be done symbolicly...

[Bart Bogaerts]

Closing issue, see #128