All Versions
89
Latest Version
Avg Release Cycle
51 days
Latest Release
1132 days ago

Changelog History
Page 4

  • v6.0 Changes

    May 07, 2017

    • This 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/en-us/research/wp-content/uploads/2016/02/nbjorner-scss2014.pdf

    • SBV now allows for real or integral valued metrics. Goals can be lexicographically (default), independently, or pareto-front optimized. Currently, only the z3 backend supports optimization routines.

      Optimization can be done over bit-vector, 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 "name-of-goal" $ x + 2*y

      Minimizes the arithmetic goal x+2*y, where x and y can be bit-vectors, 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 pareto-fronts.

      Once the objectives are given, a top level call to optimize (similar to prove and sat) performs the optimization.

    • SBV now implements soft-asserts. 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 soft-assertion can be violated by incurring a user-given numeric penalty to satisfy the remaining constraints. The solver then tries to minimize the penalty, i.e., satisfy as many of the soft-asserts 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 case-splitting in a proof to guide the underlying solver through. Here is the list of tactics implemented:

      - `CaseSplit`         : Case-split, with implicit coverage. Bool says whether we should be verbose.
- `CheckCaseVacuity`  : Should the case-splits be checked for vacuity? (Default: True.)
- `ParallelCase`      : Run case-splits in parallel. (Default: Sequential.)
- `CheckConstrVacuity`: Should constraints be checked for vacuity? (Default: False.)
- `StopAfter`         : Time-out given to solver, in seconds.
- `CheckUsing`        : Invoke with check-sat-using command, instead of check-sat
- `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.

    • Name-space clean-up. 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 backwards-compatibility 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 (for Symbolic ()), in order to simplify type signatures

    • SBV now properly adds check-sat commands and other directives in debugging output.

    • New examples:

      • Data.SBV.Examples.Optimization.LinearOpt: Simple linear-optimization example.
      • Data.SBV.Examples.Optimization.Production: Scheduling machines in a shop
      • Data.SBV.Examples.Optimization.VM: Scheduling virtual-machines in a data-center

  • v5.15 Changes

    January 30, 2017
    • Bump up dependency on CrackNum >= 1.9, to get access to hexadecimal floats.
    • Improve time/tracking-print code. Thanks to Iavor Diatchki for the patch.

  • v5.14 Changes

    January 12, 2017

    • Bump up QuickCheck dependency to >= 2.9.2 to avoid the following quick-check bug http://github.com/nick8325/quickcheck/issues/113, which transitively impacted the quick-check as implemented by SBV.

    • Generalize casts between integral-floats, using the rounding mode round-nearest-ties-to-even. 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, 2016

    • Fix 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 space-leaks fixed for better performance. Patch contributed by Robert Dockins.

    • Improved Random instance for Rational. Thanks to Joe Leslie-Hurd for the idea.

  • v5.12 Changes

    June 06, 2016

    • Fix GHC8.0 compilation issues, and warning clean-up. 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 hash-consed 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, 2016

    • Documentation: Fix a bunch of dead http links. Thanks to Andres Sicard-Ramirez for reporting.

    • Additions to the Dynamic API:

      • svSetBit : set a given bit
      • svBlastLE, svBlastBE : Bit-blast 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, 2016

    • 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 "non-model-vars," where we can now tell SBV not to take into account certain variables from a model-building 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 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 SMT-Lib 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.