« Changelog History


sbv v8.9 Release Notes

Release Date: 2020-10-28 // over 3 years ago

    • Rename 'sbvAvailableSolvers' to 'getAvailableSolvers'.

    • Use SMTLib's int2bv if supported by the backend solver. If not, we still do a manual translation. (CVC4 and z3 support it natively, Yices and MathSAT does not, for which we do the manual translation. ABC and dReal doesn't support the coversion at all, since former doesn't support integers and the latter doesn't support bit-vectors.) Thanks to Martin Lundfall for the initial pull request.

    • Add sym as a synonym for uninterpret. This allows us to write expressions of the form sat $ sym "a" - sym "b" .== (0::SInteger), without resorting to lambda expressions or having to explicitly be in the Symbolic monad.

    • Added missing instances for overflow-checking arithmetic of arbitrary sized signed and unsigned bitvectors.

    • In a sat (or allSat) call, also return the values of the uninterpreted values, along with all the explicitly named inputs. Strictly speaking, this is backwards-incompatible, but it the new behavior is consistent with how we handle uninterpreted values in general.

    • Improve SMTLib logic-detection code to use generics.