Changelog History
Page 4

v6.0 Changes
May 07, 2017This is a backwards compatibility breaking release, hence the major version bump from 5.15 to 6.0:
 Most of existing code should work with no changes.
 Old code relying on some features might require extra imports,
since we no longer export some functionality directly from
Data.SBV
. This was done in order to reduce the number of exported items to avoid extra clutter.  Old optimization features are removed, as the new and much improved capabilities should be used instead.
The next two bullets cover new features in SBV regarding optimization, based on the capabilities of the z3 SMT solver. With this release SBV gains the capability optimize objectives, and solve MaxSAT problems; by appropriately employing the corresponding capabilities in z3. A good review of these features as implemented by Z3, and thus what is available in SBV is given in this paper: http://www.microsoft.com/enus/research/wpcontent/uploads/2016/02/nbjornerscss2014.pdf
SBV now allows for real or integral valued metrics. Goals can be lexicographically (default), independently, or paretofront optimized. Currently, only the z3 backend supports optimization routines.
Optimization can be done over bitvector, real, and integer goals. The relevant functions are:
 `minimize`: Minimize a given arithmetic goal  `maximize`: Minimize a given arithmetic goal
For instance, a call of the form
minimize "nameofgoal" $ x + 2*y
Minimizes the arithmetic goal x+2*y, where x and y can be bitvectors, reals, or integers. Such goals will be lexicographically optimized, i.e., in the order given. If there are multiple goals, then user can also ask for independent optimization results, or paretofronts.
Once the objectives are given, a top level call to
optimize
(similar toprove
andsat
) performs the optimization.SBV now implements softasserts. A soft assertion is a hint to the SMT solver that we would like a particular condition to hold if possible. That is, if there is a solution satisfying it, then we would like it to hold. However, if the set of constraints is unsatisfiable, then a softassertion can be violated by incurring a usergiven numeric penalty to satisfy the remaining constraints. The solver then tries to minimize the penalty, i.e., satisfy as many of the softasserts as possible such that the total penalty for those that are not satisfied is minimized.
Note that
assertSoft
works well with optimization goals (minimize/maximize etc.), and are most useful when we are optimizing a metric and thus some of the constraints can be relaxed with a penalty to obtain a good solution.SBV no longer provides the old optimization routines, based on iterative and quantifier based methods. Those methods were rarely used, and are now superseded by the above mechanism. If the old code is needed, please contact for help: They can be resurrected in your own code if absolutely necessary.
(NB. This feature is deprecated in 7.0, see above for its replacement.) SBV now implements tactics, which allow the user to navigate the proof process. This is an advanced feature that most users will have no need of, but can become handy when dealing with complicated problems. Users can, for instance, implement casesplitting in a proof to guide the underlying solver through. Here is the list of tactics implemented:
 `CaseSplit` : Casesplit, with implicit coverage. Bool says whether we should be verbose.  `CheckCaseVacuity` : Should the casesplits be checked for vacuity? (Default: True.)  `ParallelCase` : Run casesplits in parallel. (Default: Sequential.)  `CheckConstrVacuity`: Should constraints be checked for vacuity? (Default: False.)  `StopAfter` : Timeout given to solver, in seconds.  `CheckUsing` : Invoke with checksatusing command, instead of checksat  `UseLogic` : Use this logic, a custom one can be specified too  `UseSolver` : Use this solver (z3, yices, etc.)  `OptimizePriority` : Specify priority for optimization: Lexicographic (default), Independent, or Pareto.
Namespace cleanup. The following modules are no longer automatically exported from Data.SBV:
 `Data.SBV.Tools.ExpectedValue` (computing with expected values)  `Data.SBV.Tools.GenTest` (test case generation)  `Data.SBV.Tools.Polynomial` (polynomial arithmetic, CRCs etc.)  `Data.SBV.Tools.STree` (full symbolic binary trees)
To use the functionality of these modules, users must now explicitly import the corresponding module. Not other changes should be needed other than the explicit import.
Changed the signatures of:
isSatisfiableInCurrentPath :: SBool > Symbolic Bool svIsSatisfiableInCurrentPath :: SVal > Symbolic Bool
to:
isSatisfiableInCurrentPath :: SBool > Symbolic (Maybe SatResult) svIsSatisfiableInCurrentPath :: SVal > Symbolic (Maybe SatResult)
which returns the result in case of SAT. This is more useful than before. This is backwardscompatibility breaking, but is more useful. (Requested by Jared Ziegler.)
Add instance
Provable (Symbolic ())
, which simply stands for returning true for proof/sat purposes. This allows for simpler coding, as constrain/minimize/maximize calls (which return unit) can now be directly sat/prove processed, without needing a final call to return at the end.Add type synonym
Goal
(forSymbolic ()
), in order to simplify type signaturesSBV now properly adds checksat commands and other directives in debugging output.
New examples:
 Data.SBV.Examples.Optimization.LinearOpt: Simple linearoptimization example.
 Data.SBV.Examples.Optimization.Production: Scheduling machines in a shop
 Data.SBV.Examples.Optimization.VM: Scheduling virtualmachines in a datacenter

v5.15 Changes
January 30, 2017 Bump up dependency on CrackNum >= 1.9, to get access to hexadecimal floats.
 Improve time/trackingprint code. Thanks to Iavor Diatchki for the patch.

v5.14 Changes
January 12, 2017Bump up QuickCheck dependency to >= 2.9.2 to avoid the following quickcheck bug http://github.com/nick8325/quickcheck/issues/113, which transitively impacted the quickcheck as implemented by SBV.
Generalize casts between integralfloats, using the rounding mode roundnearesttiestoeven. Previously calls to sFromIntegral did not support conversion to floats since it needed a rounding mode. But it does make sense to support them with the default mode. If a different mode is needed, use the function 'toSFloat' as before, which takes an explicit rounding mode.

v5.13 Changes
October 29, 2016Fix broken links, thanks to Stephan Renatus for the patch.
Code generation: Create directory path if it does not exist. Thanks to Robert Dockins for the patch.
Generalize the type of sFromIntegral, dropping the Bits requirement. In turn, this allowed us to remove sIntegerToSReal, since sFromIntegral can be used instead.
Add support for sRealToSInteger. (Essentially the floor function for SReal.)
Several spaceleaks fixed for better performance. Patch contributed by Robert Dockins.
Improved Random instance for Rational. Thanks to Joe LeslieHurd for the idea.

v5.12 Changes
June 06, 2016Fix GHC8.0 compilation issues, and warning cleanup. Thanks to Adam Foltzer for the bulk of the work and Tom Sydney Kerckhove for the initial patch for 8.0 compatibility.
Minor fix to printing models with floats when the base is 2/16, making sure the alignment is done properly accommodating for the crackNum output.
Wait for external process to die on exception, to avoid spawning zombies. Thanks to Daniel Wagner for the patch.
Fix hashconsed arrays: Previously we were caching based only on elements, which is not sufficient as you can have conflicts differing only on the address type, but same contents. Thanks to Brian Huffman for reporting and the corresponding patch.

v5.11 Changes
January 15, 2016 Fix documentation issue; no functional changes

v5.10 Changes
January 14, 2016Documentation: 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

v5.9 Changes
January 05, 2016Default 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. SeeData/SBV/Examples/Misc/Auxiliary.hs
for an example, and the discussion in http://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.

v5.8 Changes
January 01, 2016 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 exponentiation

v5.7 Changes
December 21, 2015 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.
 Export