Skip to content

Commit

Permalink
104-timeouts: bump version
Browse files Browse the repository at this point in the history
  • Loading branch information
bruderj15 committed Sep 12, 2024
1 parent d111a01 commit ce6d18c
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 1 deletion.
23 changes: 23 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,29 @@ 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/).

## v2.7.0 _(2024-09-12)_

### Added
- Added helpful instances for standard types for `Codec` to ease deriving.
- Added decorator `timingout` in `Language.Hasmtlib.Type.Solver` to set a time-out for solvers.
Unfortunately as of SMTLib standard v2.6 there is no SMT-Option for this. Although some solvers like `Z3` (unreliably) support it,
we instead do it by internally coordinating the kill of the solver process from Haskell using `System.Timeout.Lifted#timeout`. Works like a charme.
- Added `Language.Hasmtlib.Type.Debugger` for debugging problem construction and solver interaction.

### Changed
- *(breaking change)* Completely revised the way solver process-configurations are handled and debugged.
Solvers which previously had the type `Process.Config` from `smtlib-backends` now have the type `SolverConfig` from `Language.Hasmtlib.Type.Solver`.
This bundles information on the executable of the solver with additional information such as debugging and time-outs.
Actual solver creation still is done by funtion `solver`. Therefore this change is only breaking, if you created custom solvers or debugged solvers.
- Debugging solvers changed from `solveWith (debug z3 def) $ ...` to `solveWith (solver $ debugging z3 def) $ ...`.
Also note that there are plenty debugging configurations besides `def` existing in `Language.Hasmtlib.Type.Debugger` now.
- Interactive solving before was a two-stepper like `iZ3 <- interactiveSolver z3 ; interactiveWith iZ3 $ ...`.
Leveraging `SolverConfig` this has been changed to a more uniform way with `interactiveWith z3 $ do ...`.
Also note that `debugInteractiveWith z3 $ ...` now is replaced by `interactiveWith (debugging def z3) $ ...`.

### Removed
- Removed `Language.Hasmtlib.Solver.Common`. Contents are now in `Language.Hasmtlib.Type.Solver`.

## v2.6.3 _(2024-09-07)_

### Added
Expand Down
2 changes: 1 addition & 1 deletion hasmtlib.cabal
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
cabal-version: 3.0

name: hasmtlib
version: 2.6.3
version: 2.7.0
synopsis: A monad for interfacing with external SMT solvers
description: Hasmtlib is a library for generating SMTLib2-problems using a monad.
It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.
Expand Down

0 comments on commit ce6d18c

Please sign in to comment.