v8.14 ChangesMarch 29, 2021
Improve the fast all-sat algorithm to also support uninterpreted values.
Generalize svTestBit to work on floats, returning the respecting bit in the representation of the float.
Fixes to crack-num facility of how we display floats in detail.
v8.13 ChangesMarch 21, 2021
Generalized floating point: Add support for brain-floats, with type
SFPBFloat, which has 8-bits of exponent and 8-bits of significand. This format is affectionately called "brain-float" because it's often used in modeling neural networks machine-learning applications, offering a wider-range than IEEE's half-float, at the exponse of reduced precision. It has 8-exponent bits and 8-significand bits, including the hidden bit.
Add support for SRational type, rational values built out of the ratio of two integers. Use the module "Data.SBV.Rational", which exports the constructor .% to build rationals. Note that you cannot take numerator and denominator of rationals apart, since SMTLib has no way of storing the rational in a canonical way. Otherwise, symbolic rationals follow the same rules as Haskell's Rational type.
SBV now implements a faster allSat algorithm, which applies in most common use cases. (Essentially, when there are no uninterpreted values or sorts present.) The new algorithm has been measured to be at least an order of magnitude faster or more in common cases as it splits the search space into disjoint models, reducing the burden of accummulated lemmas over multiple calls. (See http://theory.stanford.edu/%7Enikolaj/programmingz3.html#sec-blocking-evaluations for details.)
v8.12 ChangesMarch 09, 2021
- Fix a bug in crackNum for unsigned-integer values, which incorrectly showed a negation sign for values with msb set to 1.
v8.11 ChangesMarch 09, 2021
SBV now supports floating-point numbers with arbitrary exponent and significand sizes. The type is
SFloatingPoint eb sb, where
sbare type-level naturals. In particular, SBV can now reason about half-floats, which are used much more frequently in ML applications. Through the LibBF binding, you can also use these concretely, so if you have a use case for computing with floats, you can use SBV as a vehicle for doing so. The exponent/significand sizes are limited to those supported by the LibBF bindings, though the allowed range is rather large and should not be a limitation in practice. (In particular, you'll most likely run out of memory before you hit precision limits!)
We now support a separate
crackNumparameter in model display. If set to True (default is False), SBV will display numeric values of bounded integers, words, and all floats (SDouble, SFloat, and the new SFloatingPoint) in models in detail, showing how they are laid out in memory. Numbers follow the usual 2's-complement notation if they are signed, bit-vectors if they are not signed, and the floats follow the usual IEEE754 binary layout rules. Similarly, there's now a function crack :: SBV a -> String that does the same for non-model printing contexts.
Changed the isNonModelVar config param to take a String (instead of Text). Simplifies programming.
Changes to make SBV compile with GHC9.0. Thanks to Ryan Scott for the patch.
v8.10 ChangesFebruary 13, 2021
Add "Documentation/SBV/Examples/Misc/NestedArray.hs" to demonstrate how to model multi-dimensional arrays in SBV.
Add "Documentation/SBV/Examples/Puzzles/Murder.hs" as another puzzle example.
Performance updates: Thanks to Jeff Young, SBV now uses better underlying data structures, performing better for heavy use-case scenarios.
SBV now tracks constants more closely in query mode, providing more support for constant arrays in a seamless way. (See #574 for details.)
Pop-calls are now support for Yices and Boolector. (#577)
Changes required to make SBV work with latest version of z3 regarding String and Characters, which now allow for unicode characters. This required renaming of certain recognizers in 'Data.SBV.Char' to restrict them to the Latin1 subset. Otherwise, the changes should be transparent to the end user. Please report any issues you might run into when you use SChar and SString types.
v8.9 ChangesOctober 28, 2020
Rename 'sbvAvailableSolvers' to 'getAvailableSolvers'.
Use SMTLib's int2bv if supported by the backend solver. If not, we still do a manual translation. (CVC4 and z3 support it natively, Yices and MathSAT does not, for which we do the manual translation. ABC and dReal doesn't support the coversion at all, since former doesn't support integers and the latter doesn't support bit-vectors.) Thanks to Martin Lundfall for the initial pull request.
symas a synonym for
uninterpret. This allows us to write expressions of the form
sat $ sym "a" - sym "b" .== (0::SInteger), without resorting to lambda expressions or having to explicitly be in the Symbolic monad.
Added missing instances for overflow-checking arithmetic of arbitrary sized signed and unsigned bitvectors.
In a sat (or allSat) call, also return the values of the uninterpreted values, along with all the explicitly named inputs. Strictly speaking, this is backwards-incompatible, but it the new behavior is consistent with how we handle uninterpreted values in general.
Improve SMTLib logic-detection code to use generics.
v8.8 ChangesSeptember 04, 2020
Reworked uninterpreted sorts. Added new function
mkUninterpretedSortto make declaration of completely uninterpreted sorts easier. In particular, we now automatically introduce the symbolic variant of the type (by prefixing the underlying type with
S) so it becomes automatically available, both for uninterpreted sorts and enumerations. In the latter case, we also automatically introduce the value
sXfor each enumeration constant
X, defined to be precisely
Handle incremental mode table-declarations that depend on freshly declared variables. Thanks to Gergő Érdi for reporting.
Fix a soundness bug in SFunArray caching. Thanks to Gergő Érdi for reporting. See https://github.com/LeventErkok/sbv/issues/541 for details.
Add support for the dReal solver, and introduce the notion of delta-satisfiability, where you can now check properties to be satisfiable against delta-perturbations. See "Documentation.SBV.Examples.DeltaSat.DeltaSat" for a basic example.
Add "extraArgs" parameter to SMTConfig to simplify passing extra command line arguments to the solver.
Add a method
sListArray :: (HasKind a, SymVal b) => b -> [(SBV a, SBV b)] -> array a b
SymArrayclass, which allows for creation of arrays from lists of constant or symbolic lists of pairs. The first argument is the value to use for uninitialized entries. Note that the initializer must be a known constant, i.e., it cannot be symbolic. Latter elements of the list will overwrite the earlier ones, if there are repeated keys.
Thanks to Jan Hrcek, a whole bunch of typos were fixed in the documentation and the source code. Much appreciated!
v8.7 ChangesJune 30, 2020
Add support for concurrent versions of solvers for query problems. Similar to
proveWithAnyetc., except when we have queries. Thanks to Jeffrey Young for the idea and the implementation.
Add "Documentation.SBV.Examples.Misc.Newtypes", demonstrating how to use newtypes over existing symbolic types as symbolic quantities themselves. Thanks to Curran McConnell for the example.
Added new predicate
Added new predicate
distinctExcept. This is same as
distinctexcept you can also provide an ignore list. The elements in the first list will be checked to be distinct from each other, or belong to the second list. This is good for writing constraints that either require a default value or if picked be different from each other for a set of variables. This sort of constraint can be coded in user space, but SBV generates efficient code instead of the obvious quadratic number of constraints.
Add function 'algRealToRational' that can convert an algebraic-real to a Haskell rational. We get an either value: If the algebraic real is exact, then it returns a 'Left' value that represents the value precisely. Otherwise, it returns a 'Right' value, which is only an approximation. Note: Setting 'printRealPrec' in SMTConfig to a higher value will increase the precision at the cost of more computation by the SMT solver.
Removed the 'SMTValue' class. It's functionality was not really needed. If you ever used this class, removing it from your type signatures should fix the issue. (You might have to add SymVal constraint if you did not already have it.) Please get in touch if you used this class in some cunning way and you need its functionality back.
Reworked SBVBenchSuite api, Phase 1 of BenchSuite completed.
Add support for addAxiom command to work in the interactive mode. Thanks to Martin Lundfall for the feedback.
satWithAnyfunctions so they properly kill the solvers that did not terminate first. Previously, they became zombies if they didn't end up quickly. Thanks to Robert Dockins for the investigation and the fix.
Fixed a bug where resetAssertions call was forgetting to restore the array and table contexts. Thanks to Martin Lundfall for reporting.
v8.6 ChangesFebruary 08, 2020
Fix typo in error message. Thanks to Oliver Charles for the patch.
Fix parsing of sequence counter-examples to accommodate recent changes in z3.
Add missing exports related to N-bit words. Thanks to Markus Barenhoff for the patch.
Generalized code-generation functions to accept a function with an arbitrary return type, which was previously just unit. This allows for complicated code-generation scenarios where one code-gen run can produce input to the next.
Scalability improvements for internal data structures. Thanks to Brian Huffman for the patch.
Add interpolation support for Z3, following changes to that solver. Note that SBV now supports two different APIs for interpolation extraction, one for Z3 and the other for MathSAT. This is unfortunate, but necessary since interpolant extraction isn't quite standardized amongst solvers and MathSAT and Z3 use sufficiently different calling mechanisms to warrant their own calls. See 'Documentation.SBV.Examples.Queries.Interpolants' for examples that illustrate both cases.
Add a new argument to
displayModelsfunction to allow rearranging of the results in an 'allSat
call. Strictly speaking this is a backwards breaking change, but substitutingid` for the new argument gives you old functionality, so easy to work-around.
v8.5 ChangesOctober 16, 2019
Changes to compile with GHC 8.8. Thanks to Oliver Charles for the patch.
Minor fix to how kinds are shown for non-standard sizes.
Thanks to Jeffrey Young, SBV now has a performance benchmark test-suite. The framework still new, but should help in the long run to make sure SBV performance doesn't regress on its test-suite, and by extension in general usage.