« Changelog History


sbv v0.9.24 Release Notes

Release Date: 2011-12-28 // over 12 years ago

  • Library:

    • Add "forSome," analogous to "forAll." (The name "exists" would've been better, but it's already taken.) This is not as useful as one might think as forAll and forSome do not nest, as an inner application of one pushes its argument to a Predicate, making the outer one useless, but it is nonetheless useful by itself.
    • Add a "Modelable" class, which simplifies model extraction.
    • Add support for quick-check at the "Symbolic SBool" level. Previously SBV only allowed functions returning SBool to be quick-checked, which forced a certain style of coding. In particular with the addition of quantifiers, the new coding style mostly puts the top-level expressions in the Symbolic monad, which were not quick-checkable before. With new support, the quickCheck, prove, sat, and allSat commands are all interchangeable with obvious meanings.
    • Add support for concrete test case generation, see the genTest function.
    • Improve optimize routines and add support for iterative optimization.
    • Add "constrain", simplifying conjunctive constraints, especially useful for adding constraints at variable generation time via forall/exists. Note that the interpretation of such constraints is different for genTest and quickCheck functions, where constraints will be used for appropriately filtering acceptable test values in those two cases.
    • Add "pConstrain", which probabilistically adds constraints. This is useful for quickCheck and genTest functions for filtering acceptable test values. (Calls to pConstrain will be rejected for sat/prove calls.)
    • Add "isVacuous" which can be used to check that the constraints added via constrain are satisfiable. This is useful to prevent vacuous passes, i.e., when a proof is not just passing because the constraints imposed are inconsistent. (Also added accompanying isVacuousWith.)
    • Add "free" and "free_", analogous to "forall/forall_" and "exists/exists_" The difference is that free behaves universally in a proof context, while it behaves existentially in a sat context. This allows us to express properties more succinctly, since the intended semantics is usually this way depending on the context. (i.e., in a proof, we want our variables universal, in a sat call existential.) Of course, exists/forall are still available when mixed quantifiers are needed, or when the user wants to be explicit about the quantifiers.

    Examples

    • Add Data/SBV/Examples/Puzzles/Coins.hs. (Shows the usage of "constrain".)

    Dependencies

    • Bump up random package dependency to 1.0.1.1 (from 1.0.0.2)

    Internal

    • Major reorganization of files to and build infrastructure to decrease build times and better layout
    • Get rid of custom Setup.hs, just use simple build. The extra work was not worth the complexity.