z3: Bindings for the Z3 Theorem Prover

[ bit-vectors, bsd3, formal-methods, library, math, smt, theorem-provers ] [ Propose Tags ] [ Report a vulnerability ]

Bindings for the Z3 Theorem Prover (http://z3.codeplex.com).

Low-level bindings to the Z3 API are provided by Z3.Base, this API is still incomplete but pretty much stable.

A simple but convenient wrapper for Z3.Base is provided by Z3.Monad.

The Z3.Lang API provides a high-level interface to Z3, but it is still very experimental and likely to change.

  • In version 0.3.2 the Z3.Lang interface has been deprecated, we will move it to a dedicated package.

Important notes:

A changelog is available at https://bitbucket.org/iago/z3-haskell/src/tip/CHANGES.md

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

Versions [RSS] 0.1.1, 0.2.0, 0.3.0, 0.3.1, 0.3.2, 4.0.0, 4.1.0, 4.1.1, 4.1.2, 4.2.0, 4.3, 4.3.1, 408.0, 408.1, 408.2
Dependencies base (>3 && <5), containers, mtl (<2.1 || >2.1) [details]
License BSD-3-Clause
Copyright 2012-2014, Iago Abal, David Castro
Author Iago Abal <mail@iagoabal.eu>, David Castro <david.castro.dcp@gmail.com>
Maintainer Iago Abal <mail@iagoabal.eu>, David Castro <david.castro.dcp@gmail.com>
Uploaded by IagoAbal at 2014-03-21T21:26:24Z
Category Math, SMT, Theorem Provers, Formal Methods
Home page http://bitbucket.org/iago/z3-haskell
Source repo head: hg clone https://bitbucket.org/iago/z3-haskell
Reverse Dependencies 6 direct, 0 indirect [details]
Downloads 11464 total (35 in the last 30 days)
Rating 2.25 (votes: 2) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user [build log]
All reported builds failed [all 1 reports]