Releases: lsrcz/grisette
Releases · lsrcz/grisette
v0.8.0.0
Added
- Added pretty printer for models. (#225)
- Added support for algebraic reals (
AlgReal
andSymAlgReal
). (#228, #229) - Added support for quantifiers. (#230)
- Added
SafeFdiv
,SafeLogBase
,DivOr
,FdivOr
, andLogBaseOr
. (#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
, andfpMaximumNumber
operations. (#235) - Add conversion from and to floating points. (#236)
- Add
SymFiniteBits
. (#237) - Add unified instances for all provided operations, including
FP
andAlgReal
. (#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
andliftPFormatList2
. (#225) - [Breaking] Changed the term representation with a compile-time tag for its kind (
AnyKind
for all symbols andConstantKind
for symbols other than uninterpreted functions). This also affects the 'ExtractSym'. A newextractSymMaybe
will regard this tag if not all symbols can be casted to that tag.extractSym
will always succeed, returning a set withAnyKind
. (#230) - [Breaking]
SafeDivision
renamed toSafeDiv
. (#231) - Refined the template-haskell-based derivation mechanism. (#238)
- [Breaking]
GetData
is made injective by givingIdentity
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 beMergeable
. This enable us to merge the results for converting fromUnion a
toUnion b
again. (#244)
Removed
v0.7.0.0
Added
- Added
true
andfalse
inLogicalOp
. (#211) - Exported the
FP
constructs in theGrisette
module. (#209) - Added missing
AllSyms
instance forWordN
,IntN
, andFP
. (#209) - Added unified interfaces. (#210, #212, #213, #214, #215, #217)
- Added
IEEEFPRoundingMode
. (#219) - Added
Show
instance forSomeSym
. (#219) - Added incoherent conversions (
ToSym
,ToCon
) from/toIdentity a
anda
. (#221)
Fixed
- Fixed the printing of FP terms. (#219)
Changed
- [Breaking] Relaxed constraints for type classes, according to haskell/core-libraries-committee#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 haskell/core-libraries-committee#10. (#216) - [Breaking] Renamed
UnionMergeable1
toSymBranching
. RenamedUnion
toUnionBase
, andUnionM
toUnion
. (#214, #217) - [Breaking] Renamed
EvaluateSym
toEvalSym
. RenamedSubstituteSym
toSubstSym
. RenamedExtractSymbolics
toExtractSym
. (#217) - [Breaking] Renamed
SEq
toSymEq
. RenamedSOrd
toSymOrd
. (#217) - [Breaking] Renamed
GPretty
toPPrint
. (#217, #224) - [Breaking] Discourage the use of approximation with
approx
.precise
is now the default and we do not requireprecise
to be used everytime we call a solver. (#218)
v0.6.0.0
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)
v0.5.0.1
v0.5.0.0
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
andmtl
packages. (#171) - Improved the partial evaluation for bit vectors. (#176)
- Added
symRotateNegated
andsymShiftNegated
. (#181) - Added
mrg
andsym
variants for all reasonable operations fromControl.Monad
,Control.Applicative
,Data.Foldable
,Data.List
, andData.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
andrem
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
andUnionPrjOp
interface, added theTryMerge
andPlainUnion
interface. This allowsmrg*
operations to be used with non-union programs. (#170) - [Breaking] Refined the safe operations interface using
TryMerge
. (#172) - [Breaking] Renamed
safeMinus
tosafeSub
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 somemrg*
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 toIdentifier
andSymbol
types. (#192) - Changed the internal representation of the terms. (#193)
- [Breaking] Refactored the project structures. (#194)
v0.4.1.0
v0.4.0.0
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 runFreshT
with merging. (#140) - Added
Grisette.Data.Class.SignConversion.SignConversion
for types fromData.Int
andData.Word
. (#142) - Added shift functions by symbolic shift amounts. (#151)
- Added
apply
for uninterpreted functions. (#155) - Added
liftFresh
to lift aFresh
intoMonadFresh
. (#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
andSymIntegerOp
. (#146) - [Breaking] Removed
ExtractSymbolics
instance forSymbolSet
. (#146)
Fixed
- Removed the quotation marks around the pretty printed results for string-like data types. (#127)
- Fixed the
SOrd
instance forVerificationConditions
. (#131) - Fixed the missing
SubstituteSym
instance forUnionM
. (#131) - Fixed the symbolic generation order for
Maybe
. (#131) - Fixed the
toInteger
function forIntN 1
. (#143) - Fixed the
abs
function forWordN
. (#144) - Fixed the QuickCheck shrink function for
WordN 1
andIntN 1
. (#149) - Fixed the heap overflow bug for
shiftL
forWordN
andIntN
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
toData.Text.Text
. (#141) - [Breaking]
Grisette.Data.Class.BitVector.BVSignConversion
is nowGrisette.Data.Class.SignConversion.SignConversion
. (#142) - [Breaking] Moved the
ITEOp
,LogicalOp
, andSEq
type classes to dedicated modules. (#146) - [Breaking] Moved
Grisette.Data.Class.Evaluate
toGrisette.Data.Class.EvaluateSym
. (#146) - [Breaking] Moved
Grisette.Data.Class.Substitute
toGrisette.Data.Class.SubstituteSym
. (#146) - [Breaking] Split the
Grisette.Data.Class.SafeArith
module toGrisette.Data.Class.SafeDivision
andGrisette.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)
v0.3.1.1
v0.3.1.0
v0.3.0.0
Added
- Added the conversion between signed and unsigned bit vectors. (#69)
- Added the generation of
SomeSymIntN
andSomeSymWordN
from a singleInt
for bit width. (#73) - Added the
FiniteBits
instance forSomeSymIntN
andSomeSymWordN
. (#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
andSomeWordN
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)