« Changelog History


sbv v2.0 Release Notes

Release Date: 2012-05-10 // almost 12 years ago

  • This is a major release of SBV, adding support for symbolic algebraic reals: SReal. See http://en.wikipedia.org/wiki/Algebraic_number for details. In brief, algebraic reals are solutions to univariate polynomials with rational coefficients. The arithmetic on algebraic reals is precise, with no approximation errors. Note that algebraic reals are a proper subset of all reals, in particular transcendental numbers are not representable in this way. (For instance, "sqrt 2" is algebraic, but pi, e are not.) However, algebraic reals is a superset of rationals, so SBV now also supports symbolic rationals as well.

    You should use Z3 v4.0 when working with real numbers. While the interface will work with older versions of Z3 (or other SMT solvers in general), it uses Z3 root-obj construct to retrieve and query algebraic reals.

    While SReal values have infinite precision, printing such values is not trivial since we might need an infinite number of digits if the result happens to be irrational. The user controls printing precision, by specifying how many digits after the decimal point should be printed. The default number of decimal digits to print is 10. (See the 'printRealPrec' field of SMT-solver configuration.)

    The acronym SBV used to stand for Symbolic Bit Vectors. However, SBV has grown beyond bit-vectors, especially with the addition of support for SInteger and SReal types and other code-generation utilities. Therefore, "SMT Based Verification" is now a better fit for the expansion of the acronym SBV.

    Other notable changes in the library:

    • Add functions s[TYPE] and s[TYPE]s for each symbolic type we support (i.e., sBool, sBools, sWord8, sWord8s, etc.), to create symbolic variables of the right kind. Strictly speaking these are just synonyms for 'free' and 'mapM free' (plural versions), so they are not adding any additional power. Except, they are specialized at their respective types, and might be easier to remember.
    • Add function solve, which is merely a synonym for (return . bAnd), but it simplifies expressing problems.
    • Add class SNum, which simplifies writing polymorphic code over symbolic values
    • Increase haddock coverage metrics
    • Major code refactoring around symbolic kinds
    • SMTLib2: Emit ":produce-models" call before setting the logic, as required by the SMT-Lib2 standard. [Patch provided by arrowdodger on github, thanks!]

    Bugs fixed:

    • [Performance] Use a much simpler default definition for "select": While the older version (based on binary search on the bits of the indexer) was correct, it created unnecessarily big expressions. Since SBV does not have a notion of concrete subwords, the binary-search trick was not bringing any advantage in any case. Instead, we now simply use a linear walk over the elements.

    Examples:

    • Change dog-cat-mouse example to use SInteger for the counts
    • Add merge-sort example: Data.SBV.Examples.BitPrecise.MergeSort
    • Add diophantine solver example: Data.SBV.Examples.Existentials.Diophantine