Changelog of @hackage/grisette 0.5.0.1

Changelog

All notable changes to this project will be documented in this file.

The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.

Unreleased

0.5.0.1 -- 2024-04-18

Fixed

0.5.0.0 -- 2024-04-18

Added

  • Added the creation of unparameterized bit vectors from run-time bit-widths. (#168, #177)
  • Added all the functions available for the exception transformer in transformers and mtl packages. (#171)
  • Improved the partial evaluation for bit vectors. (#176)
  • Added symRotateNegated and symShiftNegated. (#181)
  • Added mrg and sym variants for all reasonable operations from Control.Monad, Control.Applicative, Data.Foldable, Data.List, and Data.Traversable. (#182)
  • Added mrgIfPropagatedStrategy. (#184)
  • Added freshString. (#188)
  • Added localFreshIdent. (#190)
  • Added deriving for void types for builtin type classes. (#191)

Fixed

  • Fixed the merging for safe division. (#173)
  • Fixed the behavior for safe mod and rem for signed, bounded concrete types. (#173)
  • Fixed merging in mrg* operations for monad transformers to ensure that they merge the results. (#187)

Changed

  • [Breaking] Removed the UnionLike and UnionPrjOp interface, added the TryMerge and PlainUnion interface. This allows mrg* operations to be used with non-union programs. (#170)
  • [Breaking] Refined the safe operations interface using TryMerge. (#172)
  • [Breaking] Renamed safeMinus to safeSub to be more consistent. (#172)
  • [Breaking] Unifies the implementation for all symbolic non-indexed bit-vectors. The legacy types are now type and pattern synonyms. (#174, #179, #180)
  • [Breaking] Use functional dependency instead of type family for the Function class. (#178)
  • [Breaking] Added Mergeable constraints to some mrg* list operators (#182)
  • [Breaking] Refactored the mrg* constructor related template haskell code. (#185)
  • [Breaking] Dropped symbols with extra information. (#188)
  • [Breaking] The FreshIdent is removed. It is now changed to Identifier and Symbol types. (#192)
  • Changed the internal representation of the terms. (#193)
  • [Breaking] Refactored the project structures. (#194)

0.4.1.0 -- 2024-01-10

Added

  • Added cegisForAll interfaces. (#165)

0.4.0.0 -- 2024-01-08

Added

  • Added wrappers for state transformers. (#132)
  • Added toGuardList function. (#137)
  • Exported some previously hidden API (BVSignConversion, runFreshTFromIndex) that we found useful or forgot to export. (#138, #139)
  • Provided mrgRunFreshT to run FreshT with merging. (#140)
  • Added Grisette.Data.Class.SignConversion.SignConversion for types from Data.Int and Data.Word. (#142)
  • Added shift functions by symbolic shift amounts. (#151)
  • Added apply for uninterpreted functions. (#155)
  • Added liftFresh to lift a Fresh into MonadFresh. (#156)
  • Added a handle types for SBV solvers. This allows users to use SBV solvers without the need to wrap everything in the SBV monads. (#159)
  • Added a new generic CEGIS interface. This allows any verifier/fuzzer to be used in the CEGIS loop. (#159)

Removed

  • [Breaking] Removed the Grisette.Lib.Mtl module. (#132)
  • [Breaking] Removed SymBoolOp and SymIntegerOp. (#146)
  • [Breaking] Removed ExtractSymbolics instance for SymbolSet. (#146)

Fixed

  • Removed the quotation marks around the pretty printed results for string-like data types. (#127)
  • Fixed the SOrd instance for VerificationConditions. (#131)
  • Fixed the missing SubstituteSym instance for UnionM. (#131)
  • Fixed the symbolic generation order for Maybe. (#131)
  • Fixed the toInteger function for IntN 1. (#143)
  • Fixed the abs function for WordN. (#144)
  • Fixed the QuickCheck shrink function for WordN 1 and IntN 1. (#149)
  • Fixed the heap overflow bug for shiftL for WordN and IntN by large numbers. (#150)

Changed

  • Reorganized the files for MonadTrans. (#132)
  • [Breaking] Changed the name of Union constructors and patterns. (#133)
  • The Union patterns, when used as constructors, now merges the result. (#133)
  • Changed the symbolic identifier type from String to Data.Text.Text. (#141)
  • [Breaking] Grisette.Data.Class.BitVector.BVSignConversion is now Grisette.Data.Class.SignConversion.SignConversion. (#142)
  • [Breaking] Moved the ITEOp, LogicalOp, and SEq type classes to dedicated modules. (#146)
  • [Breaking] Moved Grisette.Data.Class.Evaluate to Grisette.Data.Class.EvaluateSym. (#146)
  • [Breaking] Moved Grisette.Data.Class.Substitute to Grisette.Data.Class.SubstituteSym. (#146)
  • [Breaking] Split the Grisette.Data.Class.SafeArith module to Grisette.Data.Class.SafeDivision and Grisette.Data.Class.SafeLinearArith. (#146)
  • [Breaking] Changed the API to MonadFresh. (#156)
  • [Breaking] Renamed multiple symbolic operators. (#158)
  • [Breaking] Changed the solver interface. (#159)
  • [Breaking] Changed the CEGIS solver interface. (#159)

0.3.1.1 -- 2023-09-29

No user-facing changes.

0.3.1.0 -- 2023-07-19

Added

  • Added support to Data.Text. (#95)
  • Added Arbitrary instances for bit vectors. (#97)
  • Added pretty printers for Grisette data types. (#101)
  • Added ExtractSymbolics instances for tuples longer than 2. (#103)

Fixed

  • Fixed the Read instance for bit vectors. (#99, #100)

0.3.0.0 -- 2023-07-07

Added

  • Added the conversion between signed and unsigned bit vectors. (#69)
  • Added the generation of SomeSymIntN and SomeSymWordN from a single Int for bit width. (#73)
  • Added the FiniteBits instance for SomeSymIntN and SomeSymWordN. (#83)
  • Added more flexible instances for symbolic generation for Either, Maybe and list types. (#84)
  • Added an experimental GenSymConstrained type class. (#89)

Changed

  • Changed the operations for SomeIntN and SomeWordN to accepting dynamic runtime integers rather than compile-time integers. (#71)
  • Comparing the equality of SomeIntN/SomeWordN/SomeSymIntN/SomeSymWordN with different bit widths returns false rather than crash now. (#74)

Fixed

  • Fixed the compatibility issue with sbv 10+. (#66)
  • Fixed build error with newer GHC. (#70)
  • Fixed the merging for SomeSymIntN and SomeSymWordN. (#72)

0.2.0.0 - 2023-04-13

Added

  • Add term size count API. (#48, #53)
  • Add timeout to solver interface. (#49, #50)
  • Add parallel do-notation for parallel symbolic compilation. (#51)
  • Added some missing instances for symbolic values and bit vectors. (#46, #61)
  • Add missing instances for MonadFresh and FreshT. (#59)

Changed

  • New safe operator interfaces. (#56)
  • Redesigned symbolic value interface.
    • Sym Bool/Sym Integer, etc., are no longer available and are replaced with SymBool and SymInteger. (#41)
    • New symbolic bit vector interface. Added unsized bit vector. (#41)

Removed

  • Dropped merging cache for UnionM. This fixed some segmentation fault errors. (#43)

Fixed

  • Fix CEGIS when no symbolic input is present. (#52)
  • Fix overlapping ToSym and ToCon instances. (#54)
  • Fix uninterpreted function lowering. (#57, #58)
  • Fix CEGIS crash when subsequent solver calls introduces new symbolic constant. (#60)

0.1.0.0 - 2023-01-20

Added

  • Initial release for Grisette.