grisette

grisette copied to clipboard

Add refinement to cegis

1

This pull request adds refinement to the cegis procedure. This is useful when we are implementing a cegis procedure with a cost model. The cegis will now try to synthesize...

lsrcz

Add support for microlens

1

This pull request adds the necessary constructs, instances, and mrg variants for microlens combinators for using microlens with Grisette.

lsrcz

When will the tutorials on Grisette be made available?

2

Hello @lsrcz , I am a Rosette user who would like to move to Grisette as soon as possible, but I think I will need tutorials on Grisette to get...

akothen

Standardize the constraints for Mergeable1 and SimpleMergeable1 classes

1

This pull request standardizes the constraints for `*1` classes as described in https://github.com/haskell/core-libraries-committee/issues/10. Resolves #124.

lsrcz

We should align the `*1` classes with the change to the `Eq1` and `Ord1` instances in `base-4.18` (GHC-9.6). The change in `base` is described in https://github.com/haskell/core-libraries-committee/issues/10.

lsrcz

Currently Grisette provides a limited set of wrappers for the library monadic functions to help keep the result merged. We should add more wrappers, e.g., for `StateT`.

lsrcz

Add SymReal Type

1

looking at sbv it has support for both floats of arbitrary precision and rational numbers could grisette add support for them?

eldritch-cookie

Suppose we have a type: ```haskell data AST = Add (UnionM AST) (UnionM AST) | Mul (UnionM AST) (UnionM AST) | Lit SymInteger deriving (Show, Generic) deriving (Mergeable) via (Default...

lsrcz

We need a way to convert from integer/int to bit vectors. An additional bit size parameter is needed so `fromInteger` does not work here.

lsrcz

Update README.md

1

Added instructions on running the example.

rbodik