« Changelog History


sbv v8.6 Release Notes

Release Date: 2020-02-08 // about 4 years ago

    • Fix typo in error message. Thanks to Oliver Charles for the patch.

    • Fix parsing of sequence counter-examples to accommodate recent changes in z3.

    • Add missing exports related to N-bit words. Thanks to Markus Barenhoff for the patch.

    • Generalized code-generation functions to accept a function with an arbitrary return type, which was previously just unit. This allows for complicated code-generation scenarios where one code-gen run can produce input to the next.

    • Scalability improvements for internal data structures. Thanks to Brian Huffman for the patch.

    • Add interpolation support for Z3, following changes to that solver. Note that SBV now supports two different APIs for interpolation extraction, one for Z3 and the other for MathSAT. This is unfortunate, but necessary since interpolant extraction isn't quite standardized amongst solvers and MathSAT and Z3 use sufficiently different calling mechanisms to warrant their own calls. See 'Documentation.SBV.Examples.Queries.Interpolants' for examples that illustrate both cases.

    • Add a new argument to displayModels function to allow rearranging of the results in an 'allSatcall. Strictly speaking this is a backwards breaking change, but substitutingid` for the new argument gives you old functionality, so easy to work-around.