Recall that the hybrid value modifications in the backend extend the notion of a variable-value to be in four states:
- A known constant (this was the only non-hybrid possibility before)
- A value less than some bound
- A value greater than some bound
- An unknown value
Things currently aren't very optimized. Suppose we have a variable x in the third state, i.e. we know x >= BND, where BND is some positive constant. Then, if we want to compute x > 0, we should return constant-true, not unknown. Similarly, if we multiply two large values, we should get another large value.
There's a lot of these specialized functions -- one for every operator, and for every comparator we want to know whether it's possible, or known, that e.g. x > y, or whether is possible, denoted maybe. Instead of writing these core and critical specializations by hand, it would be nice to sketch them.