# Changelog All notable changes to this project will be documented in this file. The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). ## [0.4.1.0] -- 2024-01-10 ### Added - Added `cegisForAll` interfaces. ([#165])(https://github.com/lsrcz/grisette/pull/165) ## [0.4.0.0] -- 2024-01-08 ### Added - Added wrappers for state transformers. ([#132](https://github.com/lsrcz/grisette/pull/132)) - Added `toGuardList` function. ([#137](https://github.com/lsrcz/grisette/pull/137)) - Exported some previously hidden API (`BVSignConversion`, `runFreshTFromIndex`) that we found useful or forgot to export. ([#138](https://github.com/lsrcz/grisette/pull/138), [#139](https://github.com/lsrcz/grisette/pull/139)) - Provided `mrgRunFreshT` to run `FreshT` with merging. ([#140](https://github.com/lsrcz/grisette/pull/140)) - Added `Grisette.Data.Class.SignConversion.SignConversion` for types from `Data.Int` and `Data.Word`. ([#142](https://github.com/lsrcz/grisette/pull/142)) - Added shift functions by symbolic shift amounts. ([#151](https://github.com/lsrcz/grisette/pull/151)) - Added `apply` for uninterpreted functions. ([#155](https://github.com/lsrcz/grisette/pull/155)) - Added `liftFresh` to lift a `Fresh` into `MonadFresh`. ([#156](https://github.com/lsrcz/grisette/pull/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](https://github.com/lsrcz/grisette/pull/159)) - Added a new generic CEGIS interface. This allows any verifier/fuzzer to be used in the CEGIS loop. ([#159](https://github.com/lsrcz/grisette/pull/159)) ### Removed - [Breaking] Removed the `Grisette.Lib.Mtl` module. ([#132](https://github.com/lsrcz/grisette/pull/132)) - [Breaking] Removed `SymBoolOp` and `SymIntegerOp`. ([#146](https://github.com/lsrcz/grisette/pull/146)) - [Breaking] Removed `ExtractSymbolics` instance for `SymbolSet`. ([#146](https://github.com/lsrcz/grisette/pull/146)) ### Fixed - Removed the quotation marks around the pretty printed results for string-like data types. ([#127](https://github.com/lsrcz/grisette/pull/127)) - Fixed the `SOrd` instance for `VerificationConditions`. ([#131](https://github.com/lsrcz/grisette/pull/131)) - Fixed the missing `SubstituteSym` instance for `UnionM`. ([#131](https://github.com/lsrcz/grisette/pull/131)) - Fixed the symbolic generation order for `Maybe`. ([#131](https://github.com/lsrcz/grisette/pull/131)) - Fixed the `toInteger` function for `IntN 1`. ([#143](https://github.com/lsrcz/grisette/pull/143)) - Fixed the `abs` function for `WordN`. ([#144](https://github.com/lsrcz/grisette/pull/143)) - Fixed the QuickCheck shrink function for `WordN 1` and `IntN 1`. ([#149](https://github.com/lsrcz/grisette/pull/149)) - Fixed the heap overflow bug for `shiftL` for `WordN` and `IntN` by large numbers. ([#150](https://github.com/lsrcz/grisette/pull/150)) ### Changed - Reorganized the files for `MonadTrans`. ([#132](https://github.com/lsrcz/grisette/pull/132)) - [Breaking] Changed the name of `Union` constructors and patterns. ([#133](https://github.com/lsrcz/grisette/pull/133)) - The `Union` patterns, when used as constructors, now merges the result. ([#133](https://github.com/lsrcz/grisette/pull/133)) - Changed the symbolic identifier type from `String` to `Data.Text.Text`. ([#141](https://github.com/lsrcz/grisette/pull/141)) - [Breaking] `Grisette.Data.Class.BitVector.BVSignConversion` is now `Grisette.Data.Class.SignConversion.SignConversion`. ([#142](https://github.com/lsrcz/grisette/pull/142)) - [Breaking] Moved the `ITEOp`, `LogicalOp`, and `SEq` type classes to dedicated modules. ([#146](https://github.com/lsrcz/grisette/pull/146)) - [Breaking] Moved `Grisette.Data.Class.Evaluate` to `Grisette.Data.Class.EvaluateSym`. ([#146](https://github.com/lsrcz/grisette/pull/146)) - [Breaking] Moved `Grisette.Data.Class.Substitute` to `Grisette.Data.Class.SubstituteSym`. ([#146](https://github.com/lsrcz/grisette/pull/146)) - [Breaking] Split the `Grisette.Data.Class.SafeArith` module to `Grisette.Data.Class.SafeDivision` and `Grisette.Data.Class.SafeLinearArith`. ([#146](https://github.com/lsrcz/grisette/pull/146)) - [Breaking] Changed the API to `MonadFresh`. ([#156](https://github.com/lsrcz/grisette/pull/156)) - [Breaking] Renamed multiple symbolic operators. ([#158](https://github.com/lsrcz/grisette/pull/158)) - [Breaking] Changed the solver interface. ([#159](https://github.com/lsrcz/grisette/pull/159)) - [Breaking] Changed the CEGIS solver interface. ([#159](https://github.com/lsrcz/grisette/pull/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](https://github.com/lsrcz/grisette/pull/95)) - Added `Arbitrary` instances for bit vectors. ([#97](https://github.com/lsrcz/grisette/pull/97)) - Added pretty printers for Grisette data types. ([#101](https://github.com/lsrcz/grisette/pull/101)) - Added `ExtractSymbolics` instances for tuples longer than 2. ([#103](https://github.com/lsrcz/grisette/pull/103)) ### Fixed - Fixed the `Read` instance for bit vectors. ([#99](https://github.com/lsrcz/grisette/pull/99), [#100](https://github.com/lsrcz/grisette/pull/100)) ## [0.3.0.0] -- 2023-07-07 ### Added - Added the conversion between signed and unsigned bit vectors. ([#69](https://github.com/lsrcz/grisette/pull/69)) - Added the generation of `SomeSymIntN` and `SomeSymWordN` from a single `Int` for bit width. ([#73](https://github.com/lsrcz/grisette/pull/73)) - Added the `FiniteBits` instance for `SomeSymIntN` and `SomeSymWordN`. ([#83](https://github.com/lsrcz/grisette/pull/83)) - Added more flexible instances for symbolic generation for `Either`, `Maybe` and list types. ([#84](https://github.com/lsrcz/grisette/pull/84)) - Added an experimental `GenSymConstrained` type class. ([#89](https://github.com/lsrcz/grisette/pull/89)) ### Changed - Changed the operations for `SomeIntN` and `SomeWordN` to accepting dynamic runtime integers rather than compile-time integers. ([#71](https://github.com/lsrcz/grisette/pull/71)) - Comparing the equality of `SomeIntN`/`SomeWordN`/`SomeSymIntN`/`SomeSymWordN` with different bit widths returns false rather than crash now. ([#74](https://github.com/lsrcz/grisette/pull/74)) ### Fixed - Fixed the compatibility issue with sbv 10+. ([#66](https://github.com/lsrcz/grisette/pull/66)) - Fixed build error with newer GHC. ([#70](https://github.com/lsrcz/grisette/pull/70)) - Fixed the merging for `SomeSymIntN` and `SomeSymWordN`. ([#72](https://github.com/lsrcz/grisette/pull/72)) ## [0.2.0.0] - 2023-04-13 ### Added - Add term size count API. ([#48](https://github.com/lsrcz/grisette/pull/48), [#53](https://github.com/lsrcz/grisette/pull/53)) - Add timeout to solver interface. ([#49](https://github.com/lsrcz/grisette/pull/49), [#50](https://github.com/lsrcz/grisette/pull/50)) - Add parallel do-notation for parallel symbolic compilation. ([#51](https://github.com/lsrcz/grisette/pull/51)) - Added some missing instances for symbolic values and bit vectors. ([#46](https://github.com/lsrcz/grisette/pull/46), [#61](https://github.com/lsrcz/grisette/pull/61)) - Add missing instances for `MonadFresh` and `FreshT`. ([#59](https://github.com/lsrcz/grisette/pull/59)) ### Changed - New safe operator interfaces. ([#56](https://github.com/lsrcz/grisette/pull/56)) - Redesigned symbolic value interface. - `Sym Bool`/`Sym Integer`, etc., are no longer available and are replaced with `SymBool` and `SymInteger`. ([#41](https://github.com/lsrcz/grisette/pull/41)) - New symbolic bit vector interface. Added unsized bit vector. ([#41](https://github.com/lsrcz/grisette/pull/41)) ### Removed - Dropped merging cache for `UnionM`. This fixed some segmentation fault errors. ([#43](https://github.com/lsrcz/grisette/pull/43)) ### Fixed - Fix CEGIS when no symbolic input is present. ([#52](https://github.com/lsrcz/grisette/pull/52)) - Fix overlapping `ToSym` and `ToCon` instances. ([#54](https://github.com/lsrcz/grisette/pull/54)) - Fix uninterpreted function lowering. ([#57](https://github.com/lsrcz/grisette/pull/57), [#58](https://github.com/lsrcz/grisette/pull/58)) - Fix CEGIS crash when subsequent solver calls introduces new symbolic constant. ([#60](https://github.com/lsrcz/grisette/pull/60)) ## [0.1.0.0] - 2023-01-20 ### Added - Initial release for Grisette. [0.4.1.0]: https://github.com/lsrcz/grisette/compare/v0.4.1.0...v0.4.0.0 [0.4.0.0]: https://github.com/lsrcz/grisette/compare/v0.4.0.0...v0.3.1.0 [0.3.1.1]: https://github.com/lsrcz/grisette/compare/v0.3.1.0...v0.3.1.1 [0.3.1.0]: https://github.com/lsrcz/grisette/compare/v0.3.0.0...v0.3.1.0 [0.3.0.0]: https://github.com/lsrcz/grisette/compare/v0.2.0.0...v0.3.0.0 [0.2.0.0]: https://github.com/lsrcz/grisette/compare/v0.1.0.0...v0.2.0.0 [0.1.0.0]: https://github.com/lsrcz/grisette/tree/v0.1.0.0