liquid-fixpoint: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

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

• A Z3 (http://z3.codeplex.com) or CVC4 (http://cvc4.cs.nyu.edu) binary. If on Windows, please make sure to place the binary and any associated DLLs in your "cabal/bin" folder, right next to the fixpoint.native.exe binary.

• An ocaml compiler (if installing with -fbuild-external).

Modules

[Index]

Flags

Automatic Flags

Name	Description	Default
z3mem	Link to Z3	Disabled
build-external	Build 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

• liquid-fixpoint-0.3.0.1.tar.gz [browse] (Cabal source package)
• Package description (as included in the package)

Maintainer's Corner

Package maintainers

• AlfredoDiNapoli, AndresLoeh, EricSeidel, FacundoDominguez, ranjitjhala, niki, clayrat

For package maintainers and hackage trustees

• edit package information

Candidates

• 0.2.0.0, 0.6.0.2, 0.7.0.2, 0.7.0.3, 0.8.0.2, 0.8.10.1, 0.8.10.2, 0.9.2.5, 0.9.6.3.4