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.