Changelog History
Page 7

v2.8 Changes
November 29, 2012 Rename the SNum class to SIntegral, and make it index over regular types. This makes it much more useful, simplifying coding of polymorphic symbolic functions over integral types, which is the common case.
 Add the functions:
 sbvShiftLeft
 sbvShiftRight which can accommodate unsigned symbolic shift amounts. Note that one cannot use the Haskell shiftL/shiftR functions from the Bits class since they are hardwired to take 'Int' values as the shift amounts only.
 Add a new function 'sbvArithShiftRight', which is the same as a shiftright, except it uses the MSB of the input as the bit to fill in (instead of always filling in with 0 bits). Note that this is the same as shiftRight for signed values, but differs from a shiftRight when the input is unsigned. (There is no Haskell analogue of this function, as Haskell shiftR is always arithmetic for signed types and logical for unsigned ones.) This variant is designed for use cases when one uses the underlying unsigned SMTLib representation to implement custom signed operations, for instance.
 Several typo fixes.

v2.7 Changes
October 21, 2012 Add missing QuickCheck instance for SReal
 When dealing with concrete SReals, make sure to operate only on exact algebraic reals on the Haskell side, leaving true algebraic reals (i.e., those that are roots of polynomials that cannot be expressed as a rational) symbolic. This avoids issues with functions that we cannot implement directly on the Haskell side, like exact squareroots.
 Documentation tweaks, typo fixes etc.
 Rename BVDivisible class to SDivisible; since SInteger is also an instance of this class, and SDivisible is a more appropriate name to start with. Also add sQuot and sRem methods; along with sDivMod, sDiv, and sMod, with usual semantics.
 Improve test suite, adding many constantfolding tests and start using cabal based tests (enabletests option.)

v2.3 Changes
July 20, 2012 Maintenance release, no new features.
 Tweak cabal dependencies to avoid using packages that are newer than those that come with ghc7.4.2. Apparently this is a nono that breaks many things, see the discussion in this thread: http://www.haskell.org/pipermail/haskellcafe/2012July/102352.html In particular, the use of containers >= 0.5 is not OK until we have a version of GHC that comes with that version.

v2.2 Changes
July 17, 2012 Maintenance release, no new features.
 Update cabal dependencies, in particular fix the regression with respect to latest version of the containers package.

v2.1 Changes
May 24, 2012 Library:
 Add support for uninterpreted sorts, together with user defined domain axioms. See Data.SBV.Examples.Uninterpreted.Sort and Data.SBV.Examples.Uninterpreted.Deduce for basic examples of this feature.
 Add support for C codegeneration with SReals. The user picks one of 3 possible C types for the SReal type: CgFloat, CgDouble or CgLongDouble, using the function cgSRealType. Naturally, the resulting C program will suffer a loss of precision, as it will be subject to IEE754 rounding as implied by the underlying type.
 Add toSReal :: SInteger > SReal, which can be used to promote symbolic integers to reals. Comes handy in mixed integer/real computations.
 Examples:
 Recast the dogcatmouse example to use the solver over reals.
 Add Data.SBV.Examples.Uninterpreted.Sort, and Data.SBV.Examples.Uninterpreted.Deduce for illustrating uninterpreted sorts and axioms.
 Library:

v2.0 Changes
May 10, 2012This 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 rootobj 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 SMTsolver configuration.)
The acronym SBV used to stand for Symbolic Bit Vectors. However, SBV has grown beyond bitvectors, especially with the addition of support for SInteger and SReal types and other codegeneration 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 ":producemodels" call before setting the logic, as required by the SMTLib2 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 binarysearch trick was not bringing any advantage in any case. Instead, we now simply use a linear walk over the elements.
Examples:
 Change dogcatmouse example to use SInteger for the counts
 Add mergesort example: Data.SBV.Examples.BitPrecise.MergeSort
 Add diophantine solver example: Data.SBV.Examples.Existentials.Diophantine

v1.4 Changes
May 10, 2012 Interim release for test purposes

v1.3 Changes
February 25, 2012 Workaround cabal/hackage issue, functionally the same as release 1.2 below

v1.2 Changes
February 25, 2012Library:
 Add a hook so users can add custom script segments for SMT solvers. The new "solverTweaks" field in the SMTConfig datatype can be used for this purpose. The need for this came about due to the need to workaround a Z3 v3.2 issue detailed below: http://stackoverflow.com/questions/9426420/soundnessissuewithintegerbvmixedbenchmarks As a consequence, mixed Integer/BV problems can cause soundness issues in Z3 and does in SBV. Unfortunately, it is too severe for SBV to add the workaround option, as it slows down the solver as a side effect as well. Thus, we are making this optionally available if/when needed. (Note that the workaround should not be necessary with Z3 v3.3; which is not released yet.)
 Other minor cleanup

v1.1 Changes
February 14, 2012Library:
 Rename bitValue to sbvTestBit
 Add sbvPopCount
 Add a custom implementation of 'popCount' for the Bits class instance of SBV (GHC >= 7.4.1 only)
 Add 'sbvCheckSolverInstallation', which can be used to check that the given solver is installed and good to go.
 Add 'generateSMTBenchmarks', simplifying the generation of SMTLib benchmarks for offline sharing.