« Changelog History


sbv v8.8 Release Notes

Release Date: 2020-09-04 // over 3 years ago

    • Reworked uninterpreted sorts. Added new function mkUninterpretedSort to 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 sX for each enumeration constant X, defined to be precisely literal X.

    • 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

      to the SymArray class, 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!