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.

0.11.0.0 - 2024-12-29

Added

• Added deriveGADT for deriving all relevant instances for GADTs. (#267)
• Added EvalModeConvertible for a unified constraint for the evaluation modes that can be converted to each other with ToCon and ToSym. (#267)

Changed

• [Breaking] We no longer support direct toCon from a union to a single value or toSym from a single value to a union. These should now be done through mrgToSym, toUnionSym, and unionToCon. (#267)
• [Breaking] Changed the EvalMode tag for Con to C and Sym to S. (#267)

Fixed

• Fixed some missing constraints for unified interfaces. (#267)
• Fixed badly staged types in the lifting of terms. (#267)
• Fixed the Read instance for bit-vectors on GHC 9.12. (#267)

Removed

• Removed old template-haskell-based derivation mechanism. (#267)

0.10.0.0 - 2024-12-11

Added

• SomeBV now allows being used under conditionals even if no bit-width is specified. (#261)
• Added interface to smart constructor generation with decapitalized names. (#263)
• Added SymPrim constraints for symbolic primitive types. (#264)
• Added initial support for type class derivation for GADTs. (#265)

Changed

• [Breaking] Improved the SymFiniteBits interface. (#262)
• [Breaking] Changed the smart constructor generation Template Haskell procedure name to makeSmartCtorWith, makePrefixedSmartCtorWith, makeNamedSmartCtor, and makeSmartCtor. (#263)
• [Breaking] Renamed the evaluation mode tags Con and Sym to C and S. (#264)

0.9.0.0 - 2024-11-07

Added

• Added missing instances for concrete general and tabular functions. (#249)
• Added eval mode constraint on demand. (#250)
• Added support for uninterpreted functions in unified interfaces. (#250)
• Added instances for concrete Ratio type. (#251)
• Added serialization for the core constructs. (#253)
• Added partial evaluation for distinct. (#254)

Changed

• [Breaking] Moved the constraints for the general and tabular functions and simplified their instances declaration. (#249)
• [Breaking] Renamed EvalMode to EvalModeAll, renamed MonadWithMode to MonadEvalModeAll. (#250)
• Improved parallel symbolic evaluation performance. (#252)
• [Breaking] Changed the metadata for identifiers from existential arguments to s-expressions. (#253)
• [Breaking] Changed the solving/cegis results from maintaining the exception themselves to maintaining a textual representation of them. (#253)
• [Breaking] Changed the 'VerifierResult' type for CEGIS to allow it report that the verifier cannot find a counter example. (#257)

Fixed

• Fixed memory leak within the term cache. (#252)
• Fixed printing of bv terms. (#255)
• Fixed solverGenericCEGIS and make it also return the last failing cex. (#256)
• solverGenericCEGIS will only rerun possible verifiers now. This will improve overall verification performance. (#258)
• Fixed a critical bug in the lowering/evalSym/extractSym where the intermediate states are not properly memoized. (#259)

0.8.0.0 - 2024-08-13

Added

• Added pretty printer for models. (#225)
• Added support for algebraic reals (AlgReal and SymAlgReal). (#228, #229)
• Added support for quantifiers. (#230)
• Added SafeFdiv, SafeLogBase, DivOr, FdivOr, and LogBaseOr. (#228, #231)
• Added bitcast from and to Bool, IntN, WordN, FP and their symbolic counterparts when appropriate. (#232)
• Add SymFromIntegral. (#233)
• Add operations for concrete floating point numbers. Add IEEE754-2019 fpMinimum, fpMinimumNumber, fpMaximum, and fpMaximumNumber operations. (#235)
• Add conversion from and to floating points. (#236)
• Add SymFiniteBits. (#237)
• Add unified instances for all provided operations, including FP and AlgReal. (#239, #240, #243)
• Allow the use of number literals for SomeBV. (#245)
• Add symDistinct. (#246, #247)

Fixed

• Fixed model parsing for floating points. (#227)
• Allowed mkUnifiedConstructor to be used with types without modes or args. (#242)

Changed

• [Breaking] Changed the operand order for liftPFormatPrec2 and liftPFormatList2. (#225)
• [Breaking] Changed the term representation with a compile-time tag for its kind (AnyKind for all symbols and ConstantKind for symbols other than uninterpreted functions). This also affects the 'ExtractSym'. A new extractSymMaybe will regard this tag if not all symbols can be casted to that tag. extractSym will always succeed, returning a set with AnyKind. (#230)
• [Breaking] SafeDivision renamed to SafeDiv. (#231)
• Refined the template-haskell-based derivation mechanism. (#238)
• [Breaking] GetData is made injective by giving Identity wrapped type for concrete evaluation instead of the type itself. (#242)
• Changed pprint for Identity to not to print the constructor. (#242)
• Make ToSym requires the target type to be Mergeable. This enable us to merge the results for converting from Union a to Union b again. (#244)

Removed

• Removed fpMin and fpMax, which is removed in IEEE754-2019. (#235)
• Dropped support for post-evaluation approximation. (#241)

0.7.0.0 - 2024-07-02

Added

• Added true and false in LogicalOp. (#211)
• Exported the FP constructs in the Grisette module. (#209)
• Added missing AllSyms instance for WordN, IntN, and FP. (#209)
• Added unified interfaces. (#210, #212, #213, #214, #215, #217)
• Added IEEEFPRoundingMode. (#219)
• Added Show instance for SomeSym. (#219)
• Added incoherent conversions (ToSym, ToCon) from/to Identity a and a. (#221)

Fixed

• Fixed the printing of FP terms. (#219)

Changed

• [Breaking] Relaxed constraints for type classes, according to https://github.com/haskell/core-libraries-committee/issues/10. One problem this causes is that the instances for Union will no longer be able to always merge the results. This is unfortunate, but should not be critical. (#213, #214, #221)
• [Breaking] Rewritten the generic derivation mechanism. (#213, #214, #216)
• [Breaking] Changed the type class hierarchy for operations for functors, e.g. SEq1, as described in https://github.com/haskell/core-libraries-committee/issues/10. (#216)
• [Breaking] Renamed UnionMergeable1 to SymBranching. Renamed Union to UnionBase, and UnionM to Union. (#214, #217)
• [Breaking] Renamed EvaluateSym to EvalSym. Renamed SubstituteSym to SubstSym. Renamed ExtractSymbolics to ExtractSym. (#217)
• [Breaking] Renamed SEq to SymEq. Renamed SOrd to SymOrd. (#217)
• [Breaking] Renamed GPretty to PPrint. (#217, #224)
• [Breaking] Discourage the use of approximation with approx. precise is now the default and we do not require precise to be used everytime we call a solver. (#218)

0.6.0.0 -- 2024-06-07

Added

• Added solving procedures with solver handles. (#198)
• Added overestimateUnionValues. (#203)
• Added pretty printing for hashset and hashmaps. (#205)
• Added support for refinement of solutions in CEGIS algorithm. (#206)
• Added generation of globally unique identifier with uniqueIdentifier. (#206)
• Added support for arbitrary precision floating point theory. (#207)

Fixed

• withSolver now forcifully terminate the solver when exiting the scope. (#199)
• Fixed pretty printing for monad transformers. (#205)

Changed

• [Breaking] Equality test for SomeBV with different bit widths will now return false rather than crash. (#200)
• [Breaking] More intuitive CEGIS interface. (#201)
• [Breaking] Changed the low-level solver interface. (#206)
• [Breaking] Changed the CEGIS interface. (#206)
• Bumped the minimum supported sbv version to 8.17. (#207)

0.5.0.1 -- 2024-04-18

Fixed

• Fix an building error due to a GHC 9.8.1 regression (https://gitlab.haskell.org/ghc/ghc/-/issues/24084). (#195)

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.