z3: Bindings for the Z3 Theorem Prover

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

Bindings for the Z3 Theorem Prover.

This package is still a work in progress. Low and medium-level bindings to the Z3 API are provided (Z3.Base.C and Z3.Base) in the spirit of yices-painless. These APIs are still incomplete but usable. The high-level API (Z3.Monad) is still very experimental.

More information about Z3:

Versions [faq] 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 [details]
License BSD-3-Clause
Copyright 2012, Iago Abal, David Castro
Author Iago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com>
Maintainer Iago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com>
Category Math, Theorem Provers, Formal Methods
Home page http://bitbucket.org/iago/z3-haskell
Source repo head: hg clone https://bitbucket.org/iago/z3-haskell
Uploaded by IagoAbal at 2012-07-24T23:35:49Z
Distributions NixOS:408.2
Downloads 9028 total (29 in the last 30 days)
Rating 2.25 (votes: 2) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs not available [build log]
All reported builds failed as of 2016-12-24 [all 8 reports]


  • Z3
    • Z3.Base
      • Z3.Base.C
    • Z3.Exprs
    • Z3.Monad
    • Z3.Types


Maintainer's Corner

For package maintainers and hackage trustees