Changelog for sbv-2.10

Version 2.10, 2013-03-22

Version 2.9, 2013-01-02

Version 2.8, 2012-11-29

Version 2.7, 2012-10-21

Versions 2.4, 2.5, and 2.6: Around mid October 2012

Version 2.3, 2012-07-20

Version 2.2, 2012-07-17

Version 2.1, 2012-05-24


Version 2.0, 2012-05-10

This is a major release of SBV, adding support for symbolic algebraic reals: SReal. See 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's 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 aren't 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.


Version 1.4, 2012-05-10

Version 1.3, 2012-02-25

Version 1.2, 2012-02-25


Version 1.1, 2012-02-14


Version 1.0, 2012-02-13


Version 0.9.24, 2011-12-28


Version 0.9.23, 2011-12-05


Version 0.9.22, 2011-11-13

The major change in this release is the support for quantifiers. The SBV library no longer assumes all variables are universals in a proof, (and correspondingly existential in a sat) call. Instead, the user marks free-variables appropriately using forall/exists functions, and the solver translates them accordingly. Note that this is a non-backwards compatible change in sat calls, as the semantics of formulas is essentially changing. While this is unfortunate, it's more uniform and simpler to understand in general.

This release also adds support for the Z3 solver, which is the main SMT-solver used for solving formulas involving quantifiers. More formally, we use the new AUFBV/ABV/UFBV logics when quantifiers are involved. Also, the communication with Z3 is now done via SMT-Lib2 format. Eventually the SMTLib1 connection will be severed.

The other main change is the support for C code generation with uninterpreted functions enabling users to interface with external C functions defined elsewhere. See below for details.

Other changes: Code: * Change getModel, so it returns an Either value to indicate something went wrong; instead of throwing an error * Add support for computing CRCs directly (without needing polynomial division). Code generation: * Add "cgGenerateDriver" function, which can be used to turn on/off driver program generation. Default is to generate a driver. (Issue "cgGenerateDriver False" to skip the driver.) For a library, a driver will be generated if any of the constituent parts has a driver. Otherwise it'll be skipped. * Fix a bug in C code generation where "Not" over booleans were incorrectly getting translated due to need for masking. * Add support for compilation with uninterpreted functions. Users can now specify the corresponding C code and SBV will simply call the "native" functions instead of generating it. This enables interfacing with other C programs. See the functions: cgAddPrototype, cgAddDecl, and cgAddLDFlags. Examples: * Add CRC polynomial generation example via existentials * Add USB CRC code generation example, both via polynomials and using the internal CRC functionality

Version 0.9.21, 2011-08-05

Code generation: * Allow for inclusion of user makefiles * Allow for CCFLAGS to be set by the user * Other minor clean-up

Version 0.9.20, 2011-06-05

Regression on 0.9.19; add missing file to cabal

Version 0.9.19, 2011-06-05

Code: * Add SignCast class for conversion between signed/unsigned quantities for same-sized bit-vectors * Add full-binary trees that can be indexed symbolically (STree). The advantage of this type is that the reads and writes take logarithmic time. Suitable for implementing faster symbolic look-up. * Expose HasSignAndSize class through Data.SBV.Internals * Many minor improvements, file re-orgs Examples: * Add sentence-counting example * Add an implementation of RC4

Version 0.9.18, 2011-04-07

Code: * Re-engineer code-generation, and compilation to C. In particular, allow arrays of inputs to be specified, both as function arguments and output reference values. * Add support for generation of generation of C-libraries, allowing code generation for a set of functions that work together. Examples: * Update code-generation examples to use the new API. * Include a library-generation example for doing 128-bit AES encryption

Version 0.9.17, 2011-03-29

Code: * Simplify and reorganize the test suite Examples: * Improve AES decryption example, by using table-lookups in InvMixColumns.

Version 0.9.16, 2011-03-28

Code: * Further optimizations on Bits instance of SBV Examples: * Add AES algorithm as an example, showing how encryption algorithms are particularly suitable for use with the code-generator

Version 0.9.15, 2011-03-24

Bug fixes: * Fix rotateL/rotateR instances on concrete words. Previous versions was bogus since it relied on the Integer instance, which does the wrong thing after normalization. * Fix conversion of signed numbers from bits, previous version did not handle two's complement layout correctly Testing: * Add a sleuth of concrete test cases on arithmetic to catch bugs. (There are many of them, ~30K, but they run quickly.)

Version 0.9.14, 2011-03-19

Version 0.9.13, 2011-03-16

Bug fixes: * Make sure SBool short-cut evaluations are done as early as possible, as these help with coding recursion-depth based algorithms, when dealing with symbolic termination issues. Examples: * Add fibonacci code-generation example, original code by Lee Pike. * Add a GCD code-generation/verification example

Version 0.9.12, 2011-03-10

New features: * Add support for compilation to C * Add a mechanism for offline saving of SMT-Lib files

Bug fixes: * Output naming bug, reported by Josef Svenningsson * Specification bug in Legato's multipler example

Version 0.9.11, 2011-02-16

Version 0.9.10, 2011-02-15

Version 0.9.9, 2011-01-23

Version 0.9.8, 2011-01-22

Version 0.9.7, 2011-01-18

Versions 0.0.0 - 0.9.6, Mid 2010 through early 2011