« Changelog History


hz3 v4.0.0 Release Notes

Release Date: 2015-04-11 // about 9 years ago

  • 🚀 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 the Z3 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 be Applicative.
    • Numerals API is now closer to Z3 C API. So, for instance, mkInt now takes both an integer and a sort. You can use mkInteger or mkIntNum instead.
    • Z3.Monad.assertCnstr is now called Z3.Monad.assert.

    🔨 Refactoring and clean-up

    • ⬇️ Reduce boilerplate in Z3.Base.
    • 🛠 Fix docs to distinguish Z3 API functions and helpers.