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

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

Requirements

In addition to the .cabal dependencies you require

• A Recent Ocaml compiler

• A Z3 Binary (http://z3.codeplex.com)

Modules

[Last Documentation]

Flags

Automatic Flags

Name	Description	Default
z3mem	Link to Z3	Disabled

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

Downloads

• liquid-fixpoint-0.2.0.0.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