« Changelog History


sbv v8.11 Release Notes

Release Date: 2021-03-09 // about 3 years ago

    • SBV now supports floating-point numbers with arbitrary exponent and significand sizes. The type is SFloatingPoint eb sb, where eb and sb are type-level naturals. In particular, SBV can now reason about half-floats, which are used much more frequently in ML applications. Through the LibBF binding, you can also use these concretely, so if you have a use case for computing with floats, you can use SBV as a vehicle for doing so. The exponent/significand sizes are limited to those supported by the LibBF bindings, though the allowed range is rather large and should not be a limitation in practice. (In particular, you'll most likely run out of memory before you hit precision limits!)

    • We now support a separate crackNum parameter in model display. If set to True (default is False), SBV will display numeric values of bounded integers, words, and all floats (SDouble, SFloat, and the new SFloatingPoint) in models in detail, showing how they are laid out in memory. Numbers follow the usual 2's-complement notation if they are signed, bit-vectors if they are not signed, and the floats follow the usual IEEE754 binary layout rules. Similarly, there's now a function crack :: SBV a -> String that does the same for non-model printing contexts.

    • Changed the isNonModelVar config param to take a String (instead of Text). Simplifies programming.

    • Changes to make SBV compile with GHC9.0. Thanks to Ryan Scott for the patch.