From a7ee2881e66a57d86317c13cfb7e2b42aa0955e8 Mon Sep 17 00:00:00 2001 From: Sirui Lu Date: Mon, 8 Jan 2024 19:12:45 -0800 Subject: [PATCH] :bookmark: Bump version to 0.4.0.0 --- CHANGELOG.md | 4 ++-- README.md | 25 ++++++++++++++----------- grisette.cabal | 2 +- package.yaml | 2 +- 4 files changed, 18 insertions(+), 15 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2214540e..e9b05fde 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,7 +5,7 @@ All notable changes to this project will be documented in this file. The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). -## [Unreleased] +## [0.4.0.0] -- 2024-01-08 ### Added @@ -125,7 +125,7 @@ No user-facing changes. - Initial release for Grisette. -[Unreleased]: https://github.com/lsrcz/grisette/compare/v0.3.1.0...HEAD +[0.4.0.0]: https://github.com/lsrcz/grisette/compare/v0.4.0.0...v0.3.1.0 [0.3.1.1]: https://github.com/lsrcz/grisette/compare/v0.3.1.0...v0.3.1.1 [0.3.1.0]: https://github.com/lsrcz/grisette/compare/v0.3.0.0...v0.3.1.0 [0.3.0.0]: https://github.com/lsrcz/grisette/compare/v0.2.0.0...v0.3.0.0 diff --git a/README.md b/README.md index 9514f94e..01ac2948 100644 --- a/README.md +++ b/README.md @@ -12,10 +12,10 @@ For a detailed description of the system, please refer to our POPL'23 paper ## Features - **Multi-path** symbolic evaluation with efficient (customizable) state merging. -- Symbolic evaluation is **purely functional**. The propagated symbolic value includes the assertion / error state of the execution, yet it is just a data structure. As a result, Grisette is a library that does not modify the Haskell compiler. -- The separation of symbolic and concrete values is enforced with **static types**. These types help discover opportunities for partial evaluation as well as safe use of Haskell libraries. +- Symbolic evaluation is **purely functional**. The propagated symbolic value includes the assertion / error state of the execution, yet it is just a data structure. As a result, Grisette is a library that does not modify the Haskell compiler. +- The separation of symbolic and concrete values is enforced with **static types**. These types help discover opportunities for partial evaluation as well as safe use of Haskell libraries. -## Design and Benefits +## Design and Benefits - Modular purely functional design, with a focus on composability. - Allows for symbolic evaluation of user-defined data structures / data @@ -47,7 +47,7 @@ packages. You can add it to your project's `.cabal` file: ```cabal library ... - build-depends: grisette >= 0.3 < 0.4 + build-depends: grisette >= 0.4 < 0.5 ``` #### Quick start template with `stack new` @@ -79,7 +79,7 @@ through `PATH`. You can install it with the instructions below. ### Install SMT Solvers -To run the examples, you also need to install an SMT solver and make it +To run the examples, you also need to install an SMT solver and make it available through `PATH`. We recommend that you start with [Z3](https://github.com/Z3Prover/z3), as it supports all our examples and is usually easier to install. @@ -114,17 +114,17 @@ for the build instructions. ## Example -The following example uses Grisette to build a synthesizer of arithmetic programs. Given the input-output pair (2,5), the synthesizer may output the program (\x -> x+3). The example is adapted from [this blog +The following example uses Grisette to build a synthesizer of arithmetic programs. Given the input-output pair (2,5), the synthesizer may output the program (\x -> x+3). The example is adapted from [this blog post](https://www.cs.utexas.edu/~bornholt/post/building-synthesizer.html) by James Bornholt. - The example has three parts: + - We define the arithmetic language. The language is _symbolic_: - its syntax tree represents a set of concrete syntax trees, and - - its interpreter accepts such symbolic syntax trees, and interprete at once all represented concrete syntax trees. -- We define the candidate program space of the synthesizer by creating a particular symbolic syntax tree. The synthesizer will search the space of concrete trees for a solution. -- We interpret the symbolic syntax tree and pass the resulting constraints to the solver. If a solution exists, the solver returns a concrete tree that agrees with the input-out example. + - its interpreter accepts such symbolic syntax trees, and interprete at once all represented concrete syntax trees. +- We define the candidate program space of the synthesizer by creating a particular symbolic syntax tree. The synthesizer will search the space of concrete trees for a solution. +- We interpret the symbolic syntax tree and pass the resulting constraints to the solver. If a solution exists, the solver returns a concrete tree that agrees with the input-out example. ### Defining the Arithmetic Language @@ -183,6 +183,7 @@ data SExpr -- UMrg (Single (SConst 1)) $(makeUnionWrapper "mrg" ''SExpr) ``` + Then we can define the program space. The following code defines a program space `\x -> x + {x, c}`. Some example programs in this space are `\x -> x + x`, `\x -> x + 1`, and `\x -> x + 2`. @@ -239,15 +240,17 @@ For more details, please refer to [the Grisette examples](https://github.com/lsr ## Documentation -- Haddock documentation at [grisette](https://hackage.haskell.org/package/grisette). +- Haddock documentation at [grisette](https://hackage.haskell.org/package/grisette). - Grisette essentials (WIP). - Grisette tutorials (WIP). ## License + The Grisette library is distributed under the terms of the BSD3 license. The [LICENSE](LICENSE) file contains the full license text. ## Citing Grisette + If you use Grisette in your research, please use the following bibtex entry: ```bibtex diff --git a/grisette.cabal b/grisette.cabal index a7bcdf80..69513f30 100644 --- a/grisette.cabal +++ b/grisette.cabal @@ -5,7 +5,7 @@ cabal-version: 1.12 -- see: https://github.com/sol/hpack name: grisette -version: 0.3.1.1 +version: 0.4.0.0 synopsis: Symbolic evaluation as a library description: Grisette is a reusable symbolic evaluation library for Haskell. By translating programs into constraints, Grisette can help the development of diff --git a/package.yaml b/package.yaml index 1408f8a5..e6fcd05c 100644 --- a/package.yaml +++ b/package.yaml @@ -1,5 +1,5 @@ name: grisette -version: 0.3.1.1 +version: 0.4.0.0 synopsis: Symbolic evaluation as a library description: | Grisette is a reusable symbolic evaluation library for Haskell. By