« Changelog History


sbv v8.7 Release Notes

Release Date: 2020-06-30 // almost 4 years ago

    • Add support for concurrent versions of solvers for query problems. Similar to satWithAny, proveWithAny etc., 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 sNotElem, negating sElem.

    • Added new predicate distinctExcept. This is same as distinct except 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.

    • Fixed proveWithAny and satWithAny functions 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.