• Hackage: http://hackage.haskell.org/package/sbv

• GitHub: http://leventerkok.github.com/sbv/

• Latest Hackage released version: 2.10

Version 2.10, 2013-03-22

• Add support for the Boolector SMT solver
  • See: http://fmv.jku.at/boolector/
  • Use import Data.SBV.Bridge.Boolector to use Boolector from SBV
  • Boolector supports QF_BV (with an without arrays). In the last SMT-Lib competition it won both bit-vector categories. It is definitely worth trying it out for bitvector problems.
• Changes to the library:
  • Generalize types of allDifferent and allEqual to take arbitrary EqSymbolic values. (Previously was just over SBV values.)
  • Add inRange predicate, which checks if a value is bounded within two others.
  • Add sElem predicate, which checks for symbolic membership
  • Add fullAdder: Returns the carry-over as a separate boolean bit.
  • Add fullMultiplier: Returns both the lower and higher bits resulting from multiplication.
  • Use the SMT-Lib Bool sort to represent SBool, instead of bit-vectors of length 1. While this is an under-the-hood mechanism that should be user-transparent, it turns out that one can no longer write axioms that return booleans in a direct way due to this translation. This change makes it easier to write axioms that utilize booleans as there is now a 1-to-1 match. (Suggested by Thomas DuBuisson.)
• Solvers changes:
  • Z3: Update to the new parameter naming schema of Z3. This implies that you need to have a really recent version of Z3 installed, something in the Z3-4.3 series.
• Examples:
  • Add Examples/Uninterpreted/Shannon.hs: Demonstrating Shannon expansion, boolean derivatives, etc.
• Bug-fixes:
  • Gracefully handle the case if the backend-SMT solver does not put anything in stdout. (Reported by Thomas DuBuisson.)
  • Handle uninterpreted sort values, if they happen to be only created via function calls, as opposed to being inputs. (Reported by Thomas DuBuisson.)

Version 2.9, 2013-01-02

• Add support for the CVC4 SMT solver from New York University and the University of Iowa. (http://cvc4.cs.nyu.edu/). NB. Z3 remains the default solver for SBV. To use CVC4, use the *With variants of the interface (i.e., proveWith, satWith, ..) by passing cvc4 as the solver argument. (Similarly, use 'yices' as the argument for the *With functions for invoking yices.)

• Latest release of Yices calls the SMT-Lib based solver executable yices-smt. Updated the default value of the executable to have this name for ease of use.

• Add an extra boolean flag to compileToSMTLib and generateSMTBenchmarks functions to control if the translation should keep the query as is (for SAT cases), or negate it (for PROVE cases). Previously, this value was hard-coded to do the PROVE case only.

• Add bridge modules, to simplify use of different solvers. You can now say:

    import Data.SBV.Bridge.CVC4
    import Data.SBV.Bridge.Yices
    import Data.SBV.Bridge.Z3
  

  to pick the appropriate default solver. if you simply 'import Data.SBV', then you will get the default SMT solver, which is currently Z3. The value 'defaultSMTSolver' refers to z3 (currently), and 'sbvCurrentSolver' refers to the chosen solver as determined by the imported module. (The latter is useful for modifying options to the SMT solver in an solver-agnostic way.)

• Various improvements to Z3 model parsing routines.

• New web page for SBV: http://leventerkok.github.com/sbv/ is now online.

Version 2.8, 2012-11-29

• 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 Haskell's shiftL/shiftR from the Bits class since they are hard-wired to take 'Int' values as the shift amounts only.
• Add a new function 'sbvArithShiftRight', which is the same as a shift-right, 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's 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 SMT-Lib representation to implement custom signed operations, for instance.
• Several typo fixes.

Version 2.7, 2012-10-21

• Add missing QuickCheck instance for SReal
• When dealing with concrete SReal's, 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 square-roots.
• 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 constant-folding tests and start using cabal based tests (--enable-tests option.)

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

• Workaround issues related hackage compilation, in particular to the problem with the new containers package release, which does provide an NFData instance for sequences.
• Add explicit Num requirements when necessary, as the Bits class no longer does this.
• Remove dependency on the hackage package strict-concurrency, as hackage can no longer compile it due to some dependency mismatch.
• Add forgotten Real class instance for the type 'AlgReal'
• Stop putting bounds on hackage dependencies, as they cause more trouble then they actually help. (See the discussion here: http://www.haskell.org/pipermail/haskell-cafe/2012-July/102352.html.)

Version 2.3, 2012-07-20

• Maintanence release, no new features.
• Tweak cabal dependencies to avoid using packages that are newer than those that come with ghc-7.4.2. Apparently this is a no-no that breaks many things, see the discussion in this thread: http://www.haskell.org/pipermail/haskell-cafe/2012-July/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.

Version 2.2, 2012-07-17

• Maintanence release, no new features.
• Update cabal dependencies, in particular fix the regression with respect to latest version of the containers package.

Version 2.1, 2012-05-24

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 code-generation 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 IEE-754 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 dog-cat-mouse 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.

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'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.

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

Version 1.4, 2012-05-10

• Interim release for test purposes

Version 1.3, 2012-02-25

• Workaround cabal/hackage issue, functionally the same as release 1.2 below

Version 1.2, 2012-02-25

Library:

• Add a hook so users can add custom script segments for SMT solvers. The new "solverTweaks" field in the SMTConfig data-type can be used for this purpose. The need for this came about due to the need to workaround a Z3 v3.2 issue detalied below: http://stackoverflow.com/questions/9426420/soundness-issue-with-integer-bv-mixed-benchmarks As a consequence, mixed Integer/BV problems can cause soundness issues in Z3 and does in SBV. Unfortunately, it's too severe for SBV to add the woraround option, as it slows down the solver as a side effect as well. Thus, we're making this optionally available if/when needed. (Note that the work-around should not be necessary with Z3 v3.3; which isn't released yet.)
• Other minor clean-up

Version 1.1, 2012-02-14

Library:

• 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.

Version 1.0, 2012-02-13

Library:

• Z3 is now the "default" SMT solver. Yices is still available, but has to be specifically selected. (Use satWith, allSatWith, proveWith, etc.)
• Better handling of the pConstrain probability threshold for test case generation and quickCheck purposes.
• Add 'renderTest', which accompanies 'genTest' to render test vectors as Haskell/C/Forte program segments.
• Add 'expectedValue' which can compute the expected value of a symbolic value under the given constraints. Useful for statistical analysis and probability computations.
• When saturating provable values, use forAll_ for proofs and forSome_ for sat/allSat. (Previously we were allways using forAll_, which is not incorrect but less intuitive.)
• add function: extractModels :: SatModel a => AllSatResult -> [a] which simplifies accessing allSat results greatly. Code-generation:
• add "cgGenerateMakefile" which allows the user to choose if SBV should generate a Makefile. (default: True) Other
• Changes to make it compile with GHC 7.4.1.

Version 0.9.24, 2011-12-28

Library:

• Add "forSome," analogous to "forAll." (The name "exists" would've been better, but it's already taken.) This is not as useful as one might think as forAll and forSome do not nest, as an inner application of one pushes its argument to a Predicate, making the outer one useless, but it's nonetheless useful by itself.
• Add a "Modelable" class, which simplifies model extraction.
• Add support for quick-check at the "Symbolic SBool" level. Previously SBV only allowed functions returning SBool to be quick-checked, which forced a certain style of coding. In particular with the addition of quantifiers, the new coding style mostly puts the top-level expressions in the Symbolic monad, which were not quick-checkable before. With new support, the quickCheck, prove, sat, and allSat commands are all interchangeable with obvious meanings.
• Add support for concrete test case generation, see the genTest function.
• Improve optimize routines and add support for iterative optimization.
• Add "constrain", simplifying conjunctive constraints, especially useful for adding constraints at variable generation time via forall/exists. Note that the interpretation of such constraints is different for genTest and quickCheck functions, where constraints will be used for appropriately filtering acceptable test values in those two cases.
• Add "pConstrain", which probabilistically adds constraints. This is useful for quickCheck and genTest functions for filtering acceptable test values. (Calls to pConstrain will be rejected for sat/prove calls.)
• Add "isVacuous" which can be used to check that the constraints added via constrain are satisfable. This is useful to prevent vacuous passes, i.e., when a proof is not just passing because the constraints imposed are inconsistent. (Also added accompanying isVacuousWith.)
• Add "free" and "free_", analogous to "forall/forall_" and "exists/exists_" The difference is that free behaves universally in a proof context, while it behaves existentially in a sat context. This allows us to express properties more succinctly, since the intended semantics is usually this way depending on the context. (i.e., in a proof, we want our variables universal, in a sat call existential.) Of course, exists/forall are still available when mixed quantifiers are needed, or when the user wants to be explicit about the quantifiers. Examples
• Add Data/SBV/Examples/Puzzles/Coins.hs. (Shows the usage of "constrain".) Dependencies
• Bump up random package dependency to 1.0.1.1 (from 1.0.0.2) Internal
• Major reorganization of files to and build infrastructure to decrease build times and better layout
• Get rid of custom Setup.hs, just use simple build. The extra work was not worth the complexity.

Version 0.9.23, 2011-12-05

Library:

• Add support for SInteger, the type of signed unbounded integer values. SBV can now prove theorems about unbounded numbers, following the semantics of Haskell's Integer type. (Requires z3 to be used as the backend solver.)
• Add functions 'optimize', 'maximize', and 'minimize' that can be used to find optimal solutions to given constraints with respect to a given cost function.
• Add 'cgUninterpret', which simplifies code generation when we want to use an alternate definition in the target language (i.e., C). This is important for efficient code generation, when we want to take advantage of native libraries available in the target platform. Other:
• Change getModel to return a tuple in the success case, where the first component is a boolean indicating whether the model is "potential." This is used to indicate that the solver actually returned "unknown" for the problem and the model might therefore be bogus. Note that we did not need this before since we only supported bounded bit-vectors, which has a decidable theory. With the addition of unbounded Integer's and quantifiers, the solvers can now return unknown. This should still be rare in practice, but can happen with the use of non-linear constructs. (i.e., multiplication of two variables.)

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

• Reimplement sharing using Stable names, inspired by the Data.Reify techniques. This avoids tricks with unsafe memory stashing, and hence is safe. Thus, issues with respect to CAFs are now resolved.

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

• Make ghc-7.0 happy, minor re-org on the cabal file/Setup.hs

Version 0.9.10, 2011-02-15

• Integrate commits from Iavor: Generalize SBV's to keep track the integer directly without resorting to different leaf types
• Remove the unnecessary CLC instruction from the Legato example
• More tests

Version 0.9.9, 2011-01-23

• Support for user-defined SMT-Lib axioms to be specified for uninterpreted constants/functions
• Move to using doctest style inline tests

Version 0.9.8, 2011-01-22

• Better support for uninterpreted-functions
• Support counter-examples with SArray's
• Ladner-Fischer scheme example
• Documentation updates

Version 0.9.7, 2011-01-18

• First stable public hackage release

Versions 0.0.0 - 0.9.6, Mid 2010 through early 2011

• Basic infrastructure, design exploration