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
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
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
UploadedFri May 22 00:29:58 UTC 2015 by EricSeidel
DistributionsNixOS:0.3.0.1
Downloads1107 total (110 in last 30 days)
StatusDocs available [build log]
Last success reported on 2015-05-23 [all 1 reports]

Modules

[Index]

Flags

NameDescriptionDefault
z3memLink to Z3Disabled
build-externalBuild fixpoint.native binary from source (requires ocaml)Disabled

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