Changelog for sbv-7.0

Version 7.0, Released 2017-07-19

Version 6.1, 2017-05-26

Version 6.0, 2017-05-07

Version 5.15, 2017-01-30

Version 5.14, 2017-01-12

Version 5.13, 2016-10-29

Version 5.12, 2016-06-06

Version 5.11, 2016-01-15

Version 5.10, 2016-01-14

Version 5.9, 2016-01-05

Version 5.8, 2016-01-01

Version 5.7, 2015-12-21

Version 5.6, 2015-12-06

Version 5.5, 2015-11-10

Version 5.4, 2015-11-09

Version 5.3, 2015-10-20

Version 5.2, 2015-10-12

Version 5.1, 2015-10-10

Version 5.0, 2015-09-22

Version 4.4, 2015-04-13

Version 4.3, 2015-04-10

Version 4.2, 2015-03-17

Version 4.1, 2015-03-06

Version 4.0, 2015-01-22

This release mainly contains contributions from Brian Huffman, allowing end-users to define new symbolic types, such as Word4, that SBV does not natively support. When GHC gets type-level literals, we shall most likely incorporate arbitrary bit-sized vectors and ints using this mechanism, but in the interim, this release provides a means for the users to introduce individual instances.

Version 3.5, 2015-01-15

This release is mainly adding support for enumerated types in Haskell being translated to their symbolic counterparts; instead of going completely uninterpreted.

Version 3.4, 2014-12-21

Version 3.3, 2014-12-05

Version 3.2, 2014-11-18

Version 3.1, 2014-07-12

NB: GHC 7.8.1 and 7.8.2 has a serious bug https://ghc.haskell.org/trac/ghc/ticket/9078 that causes SBV to crash under heavy/repeated calls. The bug is addressed in GHC 7.8.3; so upgrading to GHC 7.8.3 is essential for using SBV!

New features/bug-fixes in v3.1:

Version 3.0, 2014-02-16

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 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:

Bugs fixed:

Examples:

Version 1.4, 2012-05-10

Version 1.3, 2012-02-25

Version 1.2, 2012-02-25

Library:

Version 1.1, 2012-02-14

Library:

Version 1.0, 2012-02-13

Library:

Code-generation:

Other

Version 0.9.24, 2011-12-28

Library:

Examples

Dependencies

Internal

Version 0.9.23, 2011-12-05

Library:

Other:

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 is 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:

Code generation:

Examples:

Version 0.9.21, 2011-08-05

Code generation:

Version 0.9.20, 2011-06-05

Regression on 0.9.19; add missing file to cabal

Version 0.9.19, 2011-06-05

Examples:

Version 0.9.18, 2011-04-07

Code:

Examples:

Version 0.9.17, 2011-03-29

Code:

Examples:

Version 0.9.16, 2011-03-28

Code:

Examples:

Version 0.9.15, 2011-03-24

Bug fixes:

Testing:

Version 0.9.14, 2011-03-19

Version 0.9.13, 2011-03-16

Bug fixes:

Examples:

Version 0.9.12, 2011-03-10

New features:

Bug fixes:

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