@hackage liquid-fixpoint0.4.0.0

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).