Skip to content

Commit

Permalink
Merge pull request #56 from tweag/qa/0.3
Browse files Browse the repository at this point in the history
release version 0.3
  • Loading branch information
qaristote committed Feb 6, 2023
2 parents 366d2f4 + b8955c1 commit 2f5e62a
Show file tree
Hide file tree
Showing 9 changed files with 119 additions and 58 deletions.
39 changes: 30 additions & 9 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,19 +1,40 @@
see also the changelogs of `smtlib-backends-tests`, `smtlib-backends-process` and
`smtlib-backends-z3`
# Changelog

# v0.3-alpha
- **(breaking change)** add a datatype `Backends.QueuingFlag` to set the queuing mode
All notable changes to the smtlib-backends library 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 [PVP versioning](https://pvp.haskell.org/).

The same stands for the changelogs of
[smtlib-backends-tests](smtlib-backends-tests/CHANGELOG.md),
[smtlib-backends-process](smtlib-backends-process/CHANGELOG.md) and
[smtlib-backends-z3](smtlib-backends-z3/CHANGELOG.md), except the version
numbers simply follow that of `smtlib-backends`.

## v0.3 _(2023-02-03)_

### Added
- **(breaking change)** add a datatype `Backends.QueuingFlag` to set the queuing
mode
- the `initSolver` function now takes this datatype as argument instead of a
boolean
- **(breaking change)** add a `send_` method to the `Backends.Backend` datatype
for sending commands with no output
- add a `Backends.flushQueue` function for forcing the content of the queue to
be evaluated

### Changed
- **(breaking change)** make the queuing functions thread-unsafe but faster
- add a `send_` method to the `Backends.Backend` datatype for sending commands with no output
- add a `Backends.flushQueue` function for forcing the content of the queue to be
evaluated

# v0.2
## v0.2 _(2022-12-16)_

### Changed
- split the `Process` module into its own library
- rename `SMTLIB.Backends`'s `ackCommand` to `command_`
- improve read-me

### Removed
- remove logging abilities
- the user can always surround `command` or `command_` with their own logging
functions
- improve read-me
28 changes: 15 additions & 13 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -31,34 +31,36 @@ It requires the libraries `smtlib-backends` and `smtlib-backends-process`.

More examples of how to use the different backends are included in their
respective test-suites:
- [examples for the `Process` backend](smtlib-backends-process/tests/Examples.hs)
- [examples for the `Process`
backend](smtlib-backends-process/tests/Examples.hs)
- [examples for the `Z3` backend](smtlib-backends-z3/tests/Examples.hs)

## Building and testing

This repository provides a reproducible build environment through a [Nix
flake](https://www.tweag.io/blog/2020-05-25-flakes/).

Another option is to manually install Z3 to use the process backend, and the
Z3 C library to use the Z3 backend. Then you can build and test the libraries
using `cabal build` and `cabal test`.
Another option is to manually install Z3 to use the process backend, and the Z3
C library to use the Z3 backend. Then you can build and test the libraries using
`cabal build` and `cabal test`.

## Implementing backends

Currently, backends only need to provide a function to submit queries, as
documented in [SMTLIB.Backends.Backend](src/SMTLIB/Backends.hs). See
[SMTLIB.Backends.Process.toBackend](smtlib-backends-process/src/SMTLIB/Backends/Process.hs) or
[SMTLIB.Backends.Z3.toBackend](smtlib-backends-z3/src/SMTLIB/Backends/Z3.hs) for examples.
[SMTLIB.Backends.Process.toBackend](smtlib-backends-process/src/SMTLIB/Backends/Process.hs)
or [SMTLIB.Backends.Z3.toBackend](smtlib-backends-z3/src/SMTLIB/Backends/Z3.hs)
for examples.

## Motivation

This library was created because there are a lot of Haskell projects using SMT solvers
through SMT-LIB, but most of them only use solvers through external processes
and implement the interaction with the solver themselves. But running solvers
as external processes can be quite slow, hence this library aims to provide
other, more efficient ways to do so. We believe having one well-optimized and
safe library is more efficient than having the same code be spread out between
different projects.
This library was created because there are a lot of Haskell projects using SMT
solvers through SMT-LIB, but most of them only use solvers through external
processes and implement the interaction with the solver themselves. But running
solvers as external processes can be quite slow, hence this library aims to
provide other, more efficient ways to do so. We believe having one
well-optimized and safe library is more efficient than having the same code be
spread out between different projects.

## Contributing

Expand Down
43 changes: 28 additions & 15 deletions smtlib-backends-process/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,32 +1,45 @@
# v0.3-alpha
- make test-suite compatible with `smtlib-backends-0.3`
# Changelog

All notable changes to the smtlib-backends-process library will be documented in
this file.

## v0.3 _(2023-02-03)_

### Added
- add tests for documenting edge cases of the backends
- check that we can pile up procedures for exiting a process
- what happens when sending an empty command
- what happens when sending a command not producing any output
- add `Process.defaultConfig`, synonym for `def`
- improve error messages inside `Process.toBackend`
- add `Process.defaultConfig`
- add `std_err` field in `Config`: the user may now specifiy how to create the
handle for the error channel

### Changed
- make the test-suite compatible with `smtlib-backends-0.3`
- **(breaking change)** use `process` instead of `typed-process` to manage the underlying process
- change the definition of the `Process.Handle` datatype accordingly
- remove `Process.wait`
- there is now a single example in the test-suite showing how to
manage the underlying process and its I/O channels
- improve error messages inside `Process.toBackend`

### Removed
- removed `Process.wait`
- **(breaking change)** removed logging capabilities, this is now on the user to
implement
implement (see also the `underlyingProcess` example)
- remove `Config`'s `reportError` field
- remove `Handle`'s `errorReader` field
- **(breaking change)** removed `Data.Default` instance of `Config`

# v0.2
split `smtlib-backends`'s `Process` module into its own library
## `Config` datatype
- move the logger function into it
- make it an instance of the `Default` typeclass
## logging
- move the logger function into the `Config` datatype
## v0.2 _(2022-12-16)_

### Added
- made `Config` an instance of the `Default` typeclass
- add usage examples in the test-suite

### Changed
- split `smtlib-backends`'s `Process` module into its own library
- move the logger function inside the `Config` datatype
- don't prefix error messages with `[stderr]`
## test-suite
- add usage examples
- make compatible with `smtlib-backends-0.2`
## miscellaneous
- improve documentation
6 changes: 3 additions & 3 deletions smtlib-backends-process/smtlib-backends-process.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@ name: smtlib-backends-process
version: 0.3
synopsis: An SMT-LIB backend running solvers as external processes.
description:
This library implements an SMT-LIB backend (in the sense of the smtlib-backends
package) using by running solvers as external processes.
This library implements an SMT-LIB backend (in the sense of the
smtlib-backends package) which runs solvers as external processes.

license: MIT
license-file: LICENSE
Expand All @@ -22,7 +22,7 @@ source-repository head
source-repository this
type: git
location: https://github.com/tweag/smtlib-backends
tag: 0.2
tag: 0.3
subdir: smtlib-backends-process

library
Expand Down
17 changes: 14 additions & 3 deletions smtlib-backends-tests/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,17 @@
# v0.3-alpha
# Changelog

All notable changes to the smtlib-backends-tests library will be documented in
this file.

## v0.3 _(2023-02-03)_

### Changed
- make test-suite compatible with `smtlib-backends-0.3`

# v0.2
- remove `(exit)` commands at the end of sources
## v0.2 _(2022-12-16)_

### Changed
- make library compatible with `smtlib-backends-0.2`

### Removed
- remove `(exit)` commands at the end of sources
2 changes: 1 addition & 1 deletion smtlib-backends-tests/smtlib-backends-tests.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ source-repository head
source-repository this
type: git
location: https://github.com/tweag/smtlib-backends
tag: 0.2
tag: 0.3
subdir: smtlib-backends-tests

library
Expand Down
32 changes: 23 additions & 9 deletions smtlib-backends-z3/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,16 +1,30 @@
# v0.3-alpha
- make test-suite compatible with `smtlib-backends-0.3`
- **(breaking change)** the `Z3.new` and `Z3.with` functions now take a `Z3.Config`
object as argument, which one may use to set some solver options at initialization
time
- add corresponding examples in the test-suite
- add `Z3.defaultConfig`, synonym for `def`
# Changelog

All notable changes to the smtlib-backends-z3 library will be documented in this
file.

## v0.3 _(2023-02-03)_

### Added
- add `Z3.defaultConfig`
- add tests for documenting edge cases of the backends
- what happens when sending an empty command
- what happens when sending a command not producing any output
- **(breaking change)** removed `Data.Default` instance of `Config`

### Changed
- make test-suite compatible with `smtlib-backends-0.3`
- **(breaking change)** the `Z3.new` and `Z3.with` functions now take a
`Z3.Config` object as argument, which one may use to set some solver options
at initialization time
- add corresponding examples in the test-suite
- dropped dependency on `inline-c`
- removed `Data.Default` instance for `Config`

# v0.2
- make test-suite compatible with `smtlib-backends-0.2`
## v0.2 _(2022-12-16)_

### Added
- add usage examples in the test-suite

### Changed
- make test-suite compatible with `smtlib-backends-0.2`
2 changes: 1 addition & 1 deletion smtlib-backends-z3/smtlib-backends-z3.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ source-repository head
source-repository this
type: git
location: https://github.com/tweag/smtlib-backends
tag: 0.2
tag: 0.3
subdir: smtlib-backends-z3

library
Expand Down
8 changes: 4 additions & 4 deletions smtlib-backends.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,9 @@ synopsis:

description:
This library provides an extensible interface for interacting with SMT solvers
using SMT-LIB. The smtlib-backends-process provides a backend that runs solvers
as external processes, and the smtlib-backends-z3 package provides a backend that
uses inlined calls to Z3's C API.
using SMT-LIB. The smtlib-backends-process package provides a backend that
runs solvers as external processes, and the smtlib-backends-z3 package
provides a backend that uses inlined calls to Z3's C API.

license: MIT
license-file: LICENSE
Expand All @@ -25,7 +25,7 @@ source-repository head
source-repository this
type: git
location: https://github.com/tweag/smtlib-backends
tag: 0.2
tag: 0.3

library
hs-source-dirs: src
Expand Down

0 comments on commit 2f5e62a

Please sign in to comment.