Skip to content

v0.4.0.0
Compare
Choose a tag to compare
@lsrcz lsrcz released this 09 Jan 03:29
· 496 commits to main since this release
v0.4.0.0
e84e1c8

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)
Assets 2
Loading