The liquid-fixpoint package

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.


This package is a Haskell wrapper to the SMTLIB-based Horn-Clause/Logical Implication constraint solver used for Liquid Types.

The solver itself is written in Ocaml.

The package includes:

1. Types for Expressions, Predicates, Constraints, Solutions

2. Code for serializing the above

3. Code for parsing the results from the fixpoint.native binary

4. The Ocaml fixpoint code

5. (Deprecated) Z3 binaries if you want to link against the API.


In addition to the .cabal dependencies you require


Change logNone available
Dependenciesansi-terminal, array, attoparsec, base (==4.*), bifunctors, bytestring, cmdargs, containers, deepseq, directory, filemanip, filepath, ghc-prim, hashable, intern, liquid-fixpoint, mtl, parsec, pretty, process, syb, text, text-format, transformers, unordered-containers [details]
AuthorRanjit Jhala, Niki Vazou, Eric Seidel
Home page
Source repositoryhead: git clone
Executablesfixpoint, fixpoint.native
UploadedWed Sep 3 04:28:36 UTC 2014 by EricSeidel



z3memLink to Z3DisabledAutomatic

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info


Maintainers' corner

For package maintainers and hackage trustees