Changelog for grisette-0.4.1.0

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.

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 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)

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)

No user-facing changes.

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 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)

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)

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

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)