Implement true floating point semantics

[pschanely]

One big gotcha with CrossHair and floats: For performance reasons CrossHair approximates floating point behavior using true (arbitrary precision) real numbers.

Z3 is technically capable of doing floating-point-accurate symbolic execution. However, those capabilities are very slow; it might take O(minutes) to reason about a single floating point operation. In an ideal world, we might try both approaches.

Originally posted by @pschanely in #188 (comment)