Changelog of @hackage/z3 408.2
Release Notes
408.2
Tested (sort of) with Z3 4.8.8.
- Added Optimization API. (David Cao)
- Added Sequences and regular expressions API. (Carlo Nucera)
- Added z3_solver_get_proof. ("0xd34df00d")
- Added MonadZ3 instance for ReaderT. ("0xd34df00d")
- Fixed two typos in docs. (Mauro Bringolf)
408.1
Tested (sort of) with Z3 4.8.4.
- Added bindings to
substitute
andisEqAST
. (Hengchu Zhang) - Added
MonadFail
instance forZ3
, required by GHC >=8.6. (Conal Elliott) - Updated
Z3_get_error_msg
signature (Z3 C API 4.8.7). (Kevin Quick) - Removed bindings to
Z3_fixedpoint_push
andZ3_fixedpoint_pop
(Z3 C API 4.8.5). (Eric Walkingshaw) - Replaced
z3_get_error_msg_ex
withz3_get_error_msg
(Z3 C API 4.8.5). (Alexander Knauth) - Added semigroups to dependencies for GHC <= 7. (Hogeyama)
408.0
- Enabled support for Z3 4.8. (Carlo Nucera)
- Required removing the Inteprolation API,
z3_get_parser_error
and other functions!
- Required removing the Inteprolation API,
- Do not crash on empty lists. (M Farkas-Dyck)
- Added binding for
Z3_mk_finite_domain_sort
. (M Farkas-Dyck) - Implemented workaround for
Z3.Base.toBool
to work on OS X. (Matthew Doty)
By the way, you have read correctly, this new version is 408.0. Find more details about the new version policy in the README.
4.3.1
- Fixed compatibility with base 4.11 due to SMP. (M Farkas-Dyck)
NOTE: This version didn't make it into Hackage.
4.3
Fixes
- Fixed memory leak due to typo in
Z3.Base.C
. (Deian Stefan)
New API support
- Added partial support for Fixedpoint API. (David Heath)
- Added more bindings to the Models API. (Daniel Gröber)
- Added Parser interface API. (Tristan Knoth)
Misc
- After many requests, I have moved the repository to GitHub: https://github.com/IagoAbal/haskell-z3.
- From now on the revision number (aka patch level) 0 will be omitted (so x.y instead of x.y.0).
4.2.0
This release removes support for SMT-LIB 1.x in order to be compatible with Z3 4.6.
4.1.2
This minor release extends the supported quantifiers API, and adds partial support for Z3's proof tactics.
- Improved support for theorem proving with quantifiers. (Jakub Daniel)
4.1.1
Another small release, made possible thanks to third-party contributions.
- Added bindings for getting the accessors of datatype constructors. (William Hallahan)
- Added bindings for declaring mutually recursive datatypes. (William Hallahan)
- Added partial support for the Interpolation API. (Jakub Daniel)
- Added bindings for deconstructing function applications. (Jakub Daniel)
- Added bindings for
simplify
andsimplifyEx
. (Gleb Popov) - Some code cleanup. (Jakub Daniel and Iago Abal)
4.1.0
Small maintenance release that however introduces one API breaking change.
- Added bindings for the Set API. (Nadia Polikarpova)
- Fix #4: Replace the now deprecated Z3_eval with Z3_model_eval.
- Fix #5: Check error codes right after an API call. (David Castro)
To fix #4 we had to change the type of modelEval
, which now takes
an extra Bool
parameter (to force model completion).
4.0.0
This release brings support for the new Z3 4.x API, and removes support for the old API. We are following a new version policy, yet compatible with Haskell's PVP. So new versions are of the form x.y.z, where x is the version of Z3 API supported, y is a major revision of the bindings, and z is a minor revision of the bindings. Consequently, we bumped the version to 4.0.0 :-).
Special thanks to Nadia Polikarpova,
who diagnosed a problem in our use of ForeignPtr
finalizers,
and proposed a fix.
Cabal package
- Relaxed dependencies, and removed upper bounds.
New features and API functions
- Switched to Z3 4.x API.
- Reference counting is managed by the gargabe collector.
- Algebraic datatypes. (KC Sivaramakrishnan)
Z3_get_ast_kind
,Z3_solver_check_assumptions
,Z3_solver_get_unsat_core
. (Nadia Polikarpova)Z3_mk_fresh_const
,Z3_mk_fresh_func_decl
. (KC Sivaramakrishnan)MonadFix
instance for theZ3
monad. (Pepe Iborra)- Hspec test-suite, with just a couple of tests, more to come...
- A few more helpers for creating numerals, evaluating expressions, and so on.
- Module
Z3.Base.C
, a very low-level interface to Z3 C API, is now exported. Just in case you want to write your own marshaling layer ;-)
Removals and API-breaking changes
- No more support for the old Z3 3.x API.
- Removed
Z3.Lang
module, this should re-appear as a separate package soon. MonadZ3
instances must beApplicative
.- Numerals API is now closer to Z3 C API.
So, for instance,
mkInt
now takes both an integer and a sort. You can usemkInteger
ormkIntNum
instead. Z3.Monad.assertCnstr
is now calledZ3.Monad.assert
.
Refactoring and clean-up
- Reduce boilerplate in Z3.Base.
- Fix docs to distinguish Z3 API functions and helpers.
0.3.2
Thanks to Scott West and Nadia Polikarpova for contributing to this release.
Fixes
- Fixed solverCheckAndGetModel to return a model from an unknown satisfiability result, if one exists. (Nadia Polikarpova)
- Fixed mkMap API function to do not take the number of arrays as an input parameter, this should be equals to the length of the input array list. Strictly speaking this is a minor break of the API but it was considered a but and therefore fixed.
Refactoring and clean-up
- Reduced marshalling boilerplate in Z3.Base. This is a very important step towards supporting Z3 4.0 API.
- Improved API documentation. If you are having difficulties due to (presumably) poor API or source documentation, please let us know.
New features
- Support running multiple queries under the same logical context, using evalZ3WithEnv. (Scott West)
Newly supported API functions
- Many solver-related API functions (Scott West and Nadia Polikarpova).
- z3_mk_forall_const (Scott West), z3_mk_exists_const.
- Z3_get_version.
Deprecations
- We deprecate showContext, showModel and getModel; since we prefer to avoid deviations from Z3 API names. Use contextToString, modelToString and checkAndGetModel instead.
- We deprecate the Z3.Lang interface, that will be moved to a separate pacakge. Few people is using this (_DSL_ish) interface and it is arguably more unstable than Z3.Base or Z3.Monad. It also introduces dependencies with GHC extensions like type families that we prefer to avoid in a more stable package.
Misc
- Add SMT to categories in z3.cabal.