Changelog History
Page 6

v4.1 Changes
March 06, 2015Add 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.)

v4.0 Changes
January 22, 2015๐ 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.)

v3.5 Changes
January 15, 2015๐ 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.

v3.4 Changes
December 21, 2014This 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

v3.3 Changes
December 05, 2014Implement '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.

v3.2 Changes
November 18, 2014Implement '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.

v3.1 Changes
July 12, 2014NB: GHC 7.8.1 and 7.8.2 has a serious bug http://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.
 Using multipleSMT solvers in parallel:

v3.0 Changes
February 16, 2014 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.)
 Support for floatingpoint numbers:

v2.10 Changes
March 22, 2013 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.)
 Add support for the Boolector SMT solver

v2.9 Changes
January 02, 2013 Add support for the CVC4 SMT solver from Stanford: https://cvc4.github.io/ 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.