sbv
SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. http://leventerkok.github.com/sbv/
Latest on Hackage:  8.7 
Module documentation for 5.11
sbv5.11@sha256:c306ce117215aab658dfe15acf2665400a0496260c3fce1735c09309c60ac3c9,10168
Changes

Latest Hackage released version: 5.11, 20160115
Version 5.11, 20160115
 Fix documentation issue; no functional changes
Version 5.10, 20160114

Documentation: Fix a bunch of dead http links. Thanks to Andres SicardRamirez for reporting.

Additions to the Dynamic API:
 svSetBit : set a given bit
 svBlastLE, svBlastBE : Bitblast to big/little endian
 svWordFromLE, svWordFromBE: Unblast from big/little endian
 svAddConstant : Add a constant to an SVal
 svIncrement, svDecrement : Add/subtract 1 from an SVal
Version 5.9, 20160105

Default definition for ‘symbolicMerge’, which allows types that are instances of ‘Generic’ to have an automatically derivable merge (i.e., ite) instance. Thanks to Christian Conkle for the patch.

Add support for “nonmodelvars,” where we can now tell SBV not to take into account certain variables from a modelbuilding perspective. This comes handy in doing an
allSat
calls where there might be witness variables that we do not care the uniqueness for. See “Data/SBV/Examples/Misc/Auxiliary.hs” for an example, and the discussion in https://github.com/LeventErkok/sbv/issues/208 for motivation. 
Yices interface: If Reals are used, then pick the logic QF_UFLRA, instead of QF_AUFLIA. Unfortunately, logic selection remains tricky since the SMTLib story for logic selection is rather messy. Other solvers are not impacted by this change.
Version 5.8, 20160101
 Fix some typos
 Add ‘svEnumFromThenTo’ to the Dynamic interface, allowing dynamic construction of [x, y .. z] and [x .. y] when the involved values are concrete.
 Add ‘svExp’ to the Dynamic interface, implementing exponentation
Version 5.7, 20151221
 Export HasKind(..) from the Dynamic interface. Thanks to Adam Foltzer for the patch.
 More careful handling of SMTLib reserved names.
 Update tested version of MathSAT to 5.3.9
 Generalize sShiftLeft/sShiftRight/sRotateLeft/sRotateRight to work with signed shift/rotate amounts, where negative values revert the direction. Similar generalizations are also done for the dynamic variants.
Version 5.6, 20151206

Minor changes to how we print models:

Align by the type

Always print the type (previously we were skipping for Bool)

Rework how SBV properties are quickchecked; much more usable and robust

Provide a function sbvQuickCheck, which is essentially the same as quickCheck, except it also returns a boolean. Useful for the programmable API. (The dynamic version is called svQuickCheck)

Several changes/additions in support of the sbvPlugin development:

Data.SBV.Dynamic: Define/export svFloat/svDouble/sReal/sNumerator/sDenominator

Data.SBV.Internals: Export constructors of Result, SMTModel, and the function showModel

Simplify how Uninterpretedtypes are internally represented.
Version 5.5, 20151110
 This is essentially the same release as 5.4 below, except to allow SBV compile with GHC 7.8 series. Thanks to Adam Foltzer for the patch.
Version 5.4, 20151109

Add ‘sAssert’, which allows users to pepper their code with boolean conditions, much like the usual ASSERT calls. Note that the semantics of an ‘sAssert’ is that it is a NOOP, i.e., it simply returns its final argument. Use in coordination with ‘safe’ and ‘safeWith’, see below.

Implement ‘safe’ and ‘safeWith’, which statically determine all calls to ‘sAssert’ being safe to execute. Any vilations will be flagged.

SBV>C: Translate ‘sAssert’ calls to dynamic checks in the generated C code. If this is not desired, use the ‘cgIgnoreSAssert’ function to turn it off.

Add ‘isSafe’: Which converts a ‘SafeResult’ to a ‘Bool’, when we are only interested in a boolean result.

Add Data/SBV/Examples/Misc/NoDiv0 to demonstrate the use of the ‘safe’ function.
Version 5.3, 20151020

Main point of this release to make SBV compile with GHC 7.8 again, to accommodate mainly for Cryptol. As Cryptol moves to GHC >= 7.10, we intend to remove the “compatibility” changes again. Thanks to Adam Foltzer for the patch.

Minor mods to how bitvector equality/inequality are translated to SMTLib. No user visible impact.
Version 5.2, 20151012
 Regression on 5.1: Fix a minor bug in base 2/16 printing where uninterpreted constants were not handled correctly.
Version 5.1, 20151010

fpMin, fpMax: If these functions receive +0/0 as their two arguments, i.e., both zeros but alternating signs in any order, then SMTLib requires the output to be nondeterministicly chosen. Previously, we fixed this result as +0 following the interpretation in Z3, but Z3 recently changed and now incorporates the nondeterministic output. SBV similarly changed to allow for nondeterminism here.

Change the types of the following Floatingpoint operations:
* sFloatAsSWord32, sFloatAsSWord32, blastSFloat, blastSDouble
These were previously coded as relations, since NaN values were not representable in the target domain uniquely. While it was OK, it was hard to use them. We now simply implement these as functions, and they are underspecified if the inputs are NaNs: In those cases, we simply get a symbolic output. The new types are:
 sFloatAsSWord32 :: SFloat > SWord32
 sDoubleAsSWord64 :: SDouble > SWord64
 blastSFloat :: SFloat > (SBool, [SBool], [SBool])
 blastSDouble :: SDouble > (SBool, [SBool], [SBool])

MathSAT backend: Use the SMTLib interpretation of fp.min/fp.max by passing the “theory.fp.minmax_zero_mode=4” argument explicitly.

Fix a bug in hashconsing of floatingpoint constants, where we were confusing +0 and 0 since we were using them as keys into the map though they compare equal. We now explicitly keep track of the negativezero status to make sure this confusion does not arise. Note that this bug only exhibited itself in rare occurrences of both constants being present in a benchmark; a true corner case. Note that @NaN@ values are also interesting in this context: Since NaN /= NaN, we never hashcons floating point constants that have the value NaN. But that is actually OK; it is a bit wasteful in case you have a lot of NaN constants around, but there is no soundness issue: We just waste a little bit of space.

Remove the functions
allSatWithAny
andallSatWithAll
. These two variants do not make sense when run with multiple solvers, as they internally sequentialize the solutions due to the nature ofallSat
. Not really needed anyhow; so removed. The variantssatWithAny/All
andproveWithAny/All
are still available. 
Export SMTLibVersion from the library, forgotten export needed by Cryptol. Thanks to Adam Foltzer for the patch.

Slightly modify modeloutputs so the variables are aligned vertically. (Only matters if we have modelvariable names that are of differing length.)

Move to TravisCI “docker” based infrastructure for builds

Enable local builds to use the Herbie plugin. Currently SBV does not have any expressions that can benefit from Herbie, but it is nice to have this support in general.
Version 5.0, 20150922

Note: This is a backwardscompatibility breaking release, see below for details.

SBV now requires GHC 7.10.1 or newer to be compiled, taking advantage of newer features/bugfixes in GHC. If you really need SBV to compile with older GHCs, please get in touch.

SBV no longer supports SMTLib1. We now exclusively use SMTLib2 for communicating with backend solvers. Strictly speaking, this means some loss in functionality: Uninterpretedfunction models that we supported via Yices1 are no longer available. In practice this facility was not really used, and required a very old version of Yices that was no longer supported by SRI and has lacked in other features. So, in reality this change should hardly matter for endusers.

Added function “label”, which is useful in emitting comments around expressions. It is essentially a noop, but does generate a comment with the given text in the SMTLib and C output, for diagnostic purposes.

Added “sFromIntegral”: Conversions from all integral types (SInteger, SWord/SInts) between each other. Similar to the “fromIntegral” function of Haskell. These generate simple casts when used in codegeneration to C, and thus are very efficient.

SBV no longer supports the functions sBranch/sAssert, as we realized these functions can cause soundness issues under certain conditions. While the triggering scenarios are not common usecases for these functions, we are opting for safety, and thus removing support. See http://github.com/LeventErkok/sbv/issues/180 for details; and see below for the new function ‘isSatisfiableInCurrentPath’.

A new function ‘isSatisfiableInCurrentPath’ is added, which checks for satisfiability during a symbolic simulation run. This function can be used as the basis of sBranch/sAssert like functionality if needed. The difference is that this is a much lower level call, and also exposes the fact that the result is in the ‘Symbolic’ monad (which avoids the soundness issue). Of course, the new type makes it less useful as it will not be a dropin replacement for ifthenelse like structure. Intended to be used by tools built on top of SBV, as opposed to endusers.

SBV no longer implements the ‘SignCast’ class, as its functionality is replaced by the ‘sFromIntegral’ function. Programs using the functions ‘signCast’ and ‘unsignCast’ should simply replace both with calls to ‘sFromIntegral’. (Note that extra typeannotations might be necessary, similar to the uses of the ‘fromIntegral’ function in Haskell.)

Backend solver related changes:

Yices: Upgraded to work with Yices release 2.4.1. Note that earlier versions of Yices are not supported.

Boolector: Upgraded to work with new Boolector release 2.0.7. Note that earlier versions of Boolector are not supported.

MathSAT: Upgraded to work with latest release 5.3.7. Note that earlier versions of MathSAT are not supported (due to a buffering issue in MathSAT itself.)

MathSAT: Enabled floatingpoint support in MathSAT.


New examples:

Add Data.SBV.Examples.Puzzles.Birthday, which solves the CherylBirthday problem that went viral in April 2015. Turns out really easy to solve for SMT, but the formalization of the problem is still interesting as an exercise in formal reasoning.

Add Data.SBV.Examples.Puzzles.SendMoreMoney, which solves the classic send + more = money problem. Really a trivial example, but included since it is pretty much the helloworld for basic constraint solving.

Add Data.SBV.Examples.Puzzles.Fish, which solves a typical logic puzzle; finding the unique solution to a set of assertions made about a bunch of people, their pets, beverage choices, etc. Not particularly interesting, but could be fun to play around with for modeling purposes.

Add Data.SBV.Examples.BitPrecise.MultMask, which demonstrates the use of the bitvector solver to an interesting bitshuffling problem.


Rework floatingpoint arithmetic, and add missing floatingpoint operations:
 fpRem : remainder
 fpRoundToIntegral: truncating round
 fpMin : min
 fpMax : max
 fpIsEqualObject : FP equality as object (i.e., NaN equals NaN, +0 does not equal 0, etc.)
This brings SBV upto par with everything supported by the SMTLib FP theory.

Add the IEEEFloatConvertable class, which provides conversions to/from Floats and other types. (i.e., value conversions from all other types to Floats and Doubles; and back.)

Add SWord32/SWord64 to/from SFloat/SDouble conversions, as bitpattern reinterpretation; using the IEEE754 interchange format. The functions are: sWord32AsSFloat, sWord64AsSDouble, sFloatAsSWord32, sDoubleAsSWord64. Note that the sWord32AsSFloat and sWord64ToSDouble are regular functions, but sFloatToSWord32 and sDoubleToSWord64 are “relations”, since NaN values are not uniquely convertable.

Add ‘sExtractBits’, which takes a list of indices to extract bits from, essentially equivalent to ‘map sTestBit’.

Rename a set of symbolic functions for consistency. Here are the old/new names:
 sbvTestBit –> sTestBit
 sbvPopCount –> sPopCount
 sbvShiftLeft –> sShiftLeft
 sbvShiftRight –> sShiftRight
 sbvRotateLeft –> sRotateLeft
 sbvRotateRight –> sRotateRight
 sbvSignedShiftArithRight –> sSignedShiftArithRight

Rename all FP recognizers to be in sync with FP operations. Here are the old/new names:
 isNormalFP –> fpIsNormal
 isSubnormalFP –> fpIsSubnormal
 isZeroFP –> fpIsZero
 isInfiniteFP –> fpIsInfinite
 isNaNFP –> fpIsNaN
 isNegativeFP –> fpIsNegative
 isPositiveFP –> fpIsPositive
 isNegativeZeroFP –> fpIsNegativeZero
 isPositiveZeroFP –> fpIsPositiveZero
 isPointFP –> fpIsPoint

Lots of other work around floatingpoint, test cases, reorg, etc.

Introduce shorter variants for rounding modes: sRNE, sRNA, sRTP, sRTN, sRTZ; aliases for sRoundNearestTiesToEven, sRoundNearestTiesToAway, sRoundTowardPositive, sRoundTowardNegative, and sRoundTowardZero; respectively.
Version 4.4, 20150413

Hookup crackNum package; so counterexamples involving floats and doubles can be printed in detail when the printBase is chosen to be 2 or 16. (With base 10, we still get the simple output.)
Prelude Data.SBV> satWith z3{printBase=2} $ \x > x .== (2::SFloat) Satisfiable. Model: s0 = 2.0 :: Float 3 2 1 0 1 09876543 21098765432109876543210 S E8 F23 Binary: 0 10000000 00000000000000000000000 Hex: 4000 0000 Precision: SP Sign: Positive Exponent: 1 (Stored: 128, Bias: 127) Value: +2.0 (NORMAL)

Change how we print type info; for models insted of SType just print Type (i.e., for SWord8, instead print Word8) which makes more sense and is more consistent. This change should be mostly relevant as how we see the counterexample output.

Fix long standing bug #75, where we now support arrays with Boolean source/targets. This is not a very commonly used case, but by letting the solver pick the logic, we now allow arrays to be uniformly supported.
Version 4.3, 20150410

Introduce Data.SBV.Dynamic, by Brian Huffman. This is mostly an internal reorg of the SBV codebase, and endusers should not be impacted by the changes. The introduction of the Dynamic SBV variant (i.e., one that does not mandate a phantom type as in “SBV Word8” etc. allows library writers more flexibility as they deal with arbitrary bitvector sizes. The main customor of these changes are the Cryptol language and the associated toolset, but other developers building on top of SBV can find it useful as well. NB: The “stronglytyped” aspect of SBV is still the main way endusers should interact with SBV, and nothing changed in that respect!

Add symbolic variants of floatingpoint roundingmodes for convenience

Rename toSReal to sIntegerToSReal, which captures the intent more clearly

Code cleanup: remove mbMinBound/mbMaxBound thus allowing less calls to unliteral. Contributed by Brian Huffman.

Introduce FP conversion functions:
 Between SReal and SFloat/SDouble
 fpToSReal
 sRealToSFloat
 sRealToSDouble
 Between SWord32 and SFloat
 sWord32ToSFloat
 sFloatToSWord32
 Between SWord64 and SDouble. (Relational, due to nonunique NaNs)
 sWord64ToSDouble
 sDoubleToSWord64
 From float to sign/exponent/mantissa fields: (Relational, due to nonunique NaNs)
 blastSFloat
 blastSDouble
 Between SReal and SFloat/SDouble

Rework floating point classifiers. Remove isSNaN and isFPPoint (both renamed), and add the following new recognizers:
 isNormalFP
 isSubnormalFP
 isZeroFP
 isInfiniteFP
 isNaNFP
 isNegativeFP
 isPositiveFP
 isNegativeZeroFP
 isPositiveZeroFP
 isPointFP (corresponds to a real number, i.e., neither NaN nor infinity)

Reimplement sbvTestBit, by Brian Huffman. This version is much faster at large word sizes, as it avoids the costly mask generation.

Code changes to suppress warnings with GHC7.10. General cleanup.
Version 4.2, 20150317

Add exponentiation (.^). Thanks to Daniel Wagner for contributing the code!

Better handling of SBV_$SOLVER_OPTIONS, in particular keeping track of proper quoting in environment variables. Thanks to Adam Foltzer for the patch!

Silence some hlint/ghci warnings. Thanks to Trevor Elliott for the patch!

Haddock documentation fixes, improvements, etc.

Change ABC default option string to %blast; “&sweep C 5000; &syn4; &cec s m C 2000” which seems to give good results. Use SBV_ABC_OPTIONS environment variable (or via abc.rc file and a combination of SBV_ABC_OPTIONS) to experiment.
Version 4.1, 20150306

Add support for the ABC solver from Berkeley. Thanks to Adam Foltzer for the required infrastructure! See: http://www.eecs.berkeley.edu/~alanmi/abc/ And Alan Mishchenko for adding infrastructure to ABC to work with SBV.

Upgrade the Boolector connection to use a SMTLib2 based interaction. NB. You need at least Boolector 2.0.6 installed!

Tracking changes in the SMTLib floatingpoint theory. If you are using symbolic floatingpoint types (i.e., SFloat and SDouble), then you should upgrade to this version and also get a very latest (unstable) Z3 release. See http://smtlib.cs.uiowa.edu/theoriesFloatingPoint.shtml for details.

Introduce a new class, ‘RoundingFloat’, which supports floatingpoint operations with arbitrary roundingmodes. Note that Haskell only allows RoundNearestTiesToAway, but with SBV, we get all 5 IEEE754 roundingmodes and all the basic operations (‘fpAdd’, ‘fpMul’, ‘fpDiv’, etc.) with these modes.

Allow FloatingPoint RoundingMode to be symbolic as well

Improve the example “Data/SBV/Examples/Misc/Floating.hs” to include roundingmode based addition example.

Changes required to make SBV compile with GHC 7.10; mostly around instance NFData declarations. Thanks to Iavor Diatchki for the patch.

Export a few extra symbols from the Internals module (mainly for Cryptol usage.)
Version 4.0, 20150122
This release mainly contains contributions from Brian Huffman, allowing endusers to define new symbolic types, such as Word4, that SBV does not natively support. When GHC gets typelevel literals, we shall most likely incorporate arbitrary bitsized vectors and ints using this mechanism, but in the interim, this release provides a means for the users to introduce individual instances.
 Modifications to support arbitrary bitsized vectors; These changes have been contributed by Brian Huffman of Galois.. Thanks Brian.
 A new example “Data/SBV/Examples/Misc/Word4.hs” showing how users can add new symbolic types.
 Support for rotateleft/rotateright with variable rotation amounts. (From Brian Huffman.)
Version 3.5, 20150115
This release is mainly adding support for enumerated types in Haskell being translated to their symbolic counterparts; instead of going completely uninterpreted.
 Keep track of datatype details for uninterpreted sorts.
 Rework the U2Bridge example to use enumerated types.
 The “Uninterpreted” name no longer makes sense with this change, so rework the relevant names to ensure proper internal naming.
 Add Data/SBV/Examples/Misc/Enumerate.hs as an example for demonstrating how enumerations are translated.
 Fix a longstanding bug in the implementation of select when translated as SMTLib tables. (Github issue #103.) Thanks to Brian Huffman for reporting.
Version 3.4, 20141221

This release is mainly addressing floatingpoint changes in SMTLib.

Track changes in the QF_FPA logic standard; new constants and alike. If you are using the floatingpoint logic, then you need a relatively new version of Z3 installed (4.3.3 or newer).

Add unarynegation as an explicit operator. Previously, we merely used the “0x” semantics; but with floating point, this does not hold as 00 is 0, and is not 0! (Note that negativezero is a valid floating point value, that is different than positivezero; yet it compares equal to it. Sigh..)

Similarly, add abs as a native method; to make sure we map it to fp.abs for floating point values.

Test suite improvements

Version 3.3, 20141205

Implement ‘safe’ and ‘safeWith’, which statically determine all calls to ‘sAssert’ being safe to execute. This way, users can pepper their programs with liberal calls to ‘sAssert’ and check they are all safe in one go without further worry.

Robustify the interface to external solvers, by making sure we catch cases where the external solver might exist but not be runnable (library dependency missing, for example). It is impossible to be absolutely foolproof, but we now catch a few more cases and fail gracefully.
Version 3.2, 20141118

Implement ‘sAssert’. This adds conditional symbolic simulation, by ensuring arbitrary boolean conditions hold during simulation; similar to ASSERT calls in other languages. Note that failures will be detected at symbolicsimulation time, i.e., each assert will generate a call to the external solver to ensure that the condition is never violated. If violation is possible the user will get an error, indicating the failure conditions.

Also implement ‘sAssertCont’ which allows for a programmatic way to extract/display results for consumers of ‘sAssert’. While the latter simply calls ‘error’ in case of an assertion violation, the ‘sAssertCont’ variant takes a continuation which can be used to program how the results should be interpreted/displayed. (This is useful for libraries built on top of SBV.) Note that the type of the continuation is such that execution should still stop, i.e., once an assertion violation is detected, symbolic simulation will never continue.

Rework/simplify the ‘Mergeable’ class to make sure ‘sBranch’ is sufficiently lazy in case of structural merges. The original implementation was only lazy at the Word instance, but not at lists/tuples etc. Thanks to Brian Huffman for reporting this bug.

Add a few constantfolding optimizations for ‘sDiv’and ‘sRem’

Boolector: Modify output parser to conform to the new Boolector output format. This means that you need at least v2.0.0 of Boolector installed if you want to use that particular solver.

Fix longstanding translation bug regarding boolean Ord class comparisons. (i.e., ‘False > True’ etc.) While Haskell allows for this, SMTLib does not; and hence we have to be careful in translating. Thanks to Brian Huffman for reporting.

C code generation: Correctly translate squareroot and fusedMA functions to C.
Version 3.1, 20140712
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/bugfixes in v3.1:
 Using multipleSMT solvers in parallel:
 Added functions that let the user run multiple solvers, using asynchronous threads. All results can be obtained (proveWithAll, proveWithAny, satWithAll), or SBV can return the fastest result (satWithAny, allSatWithAll, allSatWithAny). These functions are good for playing with multiplesolvers, especially on machines with multiplecores.
 Add function: sbvAvailableSolvers; which returns the list of solvers currently available, as installed on the machine we are running. (Not the list that SBV supports, but those that are actually available at runtime.) This function is useful with the multisolve API.
 Implement sBranch:
 sBranch is a variant of ‘ite’ that consults the external SMT solver to see if a given branch condition is satisfiable before evaluating it. This can make certain otherwise recursive and thus notsymbolicallyterminating inputs amenable to symbolic simulation, if termination can be established this way. Needless to say, this problem is always decidable as far as SBV programs are concerned, but it does not mean the decision procedure is cheap! Use with care.
 sBranchTimeOut config parameter can be used to curtail long runs when sBranch is used. Of course, if timeout happens, SBV will assume the branch is feasible, in which case symbolictermination may come back to bite you.)
 New API:
 Add predicate ‘isSNaN’ which allows testing ‘SFloat’/‘SDouble’ values for nanness. This is similar to the Prelude function ‘isNaN’, except the Prelude version requires a RealFrac instance, which unfortunately is not currently implementable for cases. (Requires trigonometric functions etc.) Thus, we provide ‘isSNaN’ separately (along with the already existing ‘isFPPoint’) to simplify reasoning with floatingpoint.
 Examples:
 Add Data/SBV/Examples/Misc/SBranch.hs, to illustrate the use of sBranch.
 Bug fixes:
 Fix pipeblocking issue, which exhibited itself in the presence of large numbers of variables (> 10K or so). See github issue #86. Thanks to Philipp Meyer for the fine report.
 Misc:
 Add missing SFloat/SDouble instances for SatModel class
 Explicitly support KBool as a kind, separating it from “KUnbounded False 1”. Thanks to Brian Huffman for contributing the changes. This should have no uservisible impact, but comes in handy for internal reasons.
Version 3.0, 20140216
 Support for floatingpoint numbers:
 Preliminary support for IEEEfloating point arithmetic, introducing
the types
SFloat
andSDouble
. The support is still quite new, and Z3 is the only solver that currently features a solver for this logic. Likely to have bugs, both at the SBV level, and at the Z3 level; so any bug reports are welcome!
 Preliminary support for IEEEfloating point arithmetic, introducing
the types
 New backend solvers:
 SBV now supports MathSAT from Fondazione Bruno Kessler and DISIUniversity of Trento. See: http://mathsat.fbk.eu/
 Support allsat calls in the presence of uninterpreted sorts:
 Implement better support for
allSat
in the presence of uninterpreted sorts. Previously, SBV simply rejected runningallSat
queries in the presence of uninterpreted sorts, since it was not possible to generate a refuting model. The model returned by the SMT solver is simply not usable, since it names constants that is not visible in a subsequent run. Eric Seidel came up with the idea that we can actually compute equivalence classes based on a produced model, and assert the constraint that the new model should disallow the previously found equivalence classes instead. The idea seems to work well in practice, and there is also an example program demonstrating the functionality: Examples/Uninterpreted/UISortAllSat.hs
 Implement better support for
 Programmable model extraction improvements:
 Add functions
getModelDictionary
andgetModelDictionaries
, which provide lowlevel access to models returned from SMT solvers. Former forsat
andprove
calls, latter forallSat
calls. Together with the exported utils from theData.SBV.Internals
module, this should allow for expert users to dissect the models returned and do fancier programming on top of SBV.  Add
getModelValue
,getModelValues
,getModelUninterpretedValue
, andgetModelUninterpretedValues
; which further aid in model value extraction.
 Add functions
 Other:
 Allow users to specify the SMTLib logic to use, if necessary. SBV will still pick the logic automatically, but users can now override that choice. Comes in handy when playing with custom logics.
 Bug fixes:
 Address allsatlaziness issue (#78 in github issue tracker). Essentially, simplify how allsat is called so we can avoid calling the solver for solutions that are not needed. Thanks to Eric Seidel for reporting.
 Examples:
 Add Data/SBV/Examples/Misc/ModelExtract.hs as a simple example for programmable model extraction and usage.
 Add Data/SBV/Examples/Misc/Floating.hs for some FP examples.
 Use the AUFLIA logic in Examples.Existentials.Diophantine which helps z3 complete the proof quickly. (The BV logics take too long for this problem.)
Version 2.10, 20130322
 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 SMTLib competition it won both bitvector categories. It is definitely worth trying it out for bitvector problems.
 Changes to the library:
 Generalize types of
allDifferent
andallEqual
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 carryover as a separate boolean bit.  Add
fullMultiplier
: Returns both the lower and higher bits resulting from multiplication.  Use the SMTLib Bool sort to represent SBool, instead of bitvectors of length 1. While this is an underthehood mechanism that should be usertransparent, 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 1to1 match. (Suggested by Thomas DuBuisson.)
 Generalize types of
 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 Z34.3 series.
 Examples:
 Add Examples/Uninterpreted/Shannon.hs: Demonstrating Shannon expansion, boolean derivatives, etc.
 Bugfixes:
 Gracefully handle the case if the backendSMT 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, 20130102

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 SMTLib based solver executable yicessmt. 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 hardcoded 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 solveragnostic way.)

Various improvements to Z3 model parsing routines.

New web page for SBV: http://leventerkok.github.com/sbv/ is now online.
Version 2.8, 20121129
 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.
Version 2.7, 20121021
 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.)
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 strictconcurrency, 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/haskellcafe/2012July/102352.html.)
Version 2.3, 20120720
 Maintanence 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.
Version 2.2, 20120717
 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, 20120524
 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.
Version 2.0, 20120510
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 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
Version 1.4, 20120510
 Interim release for test purposes
Version 1.3, 20120225
 Workaround cabal/hackage issue, functionally the same as release 1.2 below
Version 1.2, 20120225
Library:
 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 detalied 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 woraround 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
Version 1.1, 20120214
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, 20120213
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.
Codegeneration:
 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, 20111228
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 is nonetheless useful by itself.
 Add a “Modelable” class, which simplifies model extraction.
 Add support for quickcheck at the “Symbolic SBool” level. Previously SBV only allowed functions returning SBool to be quickchecked, which forced a certain style of coding. In particular with the addition of quantifiers, the new coding style mostly puts the toplevel expressions in the Symbolic monad, which were not quickcheckable 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, 20111205
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 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 bitvectors, which has a decidable theory. With the addition of unbounded Integers and quantifiers, the solvers can now return unknown. This should still be rare in practice, but can happen with the use of nonlinear constructs. (i.e., multiplication of two variables.)
Version 0.9.22, 20111113
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 freevariables appropriately using forall/exists functions, and the solver translates them accordingly. Note that this is a nonbackwards 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 SMTsolver 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 SMTLib2 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 will 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, 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, 20110805
Code generation:
 Allow for inclusion of user makefiles
 Allow for CCFLAGS to be set by the user
 Other minor cleanup
Version 0.9.20, 20110605
Regression on 0.9.19; add missing file to cabal
Version 0.9.19, 20110605
 Add SignCast class for conversion between signed/unsigned quantities for samesized bitvectors
 Add fullbinary 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 lookup.
 Expose HasSignAndSize class through Data.SBV.Internals
 Many minor improvements, file reorgs
Examples:
 Add sentencecounting example
 Add an implementation of RC4
Version 0.9.18, 20110407
Code:
 Reengineer codegeneration, 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 Clibraries, allowing code generation for a set of functions that work together.
Examples:
 Update codegeneration examples to use the new API.
 Include a librarygeneration example for doing 128bit AES encryption
Version 0.9.17, 20110329
Code:
 Simplify and reorganize the test suite
Examples:
 Improve AES decryption example, by using tablelookups in InvMixColumns.
Version 0.9.16, 20110328
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 codegenerator
Version 0.9.15, 20110324
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 twos 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, 20110319
 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, 20110316
Bug fixes:
 Make sure SBool shortcut evaluations are done as early as possible, as these help with coding recursiondepth based algorithms, when dealing with symbolic termination issues.
Examples:
 Add fibonacci codegeneration example, original code by Lee Pike.
 Add a GCD codegeneration/verification example
Version 0.9.12, 20110310
New features:
 Add support for compilation to C
 Add a mechanism for offline saving of SMTLib files
Bug fixes:
 Output naming bug, reported by Josef Svenningsson
 Specification bug in Legatos multipler example
Version 0.9.11, 20110216
 Make ghc7.0 happy, minor reorg on the cabal file/Setup.hs
Version 0.9.10, 20110215
 Integrate commits from Iavor: Generalize SBVs 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, 20110123
 Support for userdefined SMTLib axioms to be specified for uninterpreted constants/functions
 Move to using doctest style inline tests
Version 0.9.8, 20110122
 Better support for uninterpretedfunctions
 Support counterexamples with SArrays
 LadnerFischer scheme example
 Documentation updates
Version 0.9.7, 20110118
 First stable public hackage release
Versions 0.0.0  0.9.6, Mid 2010 through early 2011
 Basic infrastructure, design exploration