The liquid-fixpoint package

[Tags: bsd3, library, program]

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 and pre-compiled binaries

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

Requirements

In addition to the .cabal dependencies you require

Properties

Versions0.1.0.0, 0.2.0.0, 0.2.1.0, 0.2.1.1, 0.2.2.0, 0.2.3.0, 0.2.3.1, 0.2.3.2, 0.3.0.0, 0.3.0.1, 0.4.0.0
Change logNone available
Dependenciesansi-terminal, array, attoparsec, base (>=4.7 && <5), 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]
LicenseBSD3
Copyright2010-15 Ranjit Jhala, University of California, San Diego.
AuthorRanjit Jhala, Niki Vazou, Eric Seidel
Maintainerjhala@cs.ucsd.edu
CategoryLanguage
Home pagehttps://github.com/ucsd-progsys/liquid-fixpoint
Source repositoryhead: git clone https://github.com/ucsd-progsys/liquid-fixpoint/
Executablesfixpoint, fixpoint.native
UploadedWed Aug 12 20:21:26 UTC 2015 by EricSeidel
UpdatedWed Aug 12 21:05:48 UTC 2015 by EricSeidel to revision 2
Downloads1300 total (109 in last 30 days)
Votes
0 []
StatusDocs available [build log]
Last success reported on 2015-08-12 [all 1 reports]

Modules

[Index]

Flags

NameDescriptionDefaultType
z3memLink to Z3DisabledAutomatic
build-externalBuild fixpoint.native binary from source (requires ocaml)DisabledAutomatic

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

Downloads

Maintainers' corner

For package maintainers and hackage trustees