Allow Cryptol's constraint solver to issue warnings

[yav]

Currently the solver can produce an error, if it notices that something is unsolveable. However, it cannot produce a warning, if something is solvable but "iffy".

This would be handly if we wanted to notify users when they've used a class instance that might have a surprising behavior.

A concrete example: overloaded fractional literals. Some fractions do not fit in some floating point representations exactly. I implemented a design where such fractions resulted in an error. This is not very nice, however, as it is extremely common to end up with numbers that are not representable exactly. I imagine in many cases this is not an issue, however, and often the closest representable number is not very readable at all. So I think it is better to allow such literals, but issue a warning, to let the user know that some rounding occurred.

[brianhuffman]

I we have a warning for writing things like non-exact floating point literals, then I hope we will also have a way to write explicitly non-exact "I meant to do this" floating point literals that will not produce a warning.

In general, I think every time we have an "I'm not sure if this is what you really meant to do" warning, there should always be a way for the programmer to make the code more explicit to avoid the warning.

[robdockins]

No pressing need for this.