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

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
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
LicenseBSD3
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
Upload dateWed Sep 3 04:29:34 UTC 2014
Uploaded byEricSeidel
Downloads234 total (54 in last 30 days)

Modules

Flags

NameDescriptionDefault
z3memLink to Z3Disabled

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