- 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:
- 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 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 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.
- 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 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.)
- Maintenance 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.
- Maintenance release, no new features.
- Update cabal dependencies, in particular fix the regression with respect to latest version of the containers package.
- 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.
- 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.
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!]
- [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.
- 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
- Interim release for test purposes
- Workaround cabal/hackage issue, functionally the same as release 1.2 below
- 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 detailed 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 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 work-around should not be necessary with Z3 v3.3; which is not released yet.)
- Other minor clean-up
- 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.