« Changelog History


sbv v8.14 Release Notes

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

    • Improve the fast all-sat algorithm to also support uninterpreted values.

    • Generalize svTestBit to work on floats, returning the respecting bit in the representation of the float.

    • Fixes to crack-num facility of how we display floats in detail.


Previous changes from v8.13

    • Generalized floating point: Add support for brain-floats, with type SFPBFloat, which has 8-bits of exponent and 8-bits of significand. This format is affectionately called "brain-float" because it's often used in modeling neural networks machine-learning applications, offering a wider-range than IEEE's half-float, at the exponse of reduced precision. It has 8-exponent bits and 8-significand bits, including the hidden bit.

    • Add support for SRational type, rational values built out of the ratio of two integers. Use the module "Data.SBV.Rational", which exports the constructor .% to build rationals. Note that you cannot take numerator and denominator of rationals apart, since SMTLib has no way of storing the rational in a canonical way. Otherwise, symbolic rationals follow the same rules as Haskell's Rational type.

    • SBV now implements a faster allSat algorithm, which applies in most common use cases. (Essentially, when there are no uninterpreted values or sorts present.) The new algorithm has been measured to be at least an order of magnitude faster or more in common cases as it splits the search space into disjoint models, reducing the burden of accummulated lemmas over multiple calls. (See http://theory.stanford.edu/%7Enikolaj/programmingz3.html#sec-blocking-evaluations for details.)