grisette

Symbolic evaluation as a library

https://github.com/lsrcz/grisette#readme

Version on this page:0.11.0.0
LTS Haskell 24.2:0.13.0.1
Stackage Nightly 2025-08-02:0.13.0.1
Latest on Hackage:0.13.0.1

See all snapshots grisette appears in

BSD-3-Clause licensed by Sirui Lu, Rastislav Bodík
Maintained by Sirui Lu ([email protected])
This version can be pinned in stack with:grisette-0.11.0.0@sha256:9daeea607f2ddaea81c0245c0919c2768d59fdb70bff497ace3e3e701af53170,21947

Module documentation for 0.11.0.0

Grisette

Haskell Tests Hackage Version

Grisette is a symbolic evaluation library for Haskell. By translating programs into SMT constraints, Grisette can help the development of program reasoning tools, including verification and synthesis.

For a detailed description of the system, please refer to our POPL’23 paper Grisette: Symbolic Compilation as a Functional Programming Library.

Design and Benefits

  • Separate the concern of problem modeling and symbolic compilation. Users only need to focus on modeling the problem and write interpreters, and the symbolic compilation algorithms are provided by Grisette.
  • Supports rich theories including booleans, uninterpreted functions, bitvectors, integers, real numbers, and floating points.
  • Multi-path symbolic evaluation with efficient state merging, suitable for whole program verification, program synthesis, and other symbolic reasoning tasks.
  • Modular purely functional design, with a focus on composability.
    • Use our familiar Haskell facilities like Either to maintain exceptions (e.g., assertions and assumptions).
    • Allows for symbolic evaluation of user-defined data structures / data structures from third-party libraries.
    • Allows for memoization / parallelization of symbolic evaluation.
  • Core multi-path symbolic evaluation semantics modeled as a monad, allowing for easy integration with other monadic effects, for example:
    • error handling via ExceptT,
    • stateful computation via StateT,
    • unstructured control flow via ContT, etc.

Installation

Install Grisette

Grisette is available on Hackage and Stackage. You can add it to your project with cabal, and we also provided a stack template for quickly starting a new project with Grisette.

Manually writing cabal file

Grisette is a library and is usually used as a dependency of other packages. You can add it to your project’s .cabal file:

library
  ...
  build-depends: grisette >= 0.11 < 0.12

Using stack

Note: Grisette on Stackage is currently outdated. Please make sure to use extra-deps to get the latest version of Grisette from stackage. In your stack.yaml file, add:

extra-deps:
  - grisette-0.11.0.0

and in your package.yaml file:

dependencies:
  - grisette >= 0.11 < 0.12

Quick start template with stack new

You can quickly start an stack-based Grisette project with stack new:

$ stack new <projectname> github:lsrcz/grisette

For more details, please see the template file and the documentation for stack templates.

You can test your installation by running the following command:

$ stack run app

The command assumes a working Z3 available through PATH. You can install it with the instructions below.

Install SMT Solvers

To run the examples, you need to install an SMT solver and make it available through PATH. We recommend that you start with Z3, as it supports all our examples and is usually easier to install. Boolector and its successor Bitwuzla are usually significantly more efficient on bit vectors.

Install Z3

On Ubuntu, you can install Z3 with:

$ apt update && apt install z3

On macOS, with Homebrew, you can install Z3 with:

brew install z3

You may also build Z3 from source, which may be more efficient on your system. Please refer to the Z3 homepage for the build instructions.

Install Boolector/Bitwuzla

Boolector/Bitwuzla from major package managers are usually outdated or inexist. We recommend that you build them from source with the CaDiCaL SAT solver. Please refer to the Boolector homepage and Bitwuzla homepage for the build instructions.

Example

The following example uses Grisette to build a symbolic domain-specific language for boolean and integer expressions.

We will

  • define the syntax and semantics of an arithmetic language, and
  • build a verifier to check if a given arithmetic expression is equivalent to another, and
  • build a synthesizer to find an arithmetic expression that is equivalent to a given expression.

Defining the Syntax

Our language is a simple boolean and integer expression language, following the grammar:

Expr -> IntExpr | BoolExpr
IntExpr -> IntVal int
         | Add IntExpr IntExpr
         | Mul IntExpr IntExpr
BoolExpr -> BoolVal bool
          | BAnd BoolExpr BoolExpr
          | BOr BoolExpr BoolExpr
          | Eq Expr Expr

A symbolic expression can be represented in Grisette as a GADT as follows. In the GADT,

  • SymInteger and SymBool are symbolic (primitive) types, and they represent SMT terms of integer and boolean theories, respectively.
  • Union represents choices of symbolic expressions, and we introduce it to represent program spaces and allow the synthesizer to choose operands from different symbolic expressions.
  • BasicSymPrim is a constraint that contains all the symbolic primitive types that Grisette supports, including SymInteger and SymBool.
data Expr a where
  IntVal :: SymInteger -> IntExpr
  BoolVal :: SymBool -> BoolExpr
  Add :: IntUExpr -> IntUExpr -> IntExpr
  Mul :: IntUExpr -> IntUExpr -> IntExpr
  BAnd :: BoolUExpr -> BoolUExpr -> BoolExpr
  BOr :: BoolUExpr -> BoolUExpr -> BoolExpr
  Eq :: (BasicSymPrim a) => UExpr a -> UExpr a -> BoolExpr

type IntExpr = Expr SymInteger
type BoolExpr = Expr SymBool
type UExpr a = Union (Expr a)
type IntUExpr = UExpr SymInteger
type BoolUExpr = UExpr SymBool

To make this GADT works well with Grisette, we need to derive some instances and get some smart constructors:

  • deriveGADT provides instances for data types that are frequently used with or provided by Grisette. See the documentation for the details on what instances are provided.
  • makeSmartCtor generates smart constructors for the GADT.
deriving instance Show (Expr a)
deriveGADT [''Expr] basicClasses0
makeSmartCtor ''Expr

> intVal 1 :: IntUExpr -- smart constructor for IntVal in Unions
{IntVal 1}
-- Add takes two IntUExprs, use the smart constructors
> Add (intVal "a") (intVal 1)
Add {IntVal a} {IntVal 1}

The introduction of Union allows us to represent choices of expressions, and the following code chooses between a + 2 or a * 2. A synthesizer can then pick true or false for the choice variable to decide which expression to pick. If the synthesizer picks true, the result is a + 2; otherwise, it is a * 2.

add2 = add (intVal "a") (intVal 2)
mul2 = mul (intVal "a") (intVal 2)
> mrgIf "choice" add2 mul2 :: IntUExpr
{If choice {Add {IntVal a} {IntVal 2}} {Mul {IntVal a} {IntVal 2}}}

Defining the Semantics

The semantics of the expressions can be defined by the following interpreter. Grisette provides various combinators for working with symbolic values. In the interpreter, the .# operator is very important. It conceptually

  • extracts all the choices from the Union container,
  • apply the eval function to each choice, and
  • merge the results into a single value.
eval :: Expr a -> a
eval (IntVal a) = a
eval (BoolVal a) = a
eval (Add a b) = eval .# a + eval .# b
eval (Mul a b) = eval .# a * eval .# b
eval (BAnd a b) = eval .# a .&& eval .# b
eval (BOr a b) = eval .# a .|| eval .# b
eval (Eq a b) = eval .# a .== eval .# b

There are other operators like .==, .&&, .||, etc. These operators are provided by Grisette and have symbolic semantics. They construct constraints instead of evaluating to a concrete value.

We may also write eval with do-notations as Union is a monad. Please refer to the tutorials for more details.

Get a verifier

With the syntax and semantics defined, we can build a verifier to check if two expressions are equivalent. This can be done by checking if there exists a counter-example that falsifies the equivalence of the two expressions.

In the following code, we verify that $a+b$ and $b+a$ are equivalent, as there does not exist a counter-example that makes the two expressions evaluate to different values.

aPlusB = Add (intVal "a") (intVal "b")
bPlusA = Add (intVal "b") (intVal "a")
aPlusA = Add (intVal "a") (intVal "a")

> solve z3 $ eval aPlusB ./= eval bPlusA
Left Unsat

In the following code, we verify that $a+b$ and $a+a$ are not equivalent, as there exists a counter-example that makes the two expressions evaluate to different values. The counter-example is $a=0$, $b=1$, such that $a+b=1$ and $a+a=0$.

> solve z3 $ eval aPlusB ./= eval aPlusA
Right (Model {a -> 0 :: Integer, b -> 1 :: Integer})

Get a synthesizer

We can also build a synthesizer using the built-in CEGIS algorithm in Grisette. Given a target expression, we can synthesize an expression using a sketch with “symbolic holes” that is equivalent to the target expression.

In the following code, we synthesize an expression that is equivalent to $a+a$ using a sketch with a “symbolic hole” $c$. The cegisForAll function treats all the variables in the sketch but not in the target expression as holes to fill in.

target = Add (intVal "a") (intVal "a")
sketch = Mul (intVal "a") (intVal "c")

> cegisForAll z3 target $ cegisPostCond $ eval target .== eval sketch
([],CEGISSuccess (Model {c -> 2 :: Integer}))

The complete code is at examples/basic/Main.hs. More examples are available in Grisette’s tutorials.

Documentation

  • Haddock documentation at grisette.
  • A tutorial to Grisette is in the tutorials directory. They are provided as jupyter notebooks with the IHaskell kernel.

License

The Grisette library is distributed under the terms of the BSD3 license. The LICENSE file contains the full license text.

Note

Grisette is fully compatible with GHC 9.6+, and works in most cases with GHC 8.10+.

CLC proposal #10

As the type classes provided by Grisette implements CLC proposal #10, which requires base-4.18.0.0 to work reliably, Grisette is fully compatible with GHC 9.6. You may experience instance resolution failure when using older GHCs in the client code (Grisette itself is buildable against GHC 8.10+ with some tricks).

Quantifiers

Grisette currently supports universal and existential quantifiers $\forall$ and $\exists$, but only when building with sbv >= 10.1. This also means that you need to use GHC >= 9.2.

Floating-points

Grisette currently supports boolean, uninterpreted functions, bitvector, integer, and floating point theories. However, if you want to use the floating point theory, please make sure that you have the latest libBF (>=0.6.8) and sbv installed (>=10.10.6). We’ve detected and fixed several bugs that would prevent a sound reasoning for floating points.

Unified interfaces

Since 0.7.0.0, Grisette provides a unified interface to symbolic and concrete evaluations. GHC 9.0 or earlier, without the QuickLook type inference algorithm for impredicative types, may fail to resolve some constraints. You may need to provide additional constraints in your code to help the compiler.

Citing Grisette

If you use Grisette in your research, please use the following bibtex entry:

@article{10.1145/3571209,
author = {Lu, Sirui and Bod\'{\i}k, Rastislav},
title = {Grisette: Symbolic Compilation as a Functional Programming Library},
year = {2023},
issue_date = {January 2023},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {7},
number = {POPL},
url = {https://doi.org/10.1145/3571209},
doi = {10.1145/3571209},
abstract = {The development of constraint solvers simplified automated reasoning about programs and shifted the engineering burden to implementing symbolic compilation tools that translate programs into efficiently solvable constraints. We describe Grisette, a reusable symbolic evaluation framework for implementing domain-specific symbolic compilers. Grisette evaluates all execution paths and merges their states into a normal form that avoids making guards mutually exclusive. This ordered-guards representation reduces the constraint size 5-fold and the solving time more than 2-fold. Grisette is designed entirely as a library, which sidesteps the complications of lifting the host language into the symbolic domain. Grisette is purely functional, enabling memoization of symbolic compilation as well as monadic integration with host libraries. Grisette is statically typed, which allows catching programming errors at compile time rather than delaying their detection to the constraint solver. We implemented Grisette in Haskell and evaluated it on benchmarks that stress both the symbolic evaluation and constraint solving.},
journal = {Proc. ACM Program. Lang.},
month = {jan},
articleno = {16},
numpages = {33},
keywords = {State Merging, Symbolic Compilation}
}

Changes

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

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.